Some minor cleanup.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4bbfe27629b1b2a2a5d7cc7a89e388f6d4b114cf..52522d59139698cec4ed793d0e30dbf6b1d9392a 100644 (file)
--- 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 7d35a443af63d0277d5208e61487f976b6621535..6e10c9a8a8db22a998b554c5775b7486bf5ce439 100644 (file)
--- 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.
  **/