diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-09 13:02:14 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-09 13:02:14 -0600 |
| commit | b384526f32eab67bce49c26e38d9bd7d8b1baca0 (patch) | |
| tree | 1c35fc83c23f11928ef6be32cb493237730568ea /src/smt | |
| parent | 1b180f87266ffa206da1d5b772816b80e7f97c14 (diff) | |
(proof-new) Minor fix and allow proof option (#6085)
This is in preparation for enabling CI / proofs on master.
This does not throw an option exception when proofs are enabled, it also makes a fix that was missing on master and needed for regressions to pass on master.
This is partially taken from #5980.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/set_defaults.cpp | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index a79d79e19..91910da47 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -72,8 +72,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Notice() << "SmtEngine: setting unsatCores" << std::endl; options::unsatCores.set(true); } - if (options::checkUnsatCoresNew()) + if (options::checkProofs() || options::checkUnsatCoresNew()) { + Notice() << "SmtEngine: setting proof" << std::endl; options::proof.set(true); } if (options::bitvectorAigSimplifications.wasSetByUser()) @@ -310,7 +311,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || options::produceAbducts() || options::produceInterpols() != options::ProduceInterpols::NONE || options::modelCoresMode() != options::ModelCoresMode::NONE - || options::blockModelsMode() != options::BlockModelsMode::NONE) + || options::blockModelsMode() != options::BlockModelsMode::NONE + || options::proof()) && !options::produceAssertions()) { Notice() << "SmtEngine: turning on produce-assertions to support " @@ -1375,11 +1377,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) "division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); } - // !!!!!!!!!!!!!!!! temporary, until proofs are functional - if (options::proof()) - { - throw OptionException("--proof is not yet supported."); - } if (logic == LogicInfo("QF_UFNRA")) { |