Merge pull request #642 from sosy-lab/cvc4-noFinalizers

CVC4: update CVC4 to v1.8.1-X to remove buggy finalizers (again)

Author: kfriedberger

build/build-publish-solvers/solver-cvc4.xml

@@ -5,7 +5,7 @@ This file is part of JavaSMT,
 an API wrapper for a collection of SMT solvers:
 https://github.com/sosy-lab/java-smt
 
-SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->

lib/ivy.xml

@@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.17.0-1009b13" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.9.2-ge4c80308" 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.1-g40eac7f05" conf="runtime-cvc4->solver-cvc4; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8.1-11-g1f9dbdca4" conf="runtime-cvc4->solver-cvc4; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="2026-02-26-d22638a" 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.9.0-gd13ef925" conf="runtime-bitwuzla-x64->solver-bitwuzla-x64; runtime-bitwuzla-arm64->solver-bitwuzla-arm64; contrib->sources,javadoc"/>

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java

@@ -13,8 +13,6 @@
 import edu.stanford.CVC4.ExprManager;
 import edu.stanford.CVC4.SExpr;
 import edu.stanford.CVC4.SmtEngine;
-import java.util.ArrayList;
-import java.util.List;
 import java.util.Set;
 import java.util.function.Consumer;
 import java.util.logging.Level;
@@ -31,10 +29,6 @@
 
 public final class CVC4SolverContext extends AbstractSolverContext {
 
-  // Keep a global list of all contexts to prevent the garbge collector from doing its job
-  // See https://github.com/sosy-lab/java-smt/issues/169
-  private static List<CVC4SolverContext> contexts = new ArrayList<>();
-
   // creator is final, except after closing, then null.
   private CVC4FormulaCreator creator;
   private final ShutdownNotifier shutdownNotifier;
@@ -49,10 +43,6 @@ private CVC4SolverContext(
     this.creator = creator;
     shutdownNotifier = pShutdownNotifier;
     randomSeed = pRandomSeed;
-
-    synchronized (CVC4SolverContext.class) {
-      contexts.add(this);
-    }
   }
 
   public static SolverContext create(

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

@@ -37,10 +37,6 @@
 class CVC4TheoremProver extends AbstractProverWithAllSat<Void>
     implements ProverEnvironment, BasicProverEnvironment<Void> {
 
-  // Keep a global list of all provers to prevent the garbge collector from doing its job
-  // See https://github.com/sosy-lab/java-smt/issues/169
-  private static List<CVC4TheoremProver> provers = new ArrayList<>();
-
   private final CVC4FormulaCreator creator;
   private final int randomSeed;
   SmtEngine smtEngine; // final except for SL theory
@@ -68,10 +64,6 @@ class CVC4TheoremProver extends AbstractProverWithAllSat<Void>
       BooleanFormulaManager pBmgr) {
     super(pOptions, pBmgr, pShutdownNotifier);
 
-    synchronized (CVC4TheoremProver.class) {
-      provers.add(this);
-    }
-
     creator = pFormulaCreator;
     randomSeed = pRandomSeed;
     incremental = !enableSL;
@@ -245,7 +237,7 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
   @Override
   public void close() {
     if (!closed) {
-      // Never release a prover
+      // Never close the context
     }
     super.close();
   }