Careful there aren't too many "success" messages with --tear-down-incremental (can...

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 4c33088d436dba035c998aa0406f324c27f3c54c..9215c607376df74514b1a1b39caa43185957c125 100644 (file)
--- 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 ed94e68f6f659e9a8a3752b7f83cf3fc37306c86..ee15238c8c526a5c1ad41b6ea8b470be93bf6875 100644 (file)
--- 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