diff --git a/src/ast/rewriter/inj_axiom.cpp b/src/ast/rewriter/inj_axiom.cpp
index bdf784230..a46e60e5c 100644
--- a/src/ast/rewriter/inj_axiom.cpp
+++ b/src/ast/rewriter/inj_axiom.cpp
@@ -74,6 +74,7 @@ bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
                     }
                 }
                 if (found_vars && !has_free_vars(q)) {
+                    (void)num_vars;
                     TRACE("inj_axiom", 
                           tout << "Cadidate for simplification:\n" << mk_ll_pp(q, m) << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n" <<
                           mk_pp(var1, m) << "\n" << mk_pp(var2, m) << "\nnum_vars: " << num_vars << "\n";);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 2589c51b8..5fe5c5e4e 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1012,7 +1012,7 @@ namespace sat {
     }
 
     bool solver::propagate_literal(literal l, bool update) {
-        literal l1, l2;
+        literal l1;
 
         bool keep;
         unsigned curr_level = lvl(l);
@@ -4733,7 +4733,7 @@ namespace sat {
                 num_lits += c.size();
             }
         }
-        unsigned total_cls = num_cls + num_ter + num_bin;
+        unsigned total_cls = num_cls + num_ter + num_bin + num_ext;
         double mem = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
         out << "(sat-status\n";
         out << "  :inconsistent    " << (m_inconsistent ? "true" : "false") << "\n";
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index cd4c8bf75..4628721ab 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -1872,13 +1872,11 @@ public:
                     // found path.
                     reset_marks();
                     m_heap.reset();              
-                    unsigned length = 0;
                     do {
                         inc_activity(m_parent[w]);
                         edge const& ee = m_edges[m_parent[w]];
                         f(ee.get_explanation());
                         w = ee.get_source();
-                        ++length;
                     }
                     while (w != src2);
                     return;
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index acb036d2a..e624f84b5 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1554,6 +1554,7 @@ namespace smt {
             min_gain.reset();
             ++round;
 
+            (void)round;
             TRACE("opt", tout << "round: " << round << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout););
             typename vector<row_entry>::const_iterator it  = r.begin_entries();
             typename vector<row_entry>::const_iterator end = r.end_entries();