Update CVC5 to fix the concurrency issues

lib/ivy.xml

@@ -193,7 +193,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.8.0-sosy0-ge831bf23" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="2025-04-03-ee76c36" conf="runtime-cvc5-x64->solver-cvc5-x64; runtime-cvc5-arm64->solver-cvc5-arm64"/>
+        <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="2025-05-16-8aeaa19" conf="runtime-cvc5-x64->solver-cvc5-x64; runtime-cvc5-arm64->solver-cvc5-arm64"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
         <dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.7.0-13.1-g595512ae" conf="runtime-bitwuzla-x64->solver-bitwuzla-x64; runtime-bitwuzla-arm64->solver-bitwuzla-arm64; contrib->sources,javadoc"/>
 

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java

@@ -48,8 +48,6 @@ public class DebuggingSolverInformation {
       Map.of(
           Solvers.PRINCESS,
           ConcurrentHashMap.newKeySet(),
-          Solvers.CVC5,
-          ConcurrentHashMap.newKeySet(),
           Solvers.YICES2,
           ConcurrentHashMap.newKeySet());
 
@@ -60,12 +58,10 @@ public class DebuggingSolverInformation {
       Map.of(
           Solvers.CVC4,
           ConcurrentHashMap.newKeySet(),
-          Solvers.CVC5,
-          ConcurrentHashMap.newKeySet(),
           Solvers.YICES2,
           ConcurrentHashMap.newKeySet());
 
-  private Set<Formula> definedFormulas;
+  private final Set<Formula> definedFormulas;
 
   private final Thread solverThread = Thread.currentThread();
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java

@@ -202,7 +202,7 @@ public void checkFPConversion() throws CVC5ApiException {
             () -> termManager.mkFloatingPoint(8, 24, bvOneFourth));
     assertThat(e.toString())
         .contains(
-            "invalid argument '((_ int2bv 32) (to_int (/ 1 4)))' for 'val', expected bit-vector"
+            "invalid argument '((_ int_to_bv 32) (to_int (/ 1 4)))' for 'val', expected bit-vector"
                 + " value");
   }
 
@@ -950,7 +950,7 @@ public void checkQuantifierEliminationBV() throws CVC5ApiException {
 
     Term quantElim = solver.getQuantifierElimination(assertion);
 
-    assertThat(quantElim.toString()).isEqualTo("(or (= #b01 (bvneg x_bv)) (= #b01 x_bv))");
+    assertThat(quantElim.toString()).isEqualTo("(or (= #b01 (bvneg x_bv)) (= x_bv #b01))");
   }
 
   @Test

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java

@@ -196,19 +196,15 @@ static void setSolverOptions(
 
   @Override
   public String getVersion() {
-    String version = solver.getInfo("version");
-    if (version.startsWith("\"") && version.endsWith("\"")) {
-      version = version.substring(1, version.length() - 1);
-    }
-    return "CVC5 " + version;
+    return "CVC5 " + solver.getVersion();
   }
 
   @Override
   public void close() {
     if (creator != null) {
       closed = true;
-      termManager.deletePointer();
       solver.deletePointer();
+      termManager.deletePointer();
       creator = null;
     }
   }

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

@@ -149,7 +149,7 @@ public void noSharedFormulasTest()
       BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE);
 
       // We expect debug mode to throw an exception for all solvers, except CVC4, CVC5 and Yices
-      if (!List.of(Solvers.CVC4, Solvers.CVC5, Solvers.YICES2).contains(solverToUse())) {
+      if (!List.of(Solvers.CVC4, Solvers.YICES2).contains(solverToUse())) {
         assertThrows(IllegalArgumentException.class, () -> checkFormulaInDebugContext(formula));
       } else {
         checkFormulaInDebugContext(formula);
@@ -180,7 +180,7 @@ public void noSharedDeclarationsTest() throws InvalidConfigurationException {
               "id", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType));
 
       // We expect debug mode to throw an exception for all solvers, except Princess, CVC4 and Yices
-      if (!List.of(Solvers.PRINCESS, Solvers.CVC5, Solvers.YICES2).contains(solverToUse())) {
+      if (!List.of(Solvers.PRINCESS, Solvers.YICES2).contains(solverToUse())) {
         assertThrows(IllegalArgumentException.class, () -> checkDeclarationInDebugContext(id));
       } else {
         checkDeclarationInDebugContext(id);

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

@@ -124,11 +124,6 @@ public void checkThatSolverIsAvailable() throws InvalidConfigurationException {
           .that(solver)
           .isNotEqualTo(Solvers.MATHSAT5);
     }
-
-    assume()
-        .withMessage("Solver does not support concurrency without concurrent context.")
-        .that(solver)
-        .isNotEqualTo(Solvers.CVC5);
   }
 
   private void requireConcurrentMultipleStackSupport() {
@@ -303,7 +298,7 @@ public void testFormulaTranslationWithConcurrentContexts()
     assume()
         .withMessage("Solver does not support translation of formulas")
         .that(solver)
-        .isNoneOf(Solvers.CVC4, Solvers.PRINCESS);
+        .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS);
 
     ConcurrentLinkedQueue<ContextAndFormula> contextAndFormulaList = new ConcurrentLinkedQueue<>();
 
@@ -540,7 +535,7 @@ public void continuousRunningThreadFormulaTransferTranslateTest() {
     assume()
         .withMessage("Solver does not support translation of formulas")
         .that(solver)
-        .isNoneOf(Solvers.CVC4, Solvers.PRINCESS);
+        .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS);
 
     // This is fine! We might access this more than once at a time,
     // but that gives only access to the bucket, which is threadsafe.

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

@@ -350,7 +350,8 @@ public void wrongContextTest()
             Solvers.Z3,
             Solvers.PRINCESS,
             Solvers.BOOLECTOR,
-            Solvers.BITWUZLA);
+            Solvers.BITWUZLA,
+            Solvers.CVC5);
 
     // FIXME: This test tries to use a formula that was created in a different context. We expect
     //  this test to fail for most solvers, but there should be a unique error message.

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

@@ -65,7 +65,10 @@ protected Logics logicToUse() {
 
   @Before
   public void setUp() {
-    // FIXME CVC5 has interruptions, but crashes on Windows, probably due to concurrency issues
+    // FIXME CVC5 does not support interruption and will segfault once the timeout is reached
+    //   The issue here seems to be that CVC5SolverContext.close() will free the C++ objects while
+    //   the solver is still running. We could consider finding a work-around for this, or maybe
+    //   ask the developers for a way to interrupt the solver.
     // TODO Add interruption for Princess
     assume()
         .withMessage(solverToUse() + " does not support interruption")