summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-12-12 16:37:59 -0800
committerGitHub <noreply@github.com>2018-12-12 16:37:59 -0800
commitc2be681200406d8a96a1c2e1b9fbbb228334eed8 (patch)
tree6ffc195c7e5288644547445194360e53c185375c /src
parent12f88ad664c24ee522643073dcddf144854ca1ef (diff)
Fix compiler warnings. (#2748)
Diffstat (limited to 'src')
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h6
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback