diff --git a/src/org/sosy_lab/java_smt/test/DebugModeTest.java b/src/org/sosy_lab/java_smt/test/DebugModeTest.java index dbfe92732b..4d614a82e8 100644 --- a/src/org/sosy_lab/java_smt/test/DebugModeTest.java +++ b/src/org/sosy_lab/java_smt/test/DebugModeTest.java @@ -112,6 +112,7 @@ public void nonLocalThreadTest() { }); // We expect debug mode to throw an exception only on CVC5 + // TODO CVC5 supports this now. Update debug mode if (solverToUse() == Solvers.CVC5) { assertThrows(IllegalStateException.class, () -> checkForExceptions(result)); } else { @@ -179,7 +180,7 @@ public void noSharedDeclarationsTest() throws InvalidConfigurationException { newFmgr.declareUF( "id", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType)); - // We expect debug mode to throw an exception for all solvers, except Princess, CVC4 and Yices + // We expect debug mode to throw an exception for all solvers, except Princess and Yices if (!List.of(Solvers.PRINCESS, Solvers.YICES2).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> checkDeclarationInDebugContext(id)); } else { diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 9287b00f67..90275f1d8e 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java @@ -285,6 +285,10 @@ public void sequentialInterpolation() throws SolverException, InterruptedExc List itps4 = stack.getSeqInterpolants( Lists.transform(ImmutableList.of(TA, TA, TA, TB, TC, TD, TD), ImmutableSet::of)); + + // FIXME With CVC5 the last interpolant returned by CVC5InterpolatingProver.getCVC5Interpolation + // is "null". Replacing it with "false" fixes the test + List itps5 = stack.getSeqInterpolants( Lists.transform(ImmutableList.of(TA, TA, TB, TC, TD, TA, TD), ImmutableSet::of)); diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index bd6e643c09..d769c4b4f1 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -1152,10 +1152,7 @@ public void testGetArrays3() throws SolverException, InterruptedException { requireArrays(); requireArrayModel(); - assume() - .withMessage("As of now, only Princess does not support multi-dimensional arrays") - .that(solver) - .isNotEqualTo(Solvers.PRINCESS); + // FIXME Add support for multi-dimensional array to the Princess backend // create formula for "arr[5][3][1]==x && x==123" BooleanFormula f = @@ -1732,7 +1729,6 @@ private void checkModelAssignmentsValid( // supported yet // TODO: only filter out UF formulas here, not all if (solver != Solvers.BOOLECTOR) { - // CVC5 crashes here assertThatFormula(bmgr.and(pModelAssignments)).implies(constraint); } } @@ -2404,8 +2400,7 @@ public void testGetBooleans1() throws SolverException, InterruptedException { false); } - @Test // (timeout = 10_000) - // TODO CVC5 crashes on making the first boolean symbol when using timeout ???. + @Test(timeout = 10_000) public void testDeeplyNestedFormulaLIA() throws SolverException, InterruptedException { requireIntegers(); @@ -2415,8 +2410,7 @@ public void testDeeplyNestedFormulaLIA() throws SolverException, InterruptedExce var -> imgr.equal(var, imgr.makeNumber(1))); } - @Test // (timeout = 10_000) - // TODO CVC5 crashes on making the first boolean symbol when using timeout ???. + @Test(timeout = 10_000) public void testDeeplyNestedFormulaBV() throws SolverException, InterruptedException { requireBitvectors(); diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 5718007828..7546f46ead 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -9,12 +9,9 @@ package org.sosy_lab.java_smt.test; import static com.google.common.truth.TruthJUnit.assume; -import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import com.google.common.collect.ImmutableList; -import com.google.common.truth.Truth; -import java.util.Collection; import java.util.concurrent.ExecutionException; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; @@ -41,9 +38,6 @@ public class SolverThreadLocalityTest extends SolverBasedTest0.ParameterizedSolv private HardIntegerFormulaGenerator hardProblem; private static final int DEFAULT_PROBLEM_SIZE = 8; - private static final Collection SOLVERS_NOT_SUPPORTING_FORMULA_THREAD_SHARING = - ImmutableList.of(Solvers.CVC5); - @Before public void makeThreads() { executor = Executors.newFixedThreadPool(2); @@ -78,7 +72,6 @@ public void allLocalTest() throws InterruptedException, SolverException { public void nonLocalContextTest() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); // generate a new context in another thread, i.e., non-locally Future result = executor.submit(() -> factory.generateContext()); @@ -113,7 +106,6 @@ public void nonLocalContextTest() public void nonLocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); // generate a new formula in another thread, i.e., non-locally Future result = @@ -142,7 +134,6 @@ public void nonLocalFormulaTest() @Test public void nonLocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); @@ -173,53 +164,6 @@ public void nonLocalProverTest() throws InterruptedException, ExecutionException assert task.get() == null; } - @Test - public void nonLocalFormulaTranslationTest() throws Throwable { - // Test that even when using translation, the thread local problem persists for CVC5 - requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - - BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); - - // generate a new prover in another thread, i.e., non-locally - Future task; - if (SOLVERS_NOT_SUPPORTING_FORMULA_THREAD_SHARING.contains(solverToUse())) { - task = - executor.submit( - () -> - assertThrows( - io.github.cvc5.CVC5ApiException.class, - () -> { - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push( - context - .getFormulaManager() - .translateFrom(formula, context.getFormulaManager())); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException exception) { - throw new RuntimeException(exception); - } - })); - Truth.assertThat(task.get()).isInstanceOf(io.github.cvc5.CVC5ApiException.class); - - } else { - task = - executor.submit( - () -> { - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push( - context - .getFormulaManager() - .translateFrom(formula, context.getFormulaManager())); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException exception) { - throw new RuntimeException(exception); - } - }); - Truth.assertThat(task.get()).isNull(); - } - } - @Override protected Logics logicToUse() { return Logics.QF_LIA; @@ -264,7 +208,6 @@ public void localInterpolationTest() throws InterruptedException, SolverExce public void nonLocalInterpolationTest() throws InterruptedException, ExecutionException { requireIntegers(); requireInterpolation(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); BooleanFormula f1 = imgr.lessThan(imgr.makeVariable("A"), imgr.makeVariable("B")); BooleanFormula f2 = imgr.lessThan(imgr.makeVariable("B"), imgr.makeVariable("A"));