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 f60ed925b1b894f4cb0a59bf4ca758e218236be3..4089f4d1b78a7bb076af81fe3d74a380441852ea 100644 (file)
--- 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 718d6cd6d5d5d05ce1b03b8ff6628b9bd93d0699..58ae025b832220a7193ba6ad46f20dc347ce650b 100644 (file)
--- 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