diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-09 22:23:32 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-09 22:23:32 +0000 |
commit | 4ec5125c8c930c6b0c64d965bbfbe609db693a8f (patch) | |
tree | e28dc6494864e33c991d2c1584f2c6e51e0db9f9 /src | |
parent | a957f6f97f2e83d29f6c5d66f01e40f588ad95c5 (diff) |
bugfix: isQuantified, bugfix: flush
Diffstat (limited to 'src')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 4 | ||||
-rw-r--r-- | 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 */ } |