From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 26 Jun 2014 04:47:55 +0000 (-0400)
Subject: Potential fix for bug 573.
X-Git-Tag: cvc5-1.0.0~6718^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4746a045ce8dd0b3155610652e0fcdf341b0f759;p=cvc5.git

Potential fix for bug 573.
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5dc10a473..028a23f01 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -69,7 +69,7 @@ bool CommandExecutor::doCommand(Command* cmd)
     bool status = true;
 
     for(CommandSequence::iterator subcmd = seq->begin();
-        status && subcmd != seq->end();
+        (status || d_options[options::continuedExecution]) && subcmd != seq->end();
         ++subcmd) {
       status = doCommand(*subcmd);
     }
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;