Fix eq proof conversion for constant merged parameterized ops (#6926)

This issue arises when using the central equality engine on several regressions.

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 6b2fae389994a6d51d20c7a19dc2a410828e6ecb..27b61e87d09fe7145c45d65632d317d9b5399aae 100644 (file)
--- 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};