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

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

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8ded902b7a367baba8cc37eb41e4ad9e9ea976dc..fa2a8d1f2fa4fc4661d96ad4e1e3735e77c20003 100644 (file)
--- 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 e6ff1945141cf0d9905bf1a178e71fe9864b372b..5953373ff9f9543e4833e5c2e92a3b43282f6871 100644 (file)
--- 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 {