projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
8c11c5b
)
[proof-new] Activating proofs when dumping proofs (#6155)
author
Haniel Barbosa
<hanielbbarbosa@gmail.com>
Tue, 16 Mar 2021 19:59:03 +0000
(16:59 -0300)
committer
GitHub
<noreply@github.com>
Tue, 16 Mar 2021 19:59:03 +0000
(19:59 +0000)
src/smt/set_defaults.cpp
patch
|
blob
|
history
diff --git
a/src/smt/set_defaults.cpp
b/src/smt/set_defaults.cpp
index f2c6c33873a533263e274550b53d96a01666aa1c..761ff87012e10efcd2453816989b0f84ecaae05c 100644
(file)
--- 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);