Add check for limit of number of node children (#3035)

This commit adds a check that makes sure that we do not try to create
nodes with more children than the maxmimum number. This can currently
happen when flattening nodes in QF_BV with lots of duplicate children.

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 9128bc1901b188a09a3620d8444e1fa20d21fe54..4558f3720b9aa827d01547adc69c741e1810fac7 100644 (file)
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -772,8 +772,8 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
-  Assert( toSize > d_nvMaxChildren,
-          "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
+  AlwaysAssert(toSize > d_nvMaxChildren,
+               "attempt to realloc() a NodeBuilder to a smaller/equal size!");
   Assert( toSize < (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
           "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
           toSize, (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );