[proof-new] Activating proofs when dumping proofs (#6155)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 16 Mar 2021 19:59:03 +0000 (16:59 -0300)
committerGitHub <noreply@github.com>
Tue, 16 Mar 2021 19:59:03 +0000 (19:59 +0000)
src/smt/set_defaults.cpp

index f2c6c33873a533263e274550b53d96a01666aa1c..761ff87012e10efcd2453816989b0f84ecaae05c 100644 (file)
@@ -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);