diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-26 00:47:55 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-26 00:50:14 -0400 |
| commit | 4746a045ce8dd0b3155610652e0fcdf341b0f759 (patch) | |
| tree | ac73899544d0860bce688e1ae4b6b7de49cf1812 /src/main/driver_unified.cpp | |
| parent | c5970b88e4334146fe142fa1644a2a36049a6448 (diff) | |
Potential fix for bug 573.
Diffstat (limited to 'src/main/driver_unified.cpp')
| -rw-r--r-- | src/main/driver_unified.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 64e10cc53..6beb9636a 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -338,7 +338,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(parser); } bool needReset = false; - while(status && (cmd = parser->nextCommand())) { + while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { if(dynamic_cast<PushCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); @@ -417,7 +417,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while(status && (cmd = parser->nextCommand())) { + while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { status = pExecutor->doCommand(cmd); if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; |