More application-track fixes for use with trace executor.

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c39627550ffb3a280107758e8bde6ed6a7e99b13..54f6383ac71fe4e5f5845129ab3576a317d3e9cd 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -332,17 +332,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
           if(needReset) {
             pExecutor->reset();
-            bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]);
-            Command::printsuccess::setPrintSuccess(*opts[options::out], false);
-            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();
+                cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
                 delete cmd;
               }
             }
-            Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
             needReset = false;
           }
           *opts[options::out] << CommandSuccess();
@@ -350,36 +347,33 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
           allCommands.pop_back(); // fixme leaks cmds here
           pExecutor->reset();
-          bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]);
-          Command::printsuccess::setPrintSuccess(*opts[options::out], 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();
+              cmd->setMuted(true);
               pExecutor->doCommand(cmd);
               delete cmd;
             }
           }
-          Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
           *opts[options::out] << CommandSuccess();
         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
           if(needReset) {
             pExecutor->reset();
-            bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]);
-            Command::printsuccess::setPrintSuccess(*opts[options::out], 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();
+                cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
                 delete cmd;
               }
             }
-            Command::printsuccess::setPrintSuccess(*opts[options::out], succ);
           }
           status = pExecutor->doCommand(cmd);
           needReset = true;
         } else {
-          allCommands.back().push_back(cmd->clone());
+          Command* copy = cmd->clone();
+          allCommands.back().push_back(copy);
           if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
             delete cmd;
             break;

diff --git a/src/options/base_options b/src/options/base_options
index ee15238c8c526a5c1ad41b6ea8b470be93bf6875..ed94e68f6f659e9a8a3752b7f83cf3fc37306c86 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" :read-write
+option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h"
  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