Ensure ext rewrites for associative ops dont throw assertions for kind arities (#3681)

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 05e789ce2..9e924f34d 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -155,6 +155,16 @@ Node ExtendedRewriter::extendedRewrite(Node n)
         // we may have subsumed children down to one
         ret = children[0];
       }
+      else if (isAssoc && children.size() > kind::metakind::getUpperBoundForKind(k))
+      {
+        Assert(kind::metakind::getUpperBoundForKind(k) >= 2);
+        // kind may require binary construction
+        ret = children[0];
+        for (unsigned i = 1, nchild = children.size(); i < nchild; i++)
+        {
+          ret = nm->mkNode(k, ret, children[i]);
+        }
+      }
       else
       {
         ret = nm->mkNode(k, children);