Fix proofs for datatype purify (#7841)

Previously we were failing to produce proofs for purification lemmas (= t witness_form(t)) from datatypes.

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 4ed6e3da94ebd26acb0f715b0ed31557622502df..d2e4947bba15602a65c856dfbdc64246520ec5a2 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -233,7 +233,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
     break;
     case InferenceId::DATATYPES_PURIFY:
     {
-      cdp->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {}, {});
+      cdp->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {}, {conc});
       success = true;
     }
     break;

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 3f13886ed1d2adfcf0791160cb52677cc777abc4..f413015c4c8b1379ffb99ab2876983635d176335 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -765,7 +765,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
       d_term_sk[n] = k;
       Node eq = k.eqNode( n );
       Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
-      d_im.addPendingLemma(eq, InferenceId::DATATYPES_PURIFY);
+      d_im.addPendingInference(eq, InferenceId::DATATYPES_PURIFY, d_true, true);
       return k;
     }else{
       return (*it).second;