From 1a9736b35db944f73a95bf98d800ebae8e435a92 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 15 Jun 2014 20:16:35 -0400
Subject: [PATCH] Careful there aren't too many "success" messages with
 --tear-down-incremental (can confuse trace runner).

---
 src/main/driver_unified.cpp | 9 +++++++++
 src/options/base_options    | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

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
-- 
2.30.2