From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 16 Mar 2021 19:59:03 +0000 (-0300)
Subject: [proof-new] Activating proofs when dumping proofs (#6155)
X-Git-Tag: cvc5-1.0.0~2067
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c1138f4a076acdabae18bf3d6d088ac1ab10587;p=cvc5.git

[proof-new] Activating proofs when dumping proofs (#6155)
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index f2c6c3387..761ff8701 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -72,7 +72,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Notice() << "SmtEngine: setting unsatCores" << std::endl;
     options::unsatCores.set(true);
   }
-  if (options::checkProofs() || options::checkUnsatCoresNew())
+  if (options::checkProofs() || options::checkUnsatCoresNew()
+      || options::dumpProofs())
   {
     Notice() << "SmtEngine: setting proof" << std::endl;
     options::produceProofs.set(true);