From bc61a1d1b0fa893ecfb4f62557916357773b5987 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 4 Jan 2022 15:50:17 -0600 Subject: [PATCH] Fix proofs for datatype purify (#7841) Previously we were failing to produce proofs for purification lemmas (= t witness_form(t)) from datatypes. --- src/theory/datatypes/infer_proof_cons.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 4ed6e3da9..d2e4947bb 100644 --- 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 3f13886ed..f413015c4 100644 --- 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; -- 2.30.2