diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp
index dc10b5f8e..0d4cd02d3 100644
--- a/src/muz/rel/dl_base.cpp
+++ b/src/muz/rel/dl_base.cpp
@@ -189,8 +189,7 @@ namespace datalog {
         union_find_default_ctx uf_ctx;
         union_find<> uf(uf_ctx); //the numbers in uf correspond to column indexes after the join
         for(unsigned i=0; i<join_sig_sz; i++) {
-            unsigned v = uf.mk_var();
-            SASSERT(v==i);
+            VERIFY(uf.mk_var() == i);
         }
 
         for(unsigned i=0; i<joined_col_cnt; i++) {
diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp
index 70229ccab..888827754 100644
--- a/src/smt/smt_implied_equalities.cpp
+++ b/src/smt/smt_implied_equalities.cpp
@@ -166,11 +166,10 @@ namespace smt {
                     terms[i].term = m.mk_app(m_array_util.get_family_id(), OP_SELECT, 0, 0, args.size(), args.c_ptr());
                 }
                 assert_relevant(terms);
-                lbool is_sat = m_solver.check_sat(0,0);
+                VERIFY(m_solver.check_sat(0,0) != l_false);
                 model_ref model1;
                 m_solver.get_model(model1);
                 SASSERT(model1.get());
-                SASSERT(is_sat != l_false);
                 get_implied_equalities_model_based(model1, terms);
                 m_solver.pop(1);
                 return;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index a7f442e1f..3f44e4ab7 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -564,11 +564,9 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_numeral(app * n) {
         rational _val;
-        context & ctx = get_context();
-        bool flag = m_util.is_numeral(n, _val);
+        VERIFY(m_util.is_numeral(n, _val));
         numeral val(_val);
-        SASSERT(flag);
-        SASSERT(!ctx.e_internalized(n));
+        SASSERT(!get_context().e_internalized(n));
         enode * e    = mk_enode(n);
         // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
         // e->mark_as_interpreted();
@@ -3117,8 +3115,7 @@ namespace smt {
         del_vars(get_old_num_vars(num_scopes));
         m_scopes.shrink(new_lvl);
         theory::pop_scope_eh(num_scopes);
-        bool r = make_feasible();
-        SASSERT(r);
+        VERIFY(make_feasible());
         SASSERT(m_to_patch.empty());
         m_to_check.reset();
         m_in_to_check.reset();
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index b33e6b4e6..663816a7d 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -645,11 +645,10 @@ namespace smt {
             if (is_store(n)) {
                 theory_var w = n->get_arg(0)->get_th_var(get_id());
                 SASSERT(w != null_theory_var);
-                ast_manager& m = get_manager();
 
                 mg_merge(v, get_representative(w));
                                 
-                TRACE("array", tout << "merge: " << mk_pp(n->get_owner(), m) << " " << v << " " << w << "\n";);
+                TRACE("array", tout << "merge: " << mk_pp(n->get_owner(), get_manager()) << " " << v << " " << w << "\n";);
             }
             else if (is_const(n)) {
                 set_default(v, n->get_arg(0));