Fix compiler warnings. (#2748)

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 7efdc2c81b70c2a7eb553d586533c47311da220a..c58d69f6f8fdd6fc0fdee82b099b8fd8d09e974a 100644 (file)
--- 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);