summaryrefslogtreecommitdiff
path: root/src/prop/prop_engine.cpp
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2012-09-08 14:25:25 +0000
committerKshitij Bansal <kshitij@cs.nyu.edu>2012-09-08 14:25:25 +0000
commitcfa9e2cbbdf77a325791b5548b41093a0781311c (patch)
treee843d38afe4b197a2dd81316998477cedac26c52 /src/prop/prop_engine.cpp
parent6935324f45bd7f2c735ca4120a9e800ef8903442 (diff)
Single driver for both sequential and portfolio
A "command executer" layer between parsing commands and invoking them. New implementation of portfolio driver splits only when check-sat or query command is encountered, and then switches back to sequential till the next one. As side effect, restores functionality of interactive mode and push/pops.
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r--src/prop/prop_engine.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 54309cd01..281645317 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -271,6 +271,7 @@ bool PropEngine::isRunning() const {
void PropEngine::interrupt() throw(ModalException) {
if(! d_inCheckSat) {
+ return;
throw ModalException("SAT solver is not currently solving anything; "
"cannot interrupt it");
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback