diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main/driver_unified.cpp | 9 | ||||
| -rw-r--r-- | src/options/base_options | 2 |
2 files changed, 10 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 4c33088d4..9215c6073 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -338,6 +338,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(dynamic_cast<PushCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); + bool succ = opts[options::printSuccess]; + opts.set(options::printSuccess, false); for(size_t i = 0; i < allCommands.size(); ++i) { for(size_t j = 0; j < allCommands[i].size(); ++j) { Command* cmd = allCommands[i][j]->clone(); @@ -345,12 +347,15 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } } + opts.set(options::printSuccess, succ); needReset = false; } allCommands.push_back(vector<Command*>()); } else if(dynamic_cast<PopCommand*>(cmd) != NULL) { allCommands.pop_back(); // fixme leaks cmds here pExecutor->reset(); + bool succ = opts[options::printSuccess]; + opts.set(options::printSuccess, false); for(size_t i = 0; i < allCommands.size(); ++i) { for(size_t j = 0; j < allCommands[i].size(); ++j) { Command* cmd = allCommands[i][j]->clone(); @@ -358,10 +363,13 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } } + opts.set(options::printSuccess, succ); } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || dynamic_cast<QueryCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); + bool succ = opts[options::printSuccess]; + opts.set(options::printSuccess, false); for(size_t i = 0; i < allCommands.size(); ++i) { for(size_t j = 0; j < allCommands[i].size(); ++j) { Command* cmd = allCommands[i][j]->clone(); @@ -369,6 +377,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } } + opts.set(options::printSuccess, succ); } status = pExecutor->doCommand(cmd); needReset = true; diff --git a/src/options/base_options b/src/options/base_options index ed94e68f6..ee15238c8 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -128,7 +128,7 @@ option - trace -t --trace=TAG argument :handler CVC4::options::addTraceTag option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag debug something (e.g. -d arith), can repeat -option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" +option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" :read-write print the "success" output required of SMT-LIBv2 alias --smtlib-strict = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values |