diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index ebb5e00c8..4f6741989 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -342,6 +342,7 @@ public:
                     else
                         cls1.push_back(cls2[j]);
                 }
+                (void)found_pivot2;
                 assert(found_pivot2);
                 return;
             }
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index f20f16a08..95d66f617 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -362,6 +362,7 @@ public:
                     else
                         cls1.push_back(cls2[j]);
                 }
+                (void)found_pivot2;
                 assert(found_pivot2);
                 return;
             }
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index e8e93dafc..049c34343 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -300,6 +300,7 @@ public:
                 break;
 
             case datalog::OK: 
+                (void)query_exn;
                 SASSERT(query_exn);
                 break;
 
diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp
index 3b9198dc6..0baa297bc 100644
--- a/src/muz/rel/karr_relation.cpp
+++ b/src/muz/rel/karr_relation.cpp
@@ -173,6 +173,7 @@ namespace datalog {
                 else {
                     processed = false;
                 }
+                (void)processed;
                 TRACE("dl", tout << (processed?"+ ":"- ") << mk_pp(e, m) << "\n";
                       if (processed) matrix::display_ineq(tout, row, M.b.back(), M.eq.back());
                       );
diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index 2881c03ae..eabc4fdb1 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -52,6 +52,7 @@ namespace sat {
 
     bool clause::check_approx() const {
         var_approx_set curr = m_approx;
+        (void)curr;
         const_cast<clause*>(this)->update_approx();
         SASSERT(may_eq(curr, m_approx));
         return true;
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index ac2a51c4d..c60fb86cb 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -159,7 +159,8 @@ namespace sat {
         for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
             literal l = ~to_literal(l_idx);            
             watch_list const & wlist = *it;
-            CTRACE("sat_bug", s.was_eliminated(l.var()) && !wlist.empty(),
+            CTRACE("sat_bug", 
+                   s.was_eliminated(l.var()) && !wlist.empty(),
                    tout << "l: " << l << "\n";
                    s.display_watches(tout);
                    s.display(tout););
@@ -179,7 +180,7 @@ namespace sat {
                            tout << "\n";
                            sat::display(tout, s.m_cls_allocator, s.get_wlist(~(it2->get_literal())));
                            tout << "\n";);
-                    SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
+                        SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
                     break;
                 case watched::TERNARY:
                     SASSERT(!s.was_eliminated(it2->get_literal1().var()));
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index daaed13ac..f55945ce4 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -739,6 +739,7 @@ public:
         if (idx2 < idx1) {
             std::swap(idx1,idx2);
         }        
+        (void) max_idx;
         SASSERT(idx1 < idx2 && idx2 < edges.size());
         SASSERT(max_idx < edges.size());
         dst = get_source(edges[idx2]);
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 88676b4d9..163452d47 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1342,6 +1342,7 @@ namespace smt {
               tout << "v" << x_i << " ";
               tout << (has_shared?"shared":"not shared") << "\n";);
 
+        (void) empty_column;
         SASSERT(!safe_gain(min_gain, max_gain) ||
                 empty_column ||
                 (unbounded_gain(max_gain) == (x_i == null_theory_var)));
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 59bcf40e8..eecf97069 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -276,6 +276,7 @@ namespace smt {
             SASSERT(r && bv_sz == m_ebits);
             r = m_bu.is_numeral(values[2], sig_r, bv_sz);
             SASSERT(r && bv_sz == m_sbits - 1);
+            (void)r;
 
             SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator()));
             SASSERT(mpzm.is_one(exp_r.to_mpq().denominator()));
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 698128e26..eae3ab5e6 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -156,6 +156,7 @@ class fm_tactic : public tactic {
                     r = c;
                 }
             }
+            (void)found;
             SASSERT(found);
             return is_lower ? LOWER : UPPER;
         }
diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp
index 0c1744a09..ea2a60627 100644
--- a/src/util/mpn.cpp
+++ b/src/util/mpn.cpp
@@ -280,7 +280,6 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
     for (size_t j = numer.size()-1; j > 0; j--) {
         temp = (((mpn_double_digit)numer[j]) << DIGIT_BITS) | ((mpn_double_digit)numer[j-1]);
         q_hat = temp / (mpn_double_digit) denom;
-        r_hat = temp % (mpn_double_digit) denom;
         if (q_hat >= BASE) {
             UNREACHABLE(); // is this reachable with normalized v?
         }
@@ -294,11 +293,13 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
             quot[j-1]--;
             numer[j] = numer[j-1] + denom;
         }
-        TRACE("mpn_div1", tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
-                          tout << " ms=" << ms;
-                          tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());
-                          tout << " borrow=" << borrow;
-                          tout << std::endl; );
+        TRACE("mpn_div1", 
+              r_hat = temp % (mpn_double_digit) denom;
+              tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
+              tout << " ms=" << ms;
+              tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());
+              tout << " borrow=" << borrow;
+              tout << std::endl; );
     }
 
     return true; // return rem != 0?