diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main/command_executor.cpp | 3 | ||||
| -rw-r--r-- | src/smt/proof_manager.cpp | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index f60ed925b..4089f4d1b 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -158,12 +158,13 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) } bool isResultUnsat = res.isUnsat() || res.isEntailed(); + bool isResultSat = res.isSat() || res.isNotEntailed(); // dump the model/proof/unsat core if option is set if (status) { std::vector<std::unique_ptr<Command> > getterCommands; if (d_solver->getOptions().driver.dumpModels - && (res.isSat() + && (isResultSat || (res.isSatUnknown() && res.getUnknownExplanation() == api::Result::INCOMPLETE))) { diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 718d6cd6d..58ae025b8 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -163,7 +163,7 @@ void PfManager::printProof(std::ostream& out, { out << "% SZS output start Proof for " << d_env.getFilename() << std::endl; // TODO (proj #37) print in TPTP compliant format - out << *fp; + out << *fp << std::endl; out << "% SZS output end Proof for " << d_env.getFilename() << std::endl; } else |