Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.

2 files changed, 13 insertions, 16 deletions

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 0e71e1539..45ee52121 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -123,17 +123,14 @@ void CommandExecutorPortfolio::lemmaSharingInit()
     }
 
     /* Output to string stream  */
-    if(d_options[options::verbosity] == 0
-       || d_options[options::separateOutput]) {
-      assert(d_ostringstreams.size() == 0);
-      for(unsigned i = 0; i < d_numThreads; ++i) {
-        d_ostringstreams.push_back(new ostringstream);
-        d_threadOptions[i].set(options::out, d_ostringstreams[i]);
-
-        // important even for muzzled builds (to get result output right)
-        *d_threadOptions[i][options::out]
-          << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
-      }
+    assert(d_ostringstreams.size() == 0);
+    for(unsigned i = 0; i < d_numThreads; ++i) {
+      d_ostringstreams.push_back(new ostringstream);
+      d_threadOptions[i].set(options::out, d_ostringstreams[i]);
+
+      // important even for muzzled builds (to get result output right)
+      *d_threadOptions[i][options::out]
+        << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
     }
   }
 }/* CommandExecutorPortfolio::lemmaSharingInit() */
@@ -208,7 +205,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
     bool ret = smtEngineInvoke(d_smts[d_lastWinner],
                                cmdExported,
-                               d_threadOptions[d_lastWinner][options::out]);
+                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else if(mode == 1) {               // portfolio
@@ -274,7 +271,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       fns[i] = boost::bind(smtEngineInvoke,
                            d_smts[i],
                            seqs[i],
-                           d_threadOptions[i][options::out]
+                           d_options[options::verbosity] >= -1 ? d_threadOptions[i][options::out] : NULL
                            );
     }
 
@@ -332,7 +329,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
     bool ret = smtEngineInvoke(d_smts[d_lastWinner],
                                cmdExported,
-                               d_threadOptions[d_lastWinner][options::out]);
+                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else {
diff --git a/src/main/options b/src/main/options
index caea63f5a..9c630270f 100644
--- a/src/main/options
+++ b/src/main/options
@@ -31,8 +31,8 @@ option threadArgv std::vector<std::string> :include <vector> <string>
  Thread configuration (a string to be passed to parseOptions)
 option thread_id int :default -1
  Thread ID, for internal use in case of multi-threaded run
-option separateOutput bool :default false
- In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
+#option separateOutput bool :default false
+# In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
 option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
  don't share (among portfolio threads) lemmas strictly longer than N
 option fallbackSequential  --fallback-sequential bool :default false