From 13eac8f6d88071725d3b0e5fe73a29bca86bb9fb Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 11 Jun 2014 19:11:56 -0400 Subject: [PATCH] Flush output stream after result printed in portfolio. --- src/main/command_executor_portfolio.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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? -- 2.30.2