From 933a5122ca26194a557a467a082afdafad917335 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 22 Jun 2014 03:01:23 -0400
Subject: [PATCH] QuitCommand needs "success" output for trace executor. :-(

---
 src/main/driver_unified.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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
-- 
2.30.2