diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-03-16 16:59:03 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-16 19:59:03 +0000 |
| commit | 8c1138f4a076acdabae18bf3d6d088ac1ab10587 (patch) | |
| tree | 3f301db87870bae906234068180ced461aa07e6f /src/smt | |
| parent | 8c11c5b2683aa13160447aef302d82115a08081a (diff) | |
[proof-new] Activating proofs when dumping proofs (#6155)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/set_defaults.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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); |