From 80a57d99aa2b611f41f13b0455d6ee089c165905 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 30 Sep 2014 19:12:26 -0400
Subject: [PATCH] Fix a command-replay bug in tear-down-incremental mode. 
 Thanks to Christoph Sticksel for the report.

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

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 1202c7882..4787701f5 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -382,8 +382,18 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           status = pExecutor->doCommand(cmd);
           needReset = true;
         } else {
-          Command* copy = cmd->clone();
-          allCommands.back().push_back(copy);
+          // We shouldn't copy certain commands, because they can cause
+          // an error on replay since there's no associated sat/unsat check
+          // preceding them.
+          if(dynamic_cast<GetUnsatCoreCommand*>(cmd) == NULL &&
+             dynamic_cast<GetProofCommand*>(cmd) == NULL &&
+             dynamic_cast<GetValueCommand*>(cmd) == NULL &&
+             dynamic_cast<GetModelCommand*>(cmd) == NULL &&
+             dynamic_cast<GetAssignmentCommand*>(cmd) == NULL &&
+             dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL) {
+            Command* copy = cmd->clone();
+            allCommands.back().push_back(copy);
+          }
           status = pExecutor->doCommand(cmd);
           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
             delete cmd;
-- 
2.30.2