From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 26 Aug 2021 16:32:09 +0000 (-0500)
Subject: Dump models for isNotEntailed results (#7071)
X-Git-Tag: cvc5-1.0.0~1332
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6cf3a69a9afd68922d67941c6fd2b877df45ecb9;p=cvc5.git

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.
---

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