From 2c7a64f5bdafd35e02510db5ec8026cff32e505f Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 2 Jun 2019 18:54:02 -0700 Subject: [PATCH] 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. --- src/expr/node_builder.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 9128bc190..4558f3720 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -772,8 +772,8 @@ void NodeBuilder::clear(Kind k) { template void NodeBuilder::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 ); -- 2.30.2