bugfix: isQuantified, bugfix: flush

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 00527702e70643b4963e7101d0214f3f0a364002..5461170e635b19cc7de9323532dcaf32a089ecbe 100644 (file)
--- 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 d2adf97c443d199e875356204ce57c64c07f3430..7c2b7b89e91f4b9efa6e88efb356a98687502f97 100644 (file)
--- 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 */
   }