Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kfriedberger merged 4 commits into from
Apr 9, 2026
+3 −21
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f6c025d
CVC4: Remove the finalizers
daniel-raffler Apr 6, 2026
abef580
CVC4: use updated version 1.8.1-8 with disabled finalizers
kfriedberger Apr 8, 2026
60e9e98
CVC4: use updated version 1.8.1-9 with disabled finalizers
kfriedberger Apr 8, 2026
72ac1f4
CVC4: use updated version 1.8.1-11 with disabled finalizers
kfriedberger Apr 8, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion build/build-publish-solvers/solver-cvc4.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
-->
Expand Down
2 changes: 1 addition & 1 deletion lib/ivy.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"/>
Expand Down
10 changes: 0 additions & 10 deletions src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -49,10 +43,6 @@ private CVC4SolverContext(
this.creator = creator;
shutdownNotifier = pShutdownNotifier;
randomSeed = pRandomSeed;

synchronized (CVC4SolverContext.class) {
contexts.add(this);
}
}

public static SolverContext create(
Expand Down
10 changes: 1 addition & 9 deletions src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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();
}
Expand Down
Loading