From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 8 Oct 2014 22:52:02 +0000 (-0400)
Subject: Some minor cleanup.
X-Git-Tag: cvc5-1.0.0~6576
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f885c4e79501827e70fe14683152af85c5f8bfd;p=cvc5.git

Some minor cleanup.
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4bbfe2762..52522d591 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -47,7 +47,6 @@ void setNoLimitCPU() {
 #endif /* ! __WIN32__ */
 }
 
-
 void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
 
 CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
@@ -128,17 +127,19 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
         ( res.asSatisfiabilityResult() == Result::SAT ||
           (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
       g = new GetModelCommand();
-    } else if( d_options[options::proof] &&
-               d_options[options::dumpProofs] &&
-               res.asSatisfiabilityResult() == Result::UNSAT ) {
+    }
+    if( d_options[options::proof] &&
+        d_options[options::dumpProofs] &&
+        res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetProofCommand();
-    } else if( d_options[options::dumpInstantiations] &&
-               ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && 
-                   ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || 
-                 res.asSatisfiabilityResult() == Result::UNSAT ) ) {
+    }
+    if( d_options[options::dumpInstantiations] &&
+        ( ( d_options[options::instFormatMode] != INST_FORMAT_MODE_SZS &&
+            ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) ||
+          res.asSatisfiabilityResult() == Result::UNSAT ) ) {
       g = new GetInstantiationsCommand();
-    } else if( d_options[options::dumpUnsatCores] &&
-               res.asSatisfiabilityResult() == Result::UNSAT ) {
+    }
+    if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetUnsatCoreCommand();
     }
     if(g != NULL) {
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 7d35a443a..6e10c9a8a 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -11,7 +11,7 @@
  **
  ** \brief An additional layer between commands and invoking them.
  **
- ** The portfolio executer branches check-sat queries to several
+ ** The portfolio executor branches check-sat queries to several
  ** threads.
  **/