diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-30 19:12:26 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-30 19:12:31 -0400 |
commit | 80a57d99aa2b611f41f13b0455d6ee089c165905 (patch) | |
tree | d4a5113aba347c72af4e58678b4cb5f77d91d48d /src/main | |
parent | 892dd18267c137f7797a4c97f7068b587cbf8c3a (diff) |
Fix a command-replay bug in tear-down-incremental mode. Thanks to Christoph Sticksel for the report.
Diffstat (limited to 'src/main')
-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; |