diff options
| -rw-r--r-- | src/main/command_executor.cpp | 21 | ||||
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 2 |
2 files changed, 12 insertions, 11 deletions
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. **/ |