From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 30 Sep 2014 23:12:26 +0000 (-0400)
Subject: Fix a command-replay bug in tear-down-incremental mode.  Thanks to Christoph Sticksel... 
X-Git-Tag: cvc5-1.0.0~6509^2~24
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80a57d99aa2b611f41f13b0455d6ee089c165905;p=cvc5.git

Fix a command-replay bug in tear-down-incremental mode.  Thanks to Christoph Sticksel for the report.
---

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;