diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index fabdb6abd..fab67a801 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -328,7 +328,6 @@ namespace smt {
             return;
         }
         context & ctx      = get_context();
-        region & r         = ctx.get_region();
         enode * _x         = get_enode(x);
         enode * _y         = get_enode(y);
         eq_vector const& eqs = antecedents.eqs();
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 46d2b0119..8f69c9489 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -591,7 +591,6 @@ namespace smt {
             get_antecedents(target, source, antecedents);
             if (l != null_literal)
                 antecedents.push_back(l);
-            region & r    = ctx.get_region();
             ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), ctx, antecedents.size(), antecedents.data())));
 
             return;
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index 18083452b..788f562d3 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -112,6 +112,7 @@ public:
         unsigned bv_sz;
         expr * f, * lhs, * rhs;
 
+#if 0
         auto match_bitmask = [&](expr* lhs, expr* rhs) {
             unsigned lo, hi;
             expr* arg;
@@ -131,7 +132,8 @@ public:
             update_unsigned_upper(to_app(arg), val);
             return true;
         };
-            
+#endif
+
         for (unsigned i = 0; i < sz; i++) {
             bool negated = false;
             f = g.form(i);