From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 9 Oct 2012 22:23:32 +0000 (+0000)
Subject: bugfix: isQuantified, bugfix: flush
X-Git-Tag: cvc5-1.0.0~7713
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4ec5125c8c930c6b0c64d965bbfbe609db693a8f;p=cvc5.git

bugfix: isQuantified, bugfix: flush
---

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 00527702e..5461170e6 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -194,7 +194,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
   } else if(mode == 1) {               // portfolio
 
     // If quantified, stay sequential
-    if(d_smts[0]->getLogicInfo().isQuantified()) {
+    LogicInfo logicInfo = d_smts[0]->getLogicInfo();
+    logicInfo.lock();
+    if(logicInfo.isQuantified()) {
       return CommandExecutor::doCommandSingleton(cmd);
     }
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d2adf97c4..7c2b7b89e 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -318,13 +318,17 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       *opts[options::replayLog] << flush;
     }
 
+    // make sure out and err streams are flushed too
+    *opts[options::out] << flush;
+    *opts[options::err] << flush;
+ 
 #ifdef CVC4_DEBUG
     if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
       _exit(returnValue);
     }
 #else /* CVC4_DEBUG */
     if(opts[options::earlyExit]) {
-      _exit(returnValue);
+     _exit(returnValue);
     }
 #endif /* CVC4_DEBUG */
   }