diff options
| -rw-r--r-- | src/theory/uf/eq_proof.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 6b2fae389..27b61e87d 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -1049,6 +1049,13 @@ Node EqProof::addToProof(CDProof* p, } // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c) Kind k = d_node[0].getKind(); + std::vector<Node> cargs; + cargs.push_back(ProofRuleChecker::mkKindNode(k)); + if (d_node[0].getMetaKind() == kind::metakind::PARAMETERIZED) + { + constChildren.insert(constChildren.begin(), d_node[0].getOperator()); + cargs.push_back(d_node[0].getOperator()); + } Node constApp = NodeManager::currentNM()->mkNode(k, constChildren); Node constEquality = constApp.eqNode(d_node[1]); Trace("eqproof-conv") << "EqProof::addToProof: adding " @@ -1060,11 +1067,7 @@ Node EqProof::addToProof(CDProof* p, Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::CONG << " step for " << congConclusion << " from " << subChildren << "\n"; - p->addStep(congConclusion, - PfRule::CONG, - {subChildren}, - {ProofRuleChecker::mkKindNode(k)}, - true); + p->addStep(congConclusion, PfRule::CONG, {subChildren}, cargs, true); Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::TRANS << " step for original conclusion " << d_node << "\n"; std::vector<Node> transitivityChildren{congConclusion, constEquality}; |