4 files changed, 38 insertions, 29 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 556e51216..9ee896107 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -24,11 +24,12 @@
 namespace CVC4 {
 namespace main {
 
-CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options):
+CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
   d_exprMgr(exprMgr),
   d_smtEngine(SmtEngine(&exprMgr)),
   d_options(options),
-  d_stats("driver") {
+  d_stats("driver"),
+  d_result() {
 }
 
 bool CommandExecutor::doCommand(Command* cmd)
@@ -58,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd)
   }
 }
 
-bool CommandExecutor::doCommandSingleton(Command *cmd)
+bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options[options::verbosity] >= -1) {
@@ -66,25 +67,27 @@ bool CommandExecutor::doCommandSingleton(Command *cmd)
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
   }
-  //dump the model if option is set
-  if(status && d_options[options::produceModels] && d_options[options::dumpModels]) {
-    CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd);
-    if(cs != NULL) {
-      if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT ||
-         (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){
-        Command * gm = new GetModelCommand;
-        status = doCommandSingleton(gm);
-      }
-    }
+  Result res;
+  CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+  if(cs != NULL) {
+    d_result = res = cs->getResult();
+  }
+  QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+  if(q != NULL) {
+    d_result = res = q->getResult();
+  }
+  // dump the model if option is set
+  if( status &&
+      d_options[options::produceModels] &&
+      d_options[options::dumpModels] &&
+      ( res.asSatisfiabilityResult() == Result::SAT ||
+        (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+    Command* gm = new GetModelCommand();
+    status = doCommandSingleton(gm);
   }
   return status;
 }
 
-std::string CommandExecutor::getSmtEngineStatus()
-{
-  return d_smtEngine.getInfo("status").getValue();
-}
-
 bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
 {
   if(out == NULL) {
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index f1b8d8f2f..cbc71b075 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -34,6 +34,7 @@ protected:
   SmtEngine d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
+  Result d_result;
 
 public:
   CommandExecutor(ExprManager &exprMgr, Options &options);
@@ -47,7 +48,7 @@ public:
    */
   bool doCommand(CVC4::Command* cmd);
 
-  virtual std::string getSmtEngineStatus();
+  Result getResult() const { return d_result; }
 
   StatisticsRegistry& getStatisticsRegistry() {
     return d_stats;
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 63f689d48..2dfd5e6bd 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -184,7 +184,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
   // command
 
   if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
-    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+     dynamic_cast<QueryCommand*>(cmd) != NULL) {
     mode = 1;
   } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
@@ -298,6 +298,16 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     d_lastWinner = portfolioReturn.first;
 
+    CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+    if(cs != NULL) {
+      d_result = cs->getResult();
+    }
+    QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+    if(q != NULL) {
+      d_result = q->getResult();
+    }
+    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+
     if(d_ostringstreams.size() != 0) {
       assert(d_numThreads == d_options[options::threads]);
       assert(portfolioReturn.first >= 0);
@@ -340,11 +350,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
 }/* CommandExecutorPortfolio::doCommandSingleton() */
 
-std::string CommandExecutorPortfolio::getSmtEngineStatus()
-{
-  return d_smts[d_lastWinner]->getInfo("status").getValue();
-}
-
 void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
   assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
   for(size_t i = 0; i < d_numThreads; ++i) {
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f57d4f2d7..20a989106 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -297,13 +297,13 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       opts.set(options::replayStream, NULL);
     }
 
-    string result = "unknown";
+    Result result;
     if(status) {
-      result = pExecutor->getSmtEngineStatus();
+      result = pExecutor->getResult();
 
-      if(result == "sat") {
+      if(result.asSatisfiabilityResult() == Result::SAT) {
         returnValue = 10;
-      } else if(result == "unsat") {
+      } else if(result.asSatisfiabilityResult() == Result::UNSAT) {
         returnValue = 20;
       } else {
         returnValue = 0;