diff --git a/build/build-publish-solvers/solver-cvc4.xml b/build/build-publish-solvers/solver-cvc4.xml index 749a7397a4..a1f10aa54b 100644 --- a/build/build-publish-solvers/solver-cvc4.xml +++ b/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 +SPDX-FileCopyrightText: 2026 Dirk Beyer SPDX-License-Identifier: Apache-2.0 --> diff --git a/lib/ivy.xml b/lib/ivy.xml index 7444de2cd9..d789da813b 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java index 318313ff43..4bf383f272 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java +++ b/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 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( diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java index 6cac04b915..fb041ca180 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -37,10 +37,6 @@ class CVC4TheoremProver extends AbstractProverWithAllSat implements ProverEnvironment, BasicProverEnvironment { - // 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 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 BooleanFormulaManager pBmgr) { super(pOptions, pBmgr, pShutdownNotifier); - synchronized (CVC4TheoremProver.class) { - provers.add(this); - } - creator = pFormulaCreator; randomSeed = pRandomSeed; incremental = !enableSL; @@ -245,7 +237,7 @@ public Optional> unsatCoreOverAssumptions( @Override public void close() { if (!closed) { - // Never release a prover + // Never close the context } super.close(); }