From f6c025db50157f87da0b7f66ed2d1c7914bf9fd8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 6 Apr 2026 20:33:15 +0200 Subject: [PATCH 1/4] CVC4: Remove the finalizers Reverts the workaround from a8eead251761d9997676b20502e2903ff5e7824a --- build/build-publish-solvers/solver-cvc4.xml | 17 ++++++++++++++++- .../solvers/cvc4/CVC4SolverContext.java | 10 ---------- .../solvers/cvc4/CVC4TheoremProver.java | 10 +--------- 3 files changed, 17 insertions(+), 20 deletions(-) diff --git a/build/build-publish-solvers/solver-cvc4.xml b/build/build-publish-solvers/solver-cvc4.xml index 749a7397a4..99565e6e40 100644 --- a/build/build-publish-solvers/solver-cvc4.xml +++ b/build/build-publish-solvers/solver-cvc4.xml @@ -75,7 +75,22 @@ 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(); } From abef580fa9e7b19721d698c7aa2bc0902332257f Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 8 Apr 2026 22:53:07 +0200 Subject: [PATCH 2/4] CVC4: use updated version 1.8.1-8 with disabled finalizers --- build/build-publish-solvers/solver-cvc4.xml | 19 ++----------------- lib/ivy.xml | 2 +- 2 files changed, 3 insertions(+), 18 deletions(-) diff --git a/build/build-publish-solvers/solver-cvc4.xml b/build/build-publish-solvers/solver-cvc4.xml index 99565e6e40..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 --> @@ -75,22 +75,7 @@ SPDX-License-Identifier: Apache-2.0 - - - - - - - - - - - + diff --git a/lib/ivy.xml b/lib/ivy.xml index 7444de2cd9..5ffa856520 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 60e9e983d481fe9c715d32dbb4b10e7ff46c9c99 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 8 Apr 2026 23:29:51 +0200 Subject: [PATCH 3/4] CVC4: use updated version 1.8.1-9 with disabled finalizers --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 5ffa856520..de1cf76154 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 72ac1f499d5bf12c07d703ac1bd8b99852079f28 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 9 Apr 2026 00:45:42 +0200 Subject: [PATCH 4/4] CVC4: use updated version 1.8.1-11 with disabled finalizers --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index de1cf76154..d789da813b 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0 - +