Skip to content

Commit 19372c0

Browse files
author
BaierD
committed
Add CVC4 implementation for prover based shutdown
1 parent e5ca134 commit 19372c0

File tree

1 file changed

+10
-3
lines changed

1 file changed

+10
-3
lines changed

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@
2424
import java.util.Optional;
2525
import java.util.Set;
2626
import org.checkerframework.checker.nullness.qual.Nullable;
27+
import org.sosy_lab.common.ShutdownManager;
2728
import org.sosy_lab.common.ShutdownNotifier;
2829
import org.sosy_lab.java_smt.api.BasicProverEnvironment;
2930
import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -202,11 +203,12 @@ public boolean isUnsat() throws InterruptedException, SolverException {
202203
}
203204

204205
Result result;
205-
try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, smtEngine::interrupt)) {
206-
shutdownNotifier.shutdownIfNecessary();
206+
try (ShutdownHook hook =
207+
new ShutdownHook(proverShutdownManager.getNotifier(), smtEngine::interrupt)) {
208+
proverShutdownManager.getNotifier().shutdownIfNecessary();
207209
result = smtEngine.checkSat();
208210
}
209-
shutdownNotifier.shutdownIfNecessary();
211+
proverShutdownManager.getNotifier().shutdownIfNecessary();
210212
return convertSatResult(result);
211213
}
212214

@@ -260,4 +262,9 @@ public void close() {
260262
}
261263
super.close();
262264
}
265+
266+
@Override
267+
protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
268+
return proverShutdownManager;
269+
}
263270
}

0 commit comments

Comments
 (0)