diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-30 19:14:53 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-30 19:14:53 -0400 |
| commit | 230dbc7f55e8f5e4e47b6110b7927e601cf8c078 (patch) | |
| tree | a4aefcc46a308ca25d2758bd35677cdc8d44fe22 /src/main | |
| parent | 7edd9eb6ecf8d36beea059a62ce573fdb6a6f8a1 (diff) | |
| parent | c9ed87b4c415a5c6c1bd6f8b3c93a02a47179365 (diff) | |
Merge branch '1.4.x'
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/driver_unified.cpp | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index bf297ad9e..5fbd5aff5 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -40,7 +40,6 @@ # endif #include "main/options.h" #include "smt/options.h" -#include "theory/uf/options.h" #include "util/output.h" #include "util/result.h" #include "util/statistics_registry.h" @@ -375,8 +374,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; |