From 4ec5125c8c930c6b0c64d965bbfbe609db693a8f Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 9 Oct 2012 22:23:32 +0000 Subject: [PATCH] bugfix: isQuantified, bugfix: flush --- src/main/command_executor_portfolio.cpp | 4 +++- src/main/driver_unified.cpp | 6 +++++- 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 */ } -- 2.30.2