Potential fix for bug 573.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5dc10a4739a8ef088d24ce943e6276e3ebbcd95a..028a23f01f8b8b07e4aabea1738fb18d563dbda9 100644 (file)
--- 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 64e10cc531f8a0736eae71199396bac06aaf7623..6beb9636a558665590dcf7643d5d02c8f987bc6c 100644 (file)
--- 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;