Flush output stream after result printed in portfolio.

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index fa1d8c7f5fdd0aae332317f2200896f8382e6caf..1a5d2f8ac74eed65c4bd055b841ac934ded181c3 100644 (file)
--- 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?