Skip to content

Commit 010ddc2

Browse files
Remove use of "synchornized" in Mathsat5AbstractProver. Mathsat only support one thread per ProverEnvironment anyway.
1 parent 389af9f commit 010ddc2

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

+3-3
Original file line numberDiff line numberDiff line change
@@ -112,13 +112,13 @@ private <T> T exec(Callable<T> closure) throws SolverException, InterruptedExcep
112112
}
113113

114114
@Override
115-
public synchronized boolean isUnsat() throws InterruptedException, SolverException {
115+
public boolean isUnsat() throws InterruptedException, SolverException {
116116
Preconditions.checkState(!closed);
117117
return exec(() -> !msat_check_sat(curEnv));
118118
}
119119

120120
@Override
121-
public synchronized boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
121+
public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
122122
throws SolverException, InterruptedException {
123123
Preconditions.checkState(!closed);
124124
checkForLiterals(pAssumptions);
@@ -238,7 +238,7 @@ protected boolean isClosed() {
238238
}
239239

240240
@Override
241-
public synchronized <T> T allSat(AllSatCallback<T> callback, List<BooleanFormula> important)
241+
public <T> T allSat(AllSatCallback<T> callback, List<BooleanFormula> important)
242242
throws InterruptedException, SolverException {
243243
Preconditions.checkState(!closed);
244244
checkGenerateAllSat();

0 commit comments

Comments
 (0)