diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h
index 78a4e8301..b050e45e1 100644
--- a/src/math/simplex/sparse_matrix_def.h
+++ b/src/math/simplex/sparse_matrix_def.h
@@ -542,10 +542,11 @@ namespace simplex {
                 continue;
             }
             SASSERT(!rows.contains(c.m_row_id));
-            _row const& row = m_rows[c.m_row_id];
-            _row_entry const& r = row.m_entries[c.m_row_idx];
-            SASSERT(r.m_var == v); 
-            SASSERT((unsigned)r.m_col_idx == i);
+            DEBUG_CODE(
+                _row const& row = m_rows[c.m_row_id];
+                _row_entry const& r = row.m_entries[c.m_row_idx];
+                SASSERT(r.m_var == v); 
+                SASSERT((unsigned)r.m_col_idx == i););
             rows.insert(c.m_row_id);
         }                           
         int idx = col.m_first_free_idx;
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 9742d2051..721e38942 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -861,11 +861,12 @@ namespace qe {
 
         void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) {
             expr_ref orig(fml);
-            ast_manager& m = fml.get_manager();
             m_nnf_core(fml);
             m_normalize_literals(fml);
             m_collect_atoms(fml, pos, neg);
-            TRACE("qe", tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";);
+            TRACE("qe",
+                  ast_manager& m = fml.get_manager(); 
+                  tout << mk_ismt2_pp(orig, m) << "\n-->\n" << mk_ismt2_pp(fml, m) << "\n";);
         }      
 
         void reset() {
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index dfba7c170..59bcf40e8 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -306,9 +306,10 @@ namespace smt {
 
     app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
         SASSERT(values.size() == 1);
-        ast_manager & m = m_th.get_manager();
 
-        TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
+        TRACE("t_fpa_detail", 
+              ast_manager & m = m_th.get_manager();
+              for (unsigned i = 0; i < values.size(); i++)
               tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
 
         app * result = 0;
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index a1aebf3e1..273bffd93 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -787,8 +787,7 @@ namespace smt {
             }
 
             for (unsigned i = 0; i < ineqs->size(); ++i) {
-                ineq* c = (*ineqs)[i]; 
-                SASSERT(c->is_ge());
+                SASSERT((*ineqs)[i]->is_ge());
                 if (assign_watch_ge(v, is_true, *ineqs, i)) {
                     // i was removed from watch list.
                     --i;
@@ -1834,13 +1833,12 @@ namespace smt {
 
     void theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
         uint_set nlits;
-        context& ctx = get_context();
         for (unsigned i = 0; i < lits.size(); ++i) {
-            SASSERT(ctx.get_assignment(lits[i]) == l_true);
+            SASSERT(get_context().get_assignment(lits[i]) == l_true);
             nlits.insert((~lits[i]).index());
         }
-        SASSERT(ctx.get_assignment(l) == l_undef);
-        SASSERT(ctx.get_assignment(c.lit()) == l_true);
+        SASSERT(get_context().get_assignment(l) == l_undef);
+        SASSERT(get_context().get_assignment(c.lit()) == l_true);
         nlits.insert(l.index());
         numeral sum = numeral::zero();
         for (unsigned i = 0; i < c.size(); ++i) {