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 /src/expr | |
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.)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 8 |
1 files changed, 8 insertions, 0 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() { |