diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-11 19:11:56 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-11 19:11:56 -0400 |
commit | 13eac8f6d88071725d3b0e5fe73a29bca86bb9fb (patch) | |
tree | 7a83286916f8c5c5113149f41a81c4d7c339c4ce /src | |
parent | bc2d62fd104deaaff3474385ef76b5c057192da1 (diff) |
Flush output stream after result printed in portfolio.
Diffstat (limited to 'src')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index fa1d8c7f5..1a5d2f8ac 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -337,7 +337,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) } *d_options[options::out] - << d_ostringstreams[portfolioReturn.first]->str(); + << d_ostringstreams[portfolioReturn.first]->str() + << std::flush; #ifdef CVC4_COMPETITION_MODE // There's some hang-up in thread destruction? |