diff --git a/src/main/java/de/stups/probkodkod/SolverChecker.java b/src/main/java/de/stups/probkodkod/SolverChecker.java index 5d358894ff87b4eb0bce203eb936b1c675183f97..cf7238a7f31af581a8f2a10e4addc78d17085564 100644 --- a/src/main/java/de/stups/probkodkod/SolverChecker.java +++ b/src/main/java/de/stups/probkodkod/SolverChecker.java @@ -41,7 +41,7 @@ public class SolverChecker { } } - public static SATFactory determineSatFactory(SATFactory... factories) { + private static SATFactory determineSatFactory(SATFactory... factories) { Map<String, Throwable> throwables = new HashMap<String, Throwable>(); for (final SATFactory factory : factories) { try { diff --git a/src/test/java/de/stups/probkodkod/NegativeIntTest.java b/src/test/java/de/stups/probkodkod/NegativeIntTest.java index 164137f1e26509c0d426b52688bd968b7b9d9267..0f79c5c78406cc98276c84f35c41ebd595b2f673 100644 --- a/src/test/java/de/stups/probkodkod/NegativeIntTest.java +++ b/src/test/java/de/stups/probkodkod/NegativeIntTest.java @@ -5,6 +5,9 @@ package de.stups.probkodkod; import java.util.Iterator; +import org.junit.Assert; +import org.junit.Test; + import kodkod.ast.Formula; import kodkod.ast.IntConstant; import kodkod.ast.Relation; @@ -17,9 +20,6 @@ import kodkod.instance.TupleFactory; import kodkod.instance.TupleSet; import kodkod.instance.Universe; -import org.junit.Assert; -import org.junit.Test; - /** * @author plagge * @@ -45,7 +45,7 @@ public class NegativeIntTest { bounds.bound(x, factory.allOf(1)); final Formula formula = x.sum().eq(IntConstant.constant(value)); final Solver solver = new Solver(); - solver.options().setSolver(SolverChecker.determineSatFactory()); + solver.options().setSolver(SolverChecker.determineSatFactory(SATSolver.sat4j)); solver.options().setBitwidth(5); final Iterator<Solution> iterator = solver.solveAll(formula, bounds); Assert.assertTrue("solution expected", iterator.hasNext()); @@ -58,9 +58,7 @@ public class NegativeIntTest { final Object atom = tuple.atom(0); sum += ((Integer) atom).intValue(); } - Assert.assertEquals("constant in formula and solution should be same", - value, sum); - Assert.assertTrue("no other solution expected", !iterator.hasNext() - || iterator.next().instance() == null); + Assert.assertEquals("constant in formula and solution should be same", value, sum); + Assert.assertTrue("no other solution expected", !iterator.hasNext() || iterator.next().instance() == null); } }