fix in CommandSequence invoke : maintain success/failure. Fixes bug 465.

(this commit was certified error- and warning-free by the test-and-commit script.)

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() {