Skip to content

Commit e5ca134

Browse files
author
BaierD
committed
Add OpenSMT2 implementation for prover based shutdown
1 parent b5105a2 commit e5ca134

File tree

1 file changed

+10
-3
lines changed

1 file changed

+10
-3
lines changed

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020
import java.util.Optional;
2121
import java.util.Set;
2222
import org.checkerframework.checker.nullness.qual.Nullable;
23+
import org.sosy_lab.common.ShutdownManager;
2324
import org.sosy_lab.common.ShutdownNotifier;
2425
import org.sosy_lab.java_smt.api.BooleanFormula;
2526
import org.sosy_lab.java_smt.api.Evaluator;
@@ -230,8 +231,9 @@ public boolean isUnsat() throws InterruptedException, SolverException {
230231
changedSinceLastSatQuery = false;
231232

232233
sstat result;
233-
try (ShutdownHook listener = new ShutdownHook(shutdownNotifier, osmtSolver::stop)) {
234-
shutdownNotifier.shutdownIfNecessary();
234+
try (ShutdownHook listener =
235+
new ShutdownHook(proverShutdownManager.getNotifier(), osmtSolver::stop)) {
236+
proverShutdownManager.getNotifier().shutdownIfNecessary();
235237
try {
236238
result = osmtSolver.check();
237239
} catch (Exception e) {
@@ -250,7 +252,7 @@ public boolean isUnsat() throws InterruptedException, SolverException {
250252
throw new SolverException("OpenSMT crashed while checking satisfiability.", e);
251253
}
252254
}
253-
shutdownNotifier.shutdownIfNecessary();
255+
proverShutdownManager.getNotifier().shutdownIfNecessary();
254256
}
255257

256258
if (result.equals(sstat.Error())) {
@@ -289,4 +291,9 @@ public void close() {
289291
}
290292
super.close();
291293
}
294+
295+
@Override
296+
protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
297+
return proverShutdownManager;
298+
}
292299
}

0 commit comments

Comments
 (0)