From 551d1d37fe9c8ec25ddeac1e37b68d39158378ea Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 27 Nov 2012 21:31:46 +0000 Subject: [PATCH] fix in CommandSequence invoke : maintain success/failure. Fixes bug 465. (this commit was certified error- and warning-free by the test-and-commit script.) --- src/expr/command.cpp | 8 ++++++++ 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 { -- 2.30.2