From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 12 Mar 2021 18:03:41 +0000 (-0300)
Subject: [proof-new] Fix arity check when building equality engine proofs  (#6133)
X-Git-Tag: cvc5-1.0.0~2089
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b4c45340a74a8e2419667d403cd1fde9c7664fd;p=cvc5.git

[proof-new] Fix arity check when building equality engine proofs  (#6133)

Broken in dc679ed.
---

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 1c5419977..8b44cc4d9 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1076,7 +1076,7 @@ void EqualityEngine::buildEqConclusion(EqualityNodeId id1,
         << id2 << "} " << d_nodes[id2] << "\n";
     // if has at least as many children as the minimal
     // number of children of the n-ary kind, build the node
-    if (numChildren >= kind::metakind::getMaxArityForKind(k1))
+    if (numChildren >= kind::metakind::getMinArityForKind(k1))
     {
       std::vector<Node> children;
       for (unsigned j = 0; j < numChildren; ++j)