From 6cf3a69a9afd68922d67941c6fd2b877df45ecb9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 26 Aug 2021 11:32:09 -0500 Subject: [PATCH] Dump models for isNotEntailed results (#7071) This fixes a minor issue where models should be dumped for "not entailed" results. This fix was required when preparing the submission to CASC this year. --- src/main/command_executor.cpp | 3 ++- 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 > 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 -- 2.30.2