From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 5 Dec 2011 21:11:19 +0000 (+0000)
Subject: change short-circuiting behavior of Command execution in the main driver; allows... 
X-Git-Tag: cvc5-1.0.0~8367
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c232c1054d0635f4fcd136c3cb2038fa57538e6b;p=cvc5.git

change short-circuiting behavior of Command execution in the main driver; allows a (limited) form of error recovery, matching what we had previously
---

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 76ca7a925..df9063808 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -294,7 +294,7 @@ static int runCvc4(int argc, char* argv[]) {
       replayParser->useDeclarationsFrom(shell.getParser());
     }
     while((cmd = shell.readCommand())) {
-      status = status && doCommand(smt, cmd);
+      status = doCommand(smt, cmd) && status;
       delete cmd;
     }
   } else {
@@ -310,7 +310,7 @@ static int runCvc4(int argc, char* argv[]) {
       replayParser->useDeclarationsFrom(parser);
     }
     while((cmd = parser->nextCommand())) {
-      status = status && doCommand(smt, cmd);
+      status = doCommand(smt, cmd) && status;
       delete cmd;
     }
     // Remove the parser
@@ -370,7 +370,7 @@ static bool doCommand(SmtEngine& smt, Command* cmd) {
     for(CommandSequence::iterator subcmd = seq->begin();
         subcmd != seq->end();
         ++subcmd) {
-      status = status && doCommand(smt, *subcmd);
+      status = doCommand(smt, *subcmd) && status;
     }
   } else {
     if(options.verbosity > 0) {