diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 68e5717291..5facef977b 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -112,13 +112,13 @@ private T exec(Callable closure) throws SolverException, InterruptedExcep } @Override - public synchronized boolean isUnsat() throws InterruptedException, SolverException { + public boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); return exec(() -> !msat_check_sat(curEnv)); } @Override - public synchronized boolean isUnsatWithAssumptions(Collection pAssumptions) + public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); checkForLiterals(pAssumptions); @@ -238,7 +238,7 @@ protected boolean isClosed() { } @Override - public synchronized T allSat(AllSatCallback callback, List important) + public T allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { Preconditions.checkState(!closed); checkGenerateAllSat();