some changes to make CVC4 work nicely with trace executor for application track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.

2 files changed, 10 insertions, 0 deletions

diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index 00072d6d9..5ecfed3a6 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -242,6 +242,9 @@ int runCvc4(int argc, char* argv[], Options& options) {
     *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
   }
 
+  // important even for muzzled builds (to get result output right)
+  *options.out << Expr::setlanguage(options.outputLanguage);
+
   // Parse and execute commands until we are done
   Command* cmd;
   bool status = true;
@@ -281,6 +284,10 @@ int runCvc4(int argc, char* argv[], Options& options) {
       replayParser->useDeclarationsFrom(parser);
     }
     while((cmd = parser->nextCommand())) {
+      if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+        delete cmd;
+        break;
+      }
       status = doCommand(smt, cmd, options) && status;
       delete cmd;
     }
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 1908d3e90..7972cd94d 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -301,6 +301,9 @@ int runCvc4(int argc, char *argv[], Options& options) {
                      << Expr::printtypes(false);
   }
 
+  // important even for muzzled builds (to get result output right)
+  *options.out << Expr::setlanguage(options.outputLanguage);
+
   vector<Options> threadOptions;
   for(int i = 0; i < numThreads; ++i) {
     threadOptions.push_back(options);