diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2019-06-02 18:54:02 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-06-02 18:54:02 -0700 |
| commit | 2c7a64f5bdafd35e02510db5ec8026cff32e505f (patch) | |
| tree | ae3a1a93ff6e01f5664fd52113a55f67175b5b4e | |
| parent | 2d9f552b86cf75a95187541699612ea1331ec990 (diff) | |
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.
| -rw-r--r-- | src/expr/node_builder.h | 4 |
1 files 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<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 ); |