diff options
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 7efdc2c81..c58d69f6f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -535,7 +535,7 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")" << std::endl; - uint32_t m, my, mz, n; + uint32_t m, my, mz; size_t nc; Kind kind = node.getKind(); TNode concat; @@ -589,7 +589,9 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) z = nc > 1 ? zb.constructNode() : zb[0]; } m = utils::getSize(x); - n = utils::getSize(c); +#ifdef CVC4_ASSERTIONS + uint32_t n = utils::getSize(c); +#endif my = y.isNull() ? 0 : utils::getSize(y); mz = z.isNull() ? 0 : utils::getSize(z); Assert(mz == m - my - n); |