diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-27 21:31:46 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-27 21:31:46 +0000 |
| commit | 551d1d37fe9c8ec25ddeac1e37b68d39158378ea (patch) | |
| tree | 5507dd24bfb94349bdaf6ad9afb7dd5c44d3455c | |
| parent | 49da3204bbb10fbcd87923428f3b476ba5b57af6 (diff) | |
fix in CommandSequence invoke : maintain success/failure. Fixes bug 465.
(this commit was certified error- and warning-free by the test-and-commit script.)
| -rw-r--r-- | src/expr/command.cpp | 8 | ||||
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 12 |
2 files changed, 14 insertions, 6 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8ded902b7..fa2a8d1f2 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -407,8 +407,16 @@ void CommandSequence::invoke(SmtEngine* smtEngine) throw() { void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { for(; d_index < d_commandSequence.size(); ++d_index) { d_commandSequence[d_index]->invoke(smtEngine, out); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } delete d_commandSequence[d_index]; } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); } CommandSequence::const_iterator CommandSequence::begin() const throw() { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index e6ff19451..5953373ff 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -198,9 +198,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) Command* cmdExported = d_lastWinner == 0 ? cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); - int ret = smtEngineInvoke(d_smts[d_lastWinner], - cmdExported, - d_threadOptions[d_lastWinner][options::out]); + bool ret = smtEngineInvoke(d_smts[d_lastWinner], + cmdExported, + d_threadOptions[d_lastWinner][options::out]); if(d_lastWinner != 0) delete cmdExported; return ret; } else if(mode == 1) { // portfolio @@ -310,9 +310,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) Command* cmdExported = d_lastWinner == 0 ? cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); - int ret = smtEngineInvoke(d_smts[d_lastWinner], - cmdExported, - d_threadOptions[d_lastWinner][options::out]); + bool ret = smtEngineInvoke(d_smts[d_lastWinner], + cmdExported, + d_threadOptions[d_lastWinner][options::out]); if(d_lastWinner != 0) delete cmdExported; return ret; } else { |