(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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index a79d79e19a4486de5c9cd09d3b358a29a98e72d5..91910da479b1e83eed958998218b2d1f96711d3b 100644 (file)
--- 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"))
   {

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 206b47348aaa8858dc0635b7527c46c62bd60041..75f93af47f45917ef10de5de4fe19d5af161d2e9 100644 (file)
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -422,7 +422,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
            || id == PfRule::THEORY_PREPROCESS_LEMMA
            || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM
            || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE
-           || id == PfRule::TRUST_SUBS || id == PfRule::TRUST_SUBS_MAP)
+           || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS
+           || id == PfRule::TRUST_SUBS_MAP)
   {
     // "trusted" rules
     Assert(children.empty());