diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-12 16:37:59 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-12 16:37:59 -0800 |
commit | c2be681200406d8a96a1c2e1b9fbbb228334eed8 (patch) | |
tree | 6ffc195c7e5288644547445194360e53c185375c /src/theory/bv | |
parent | 12f88ad664c24ee522643073dcddf144854ca1ef (diff) |
Fix compiler warnings. (#2748)
Diffstat (limited to 'src/theory/bv')
-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); |