some portfolio driver cleanup

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 48dcc17ef409e267ef834d0e89da856f8fb362fa..2cdcc344cfbc0d426cf234a3c76d05fe00c7df68 100644 (file)
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -214,7 +214,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     // We currently don't support changing number of threads for each
     // command, but things have been architected in a way so that this
-    // can be acheived with not a lot of work
+    // can be achieved without a lot of work.
     Command *seqs[d_numThreads];
 
     if(d_lastWinner == 0)
@@ -238,7 +238,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
           int(i) == d_lastWinner ?
           cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) :
           d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
-      }catch(ExportUnsupportedException& e){
+      } catch(ExportUnsupportedException& e) {
         if(d_options[options::fallbackSequential]) {
           Notice() << "Unsupported theory encountered, switching to sequential mode.";
           return CommandExecutor::doCommandSingleton(cmd);
@@ -292,20 +292,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
         runPortfolio(d_numThreads, smFn, fns,
                      d_options[options::waitToJoin]);
 
-    d_seq = NULL;
     delete d_seq;
     d_seq = new CommandSequence();
 
     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();
-    }
+    d_result = d_smts[d_lastWinner]->getStatusOfLastCommand();
 
     if(d_ostringstreams.size() != 0) {
       assert(d_numThreads == d_options[options::threads]);