Merge pull request #499 from sosy-lab/cvc5/update_2025-07-24

update CVC5 to latest version from 2025-07-24

Author: kfriedberger

lib/ivy.xml

@@ -193,7 +193,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.9.0-gef441e1c" 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-05-16-8aeaa19" conf="runtime-cvc5-x64->solver-cvc5-x64; runtime-cvc5-arm64->solver-cvc5-arm64"/>
+        <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="2025-07-29-6dacfa5" 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.8.1-gc1454189" conf="runtime-bitwuzla-x64->solver-bitwuzla-x64; runtime-bitwuzla-arm64->solver-bitwuzla-arm64; contrib->sources,javadoc"/>
 

src/org/sosy_lab/java_smt/basicimpl/AbstractProverWithAllSat.java

@@ -12,6 +12,7 @@
 import com.google.common.collect.ImmutableList;
 import java.util.ArrayDeque;
 import java.util.Deque;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Set;
 import org.sosy_lab.common.ShutdownNotifier;
@@ -67,6 +68,7 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> importantPr
   private <R> void iterateOverAllModels(
       AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
       throws SolverException, InterruptedException {
+    final Set<ImmutableList<BooleanFormula>> modelEvaluations = new LinkedHashSet<>();
     while (!isUnsat()) {
       shutdownNotifier.shutdownIfNecessary();
 
@@ -87,6 +89,11 @@ private <R> void iterateOverAllModels(
       }
 
       final ImmutableList<BooleanFormula> values = valuesOfModel.build();
+      // avoid endless loops in case of repeated models.
+      Preconditions.checkState(
+          modelEvaluations.add(values),
+          "The model evaluation %s was found before. ALLSAT computation did not make progress.",
+          values);
       callback.apply(values);
       shutdownNotifier.shutdownIfNecessary();
 

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

@@ -149,10 +149,13 @@ public void apply(List<BooleanFormula> pModel) {
     assertThat(env.allSat(callback, ImmutableList.of(v1, v2))).isEqualTo(EXPECTED_RESULT);
   }
 
-  @Test
+  @Test(timeout = 5_000)
   public void allSatTest_xor() throws SolverException, InterruptedException {
     requireIntegers();
 
+    // We have the following constraint: '(i=1) XOR (i=2)'
+    // with the predicates b1 and b2 defined as: '(i=1) <=> b1' and '(i=2) <=> b2'.
+    // We expect exactly two models from ALLSAT: {b1,-b2} and {-b1, b2}.
     IntegerFormula a = imgr.makeVariable("i");
     IntegerFormula n1 = imgr.makeNumber(1);
     IntegerFormula n2 = imgr.makeNumber(2);
@@ -168,9 +171,6 @@ public void allSatTest_xor() throws SolverException, InterruptedException {
     env.push(bmgr.equivalence(v1, cond1));
     env.push(bmgr.equivalence(v2, cond2));
 
-    // ((i=1) XOR (i=2)) & b1 <=> (i=1) & b2 <=> (i=2)
-    // query ALLSAT for predicates [b1, b2] --> {[b1,-b2], [-b1,b2]}
-
     TestAllSatCallback callback = new TestAllSatCallback();
 
     assertThat(env.allSat(callback, ImmutableList.of(v1, v2))).isEqualTo(EXPECTED_RESULT);