diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index 0dec98e5c..c113627f9 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/src/ast/fpa/bv2fpa_converter.cpp
@@ -312,11 +312,11 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
         unsigned sbits = m_fpa_util.get_sbits(var->get_range());
 
         app * a0 = to_app(val->get_arg(0));
-        app * a1 = to_app(val->get_arg(1));
-        app * a2 = to_app(val->get_arg(2));
 
         expr_ref v0(m), v1(m), v2(m);
 #ifdef Z3DEBUG
+        app * a1 = to_app(val->get_arg(1));
+        app * a2 = to_app(val->get_arg(2));
         v0 = mc->get_const_interp(a0->get_decl());
         v1 = mc->get_const_interp(a1->get_decl());
         v2 = mc->get_const_interp(a2->get_decl());
@@ -555,4 +555,4 @@ void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
         tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
     });
 
-}
\ No newline at end of file
+}
diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp
index 22decbb7c..1e9ff926c 100644
--- a/src/ast/rewriter/bv_bounds.cpp
+++ b/src/ast/rewriter/bv_bounds.cpp
@@ -24,9 +24,8 @@ bv_bounds::~bv_bounds() {
 bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool negated, vector<ninterval>& nis) {
     TRACE("bv_bounds", tout << "record0 " << mk_ismt2_pp(v, m_m) << ":" << (negated ? "~[" : "[") << lo << ";" << hi << "]" << std::endl;);
     const unsigned bv_sz = m_bv_util.get_bv_size(v);
-    const numeral& zero = numeral::zero();
     const numeral& one = numeral::one();
-    SASSERT(zero <= lo);
+    SASSERT(numerl::zero() <= lo);
     SASSERT(lo <= hi);
     SASSERT(hi < numeral::power_of_two(bv_sz));
     numeral vmax, vmin;
@@ -49,7 +48,7 @@ bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool nega
             hi_max = hi >= vmax;
             lo_min = true;
         }
-        SASSERT(zero <= lo);
+        SASSERT(lo.is_nonneg());
         SASSERT(lo <= hi);
         SASSERT(hi < numeral::power_of_two(bv_sz));
     }
diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp
index 63731c679..6f7e62fd4 100644
--- a/src/ast/simplifier/simplifier.cpp
+++ b/src/ast/simplifier/simplifier.cpp
@@ -650,10 +650,12 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
 #define Grey  1
 #define Black 2
 
+#ifdef Z3DEBUG
 static int get_color(obj_map<expr, int> & colors, expr * n) {
     obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(n, White);
     return entry->get_data().m_value;
 }
+#endif
 
 static bool visit_ac_children(func_decl * f, expr * n, obj_map<expr, int> & colors, ptr_buffer<expr> & todo, ptr_buffer<expr> & result) {
     if (is_app_of(n, f)) {
diff --git a/src/muz/pdr/pdr_sym_mux.cpp b/src/muz/pdr/pdr_sym_mux.cpp
index a68b57e9c..47edb35ac 100644
--- a/src/muz/pdr/pdr_sym_mux.cpp
+++ b/src/muz/pdr/pdr_sym_mux.cpp
@@ -366,6 +366,7 @@ public:
         app * a = to_app(s);
         func_decl * sym = a->get_decl();
         if(!m_parent.has_index(sym, m_from_idx)) {
+            (void) m_homogenous;
             SASSERT(!m_homogenous || !m_parent.is_muxed(sym));
             return false;
         }
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index 8db27c7ec..f7cd371f8 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -96,8 +96,8 @@ namespace sat {
             }
             
             // the first two literals must be watched.
-            SASSERT(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c)));
-            SASSERT(contains_watched(s.get_wlist(~c[1]), c, s.get_offset(c)));
+            VERIFY(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c)));
+            VERIFY(contains_watched(s.get_wlist(~c[1]), c, s.get_offset(c)));
         }
         return true;
     }
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index e6edbf87e..c872a7139 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -426,8 +426,7 @@ namespace smt {
             TRACE("context", tout << "checking: " << mk_pp(conseq[i], m) << "\n";);
             tmp = m.mk_not(conseq[i]);
             assert_expr(tmp);
-            lbool is_sat = check();
-            SASSERT(is_sat != l_true);
+            VERIFY(check() != l_true);
             pop(1);
         }
         model_ref mdl;
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index b84ae68f0..dddb0c636 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -53,8 +53,10 @@ struct aig {
     aig() {}
 };
 
+#if Z3DEBUG
 inline bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
-inline bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
+#endif
+// inline bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
 inline bool is_var(aig * n) { return n->m_children[0].is_null(); }
 inline bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
 inline unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
@@ -66,12 +68,6 @@ inline aig_lit right(aig_lit const & n) { return right(n.ptr()); }
 
 inline unsigned to_idx(aig * p) { SASSERT(!is_var(p)); return p->m_id - FIRST_NODE_ID; }
 
-void unmark(unsigned sz, aig_lit const * ns) {
-    for (unsigned i = 0; i < sz; i++) {
-        ns[i].ptr()->m_mark = false;
-    }
-}
-
 void unmark(unsigned sz, aig * const * ns) {
     for (unsigned i = 0; i < sz; i++) {
         ns[i]->m_mark = false;
diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp
index e67c2470b..1b324b2eb 100644
--- a/src/tactic/bv/bv_bounds_tactic.cpp
+++ b/src/tactic/bv/bv_bounds_tactic.cpp
@@ -148,10 +148,12 @@ struct interval {
     }
 };
 
+#ifdef _TRACE
 std::ostream& operator<<(std::ostream& o, const interval& I) {
     o << "[" << I.l << ", " << I.h << "]";
     return o;
 }
+#endif
 
 
 struct undo_bound {
diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp
index 345ea5cc9..ee6b8f691 100644
--- a/src/tactic/extension_model_converter.cpp
+++ b/src/tactic/extension_model_converter.cpp
@@ -25,7 +25,7 @@ Notes:
 extension_model_converter::~extension_model_converter() {
 }
 
-
+#ifdef _TRACE
 static void display_decls_info(std::ostream & out, model_ref & md) {
     ast_manager & m = md->get_manager();
     unsigned sz = md->get_num_decls();
@@ -42,6 +42,7 @@ static void display_decls_info(std::ostream & out, model_ref & md) {
         out << " :id " << d->get_id() << "\n";
     }
 }
+#endif
 
 void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
     SASSERT(goal_idx == 0);
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 92e916d80..2ccb23305 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -126,7 +126,7 @@ tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl) {
 class trace_tactic : public skip_tactic {
     char const * m_tag;
 public:
-    trace_tactic(char const * tag):m_tag(tag) {}
+    trace_tactic(char const * tag): m_tag(tag) {}
     
     virtual void operator()(goal_ref const & in, 
                             goal_ref_buffer & result, 
@@ -134,6 +134,7 @@ public:
                             proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         TRACE(m_tag, in->display(tout););
+        (void)m_tag;
         skip_tactic::operator()(in, result, mc, pc, core);
     }
 };
diff --git a/src/test/fuzzing/expr_rand.cpp b/src/test/fuzzing/expr_rand.cpp
index f56704e45..ccc4a9e5c 100644
--- a/src/test/fuzzing/expr_rand.cpp
+++ b/src/test/fuzzing/expr_rand.cpp
@@ -13,9 +13,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 expr_rand::expr_rand(ast_manager& m):
     m_manager(m),
-    m_num_vars(0),
-    m_num_apps(0),
-    m_num_nodes(0),
     m_max_steps(10),
     m_funcs(m)
 {}
diff --git a/src/test/fuzzing/expr_rand.h b/src/test/fuzzing/expr_rand.h
index 971a3ec60..bbadd587e 100644
--- a/src/test/fuzzing/expr_rand.h
+++ b/src/test/fuzzing/expr_rand.h
@@ -24,9 +24,6 @@ Revision History:
 
 class expr_rand {
     ast_manager& m_manager;
-    unsigned     m_num_vars;
-    unsigned     m_num_apps;
-    unsigned     m_num_nodes;
     unsigned     m_max_steps;
     random_gen   m_random;