diff options
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 14 |
1 files 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; |