From d08985731908d798ec5dbf8c4b1529266798a68e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 23 Mar 2013 21:38:55 -0400 Subject: [PATCH] Fix bug in portfolio executor output; fixes nightly portfolio-checking runs. --- src/main/command_executor_portfolio.cpp | 25 +++++++++++-------------- src/main/options | 4 ++-- 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 :include 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 -- 2.30.2