Re-enable tests that were previously disabled

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 {

src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

@@ -285,6 +285,10 @@ public <T> void sequentialInterpolation() throws SolverException, InterruptedExc
     List<BooleanFormula> 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<BooleanFormula> itps5 =
         stack.getSeqInterpolants(
             Lists.transform(ImmutableList.of(TA, TA, TB, TC, TD, TA, TD), ImmutableSet::of));

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();
 

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> 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<SolverContext> 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<BooleanFormula> 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 <T> void localInterpolationTest() throws InterruptedException, SolverExce
   public <T> 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"));