From 8c1138f4a076acdabae18bf3d6d088ac1ab10587 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 16 Mar 2021 16:59:03 -0300 Subject: [PATCH] [proof-new] Activating proofs when dumping proofs (#6155) --- src/smt/set_defaults.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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); -- 2.30.2