diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 48dcc17ef..2cdcc344c 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -214,7 +214,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // We currently don't support changing number of threads for each // command, but things have been architected in a way so that this - // can be acheived with not a lot of work + // can be achieved without a lot of work. Command *seqs[d_numThreads]; if(d_lastWinner == 0) @@ -238,7 +238,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) int(i) == d_lastWinner ? cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) : d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); - }catch(ExportUnsupportedException& e){ + } catch(ExportUnsupportedException& e) { if(d_options[options::fallbackSequential]) { Notice() << "Unsupported theory encountered, switching to sequential mode."; return CommandExecutor::doCommandSingleton(cmd); @@ -292,20 +292,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) runPortfolio(d_numThreads, smFn, fns, d_options[options::waitToJoin]); - d_seq = NULL; delete d_seq; d_seq = new CommandSequence(); d_lastWinner = portfolioReturn.first; - - CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd); - if(cs != NULL) { - d_result = cs->getResult(); - } - QueryCommand* q = dynamic_cast<QueryCommand*>(cmd); - if(q != NULL) { - d_result = q->getResult(); - } + d_result = d_smts[d_lastWinner]->getStatusOfLastCommand(); if(d_ostringstreams.size() != 0) { assert(d_numThreads == d_options[options::threads]); |