Commit afab137a authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Updated test case to make it really useful (thanks STAMP).

parent 09e9173e
Pipeline #567 passed with stages
in 29 minutes and 38 seconds
...@@ -29,6 +29,7 @@ ...@@ -29,6 +29,7 @@
*******************************************************************************/ *******************************************************************************/
package org.sat4j; package org.sat4j;
import static org.junit.Assert.assertFalse;
import static org.junit.Assert.assertTrue; import static org.junit.Assert.assertTrue;
import java.io.FileNotFoundException; import java.io.FileNotFoundException;
...@@ -61,15 +62,17 @@ public class BugSAT26 { ...@@ -61,15 +62,17 @@ public class BugSAT26 {
} }
@Test @Test
public void testConsecutiveCallToSolver() throws ContradictionException, public void testConsecutiveCallToSolver()
TimeoutException { throws ContradictionException, TimeoutException {
assertTrue(this.xplain.isSatisfiable()); assertTrue(this.xplain.isSatisfiable());
int i = 0; int i = 0;
while (i < 5) { while (i < 5) {
VecInt assumption = new VecInt(); VecInt assumption = new VecInt();
assumption.push(1187); assumption.push(1187);
IConstr constr = this.xplain.addClause(assumption); IConstr constr = this.xplain.addClause(assumption);
assertFalse(this.xplain.isSatisfiable());
this.xplain.removeConstr(constr); this.xplain.removeConstr(constr);
assertTrue(this.xplain.isSatisfiable());
i++; i++;
} }
} }
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment