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

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 1202c7882bd52b893ec2282c8119c9abd7ec85d2..4787701f550d5e2f7315c67abb40be4df5cd76a6 100644 (file)
--- 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;