From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 22 Jun 2014 07:01:23 +0000 (-0400)
Subject: QuitCommand needs "success" output for trace executor. :-(
X-Git-Tag: cvc5-1.0.0~6700^2~8
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=933a5122ca26194a557a467a082afdafad917335;p=cvc5.git

QuitCommand needs "success" output for trace executor. :-(
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d9b9694e5..2f75c8887 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -383,11 +383,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         } else {
           Command* copy = cmd->clone();
           allCommands.back().push_back(copy);
+          status = pExecutor->doCommand(cmd);
           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
             delete cmd;
             break;
           }
-          status = pExecutor->doCommand(cmd);
         }
         delete cmd;
       }
@@ -417,11 +417,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         replayParser->useDeclarationsFrom(parser);
       }
       while(status && (cmd = parser->nextCommand())) {
+        status = pExecutor->doCommand(cmd);
         if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
           delete cmd;
           break;
         }
-        status = pExecutor->doCommand(cmd);
         delete cmd;
       }
       // Remove the parser