diff --git a/lib/ivy.xml b/lib/ivy.xml
index 089d59aadb..5f5df5f5dd 100644
--- a/lib/ivy.xml
+++ b/lib/ivy.xml
@@ -193,7 +193,7 @@ SPDX-License-Identifier: Apache-2.0
-
+
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java
index 71d6b2a463..9b06865d0e 100644
--- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java
+++ b/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 definedFormulas;
+ private final Set definedFormulas;
private final Thread solverThread = Thread.currentThread();
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java
index e15fdec270..9a61f193fd 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java
+++ b/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
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
index 3d070b61b5..97e0d269b2 100644
--- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java
+++ b/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;
}
}
diff --git a/src/org/sosy_lab/java_smt/test/DebugModeTest.java b/src/org/sosy_lab/java_smt/test/DebugModeTest.java
index c0dedaa668..f6d5ea092c 100644
--- a/src/org/sosy_lab/java_smt/test/DebugModeTest.java
+++ b/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);
diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
index f6f1954fb6..8ea5406061 100644
--- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java
+++ b/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 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.
diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java
index 7619b7b1fe..a08232a24a 100644
--- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java
+++ b/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.
diff --git a/src/org/sosy_lab/java_smt/test/TimeoutTest.java b/src/org/sosy_lab/java_smt/test/TimeoutTest.java
index ffcdcb05b3..59d6d6a0c3 100644
--- a/src/org/sosy_lab/java_smt/test/TimeoutTest.java
+++ b/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")