bugfix: isQuantified, bugfix: flush

2 files changed, 8 insertions, 2 deletions

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 */
   }