diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index b93dd7657..64ec064a8 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -474,13 +474,15 @@ void pattern_inference::reset_pre_patterns() {
     m_pre_patterns.reset();
 }
 
-
+#ifdef _TRACE
 static void dump_app_vector(std::ostream & out, ptr_vector<app> const & v, ast_manager & m) {
     ptr_vector<app>::const_iterator it  = v.begin();
     ptr_vector<app>::const_iterator end = v.end();
     for (; it != end; ++it) 
         out << mk_pp(*it, m) << "\n";
 }
+#endif
+
 bool pattern_inference::is_forbidden(app * n) const {
     func_decl const * decl = n->get_decl();
     if (is_ground(n))
diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp
index 1e9ff926c..76cdfbdbe 100644
--- a/src/ast/rewriter/bv_bounds.cpp
+++ b/src/ast/rewriter/bv_bounds.cpp
@@ -25,7 +25,7 @@ bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool nega
     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& one = numeral::one();
-    SASSERT(numerl::zero() <= lo);
+    SASSERT(numeral::zero() <= lo);
     SASSERT(lo <= hi);
     SASSERT(hi < numeral::power_of_two(bv_sz));
     numeral vmax, vmin;
diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h
index 98f65a734..66d17fdc8 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.h
+++ b/src/muz/transforms/dl_mk_rule_inliner.h
@@ -88,7 +88,7 @@ namespace datalog {
             svector<bool> m_can_remove, m_can_expand;
             obj_map<expr, unsigned_vector> m_positions;
         public:
-            visitor(context& c, substitution & s): st_visitor(s), m_context(c) {}
+            visitor(context& c, substitution & s): st_visitor(s), m_context(c) { (void) m_context; }
             virtual bool operator()(expr* e);
             void         reset() { m_unifiers.reset(); }
             void         reset(unsigned sz);
diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp
index 9a6868ff1..de88d37bb 100644
--- a/src/smt/arith_eq_solver.cpp
+++ b/src/smt/arith_eq_solver.cpp
@@ -113,6 +113,8 @@ unsigned arith_eq_solver::find_abs_min(vector<numeral>& values) {
     return index;
 }
 
+#ifdef _TRACE
+
 static void print_row(std::ostream& out, vector<rational> const& row) {
     for(unsigned i = 0; i < row.size(); ++i) { 
         out << row[i] << " "; 
@@ -125,6 +127,7 @@ static void print_rows(std::ostream& out, vector<vector<rational> > const& rows)
         print_row(out, rows[i]);
     }
 }
+#endif
 
 //
 // The gcd of the coefficients to variables have to divide the
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 60aed12e1..5d03a3563 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -490,6 +490,7 @@ namespace smt {
 #ifdef _PROFILE_MAM
             m_counter = 0;
 #endif
+            (void)m_lbl_hasher;
         }
 
 #ifdef _PROFILE_MAM
@@ -2881,6 +2882,7 @@ namespace smt {
            - first_idx: index to be used as head of the multi-pattern mp
         */
         void add_pattern(quantifier * qa, app * mp, unsigned first_idx) {
+            (void)m_ast_manager;
             SASSERT(m_ast_manager.is_pattern(mp));
             SASSERT(first_idx < mp->get_num_args());
             app * p           = to_app(mp->get_arg(first_idx));
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index ad1e55ba6..f7936eacd 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -335,23 +335,6 @@ namespace smt {
         }
     }
 
-    static bool find_arg(app * n, expr * t, expr * & other) {
-        SASSERT(n->get_num_args() == 2);
-        if (n->get_arg(0) == t) {
-            other = n->get_arg(1);
-            return true;
-        }
-        else if (n->get_arg(1) == t) {
-            other = n->get_arg(0);
-            return true;
-        }
-        return false;
-    }
-
-    static bool check_args(app * n, expr * t1, expr * t2) {
-        SASSERT(n->get_num_args() == 2);
-        return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2);
-    }
 
     /**
        \brief Internalize the given formula into the logical context.
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 2b327eb66..a70ddb98f 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -112,7 +112,6 @@ namespace smt {
         };
 
         class fpa_rm_value_proc : public model_value_proc {
-            theory_fpa  & m_th;
             ast_manager & m;
             fpa_util    & m_fu;
             bv_util     & m_bu;
@@ -120,7 +119,7 @@ namespace smt {
 
         public:
             fpa_rm_value_proc(theory_fpa * th) :
-                m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
+                m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
 
             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
 
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index b665c2a94..e396b67cc 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/src/smt/theory_wmaxsat.cpp
@@ -102,6 +102,7 @@ namespace smt {
         m_enabled.push_back(true);
         m_normalize = true;
         bool_var bv = register_var(var, true);
+        (void)bv;
         TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
               tout << wfml << "\n";);
         return var;