diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 945f6686e..f29f73b3a 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2256,9 +2256,10 @@ bool context::validate()
                     fv.reverse ();
                     tmp = m.mk_exists(fv.size(), fv.c_ptr(), names.c_ptr(), tmp);
                 }
-                smt::kernel solver(m, m_pm.fparams2());
-                solver.assert_expr(tmp);
-                lbool res = solver.check();
+                ref<solver> sol =
+                    mk_smt_solver(m, params_ref::get_empty(), symbol::null);
+                sol->assert_expr(tmp);
+                lbool res = sol->check_sat(0, nullptr);
                 if (res != l_false) {
                     msg << "rule validation failed when checking: "
                         << mk_pp(tmp, m);
@@ -2648,7 +2649,8 @@ expr_ref context::get_ground_sat_answer()
     { cex.push_back(m.mk_const(preds[0])); }
 
     // smt context to obtain local cexes
-    scoped_ptr<smt::kernel> cex_ctx = alloc (smt::kernel, m, m_pm.fparams2 ());
+    ref<solver> cex_ctx =
+        mk_smt_solver(m, params_ref::get_empty(), symbol::null);
     model_evaluator_util mev (m);
 
     // preorder traversal of the query derivation tree
@@ -2689,7 +2691,7 @@ expr_ref context::get_ground_sat_answer()
         }
         cex_ctx->assert_expr (pt->transition ());
         cex_ctx->assert_expr (pt->rule2tag (r));
-        lbool res = cex_ctx->check ();
+        lbool res = cex_ctx->check_sat(0, nullptr);
         CTRACE("cex", res == l_false,
                tout << "Cex fact: " << mk_pp(cex_fact, m) << "\n";
                for (unsigned i = 0; i < u_tail_sz; i++)
@@ -3624,10 +3626,9 @@ void context::reset_statistics()
 
 bool context::check_invariant(unsigned lvl)
 {
-    decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
-    for (; it != end; ++it) {
+    for (auto &entry : m_rels) {
         checkpoint();
-        if (!check_invariant(lvl, it->m_key)) {
+        if (!check_invariant(lvl, entry.m_key)) {
             return false;
         }
     }
@@ -3636,7 +3637,7 @@ bool context::check_invariant(unsigned lvl)
 
 bool context::check_invariant(unsigned lvl, func_decl* fn)
 {
-    smt::kernel ctx(m, m_pm.fparams2());
+    ref<solver> ctx = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
     pred_transformer& pt = *m_rels.find(fn);
     expr_ref_vector conj(m);
     expr_ref inv = pt.get_formulas(next_level(lvl), false);
@@ -3644,9 +3645,10 @@ bool context::check_invariant(unsigned lvl, func_decl* fn)
     pt.add_premises(m_rels, lvl, conj);
     conj.push_back(m.mk_not(inv));
     expr_ref fml(m.mk_and(conj.size(), conj.c_ptr()), m);
-    ctx.assert_expr(fml);
-    lbool result = ctx.check();
-    TRACE("spacer", tout << "Check invariant level: " << lvl << " " << result << "\n" << mk_pp(fml, m) << "\n";);
+    ctx->assert_expr(fml);
+    lbool result = ctx->check_sat(0, nullptr);
+    TRACE("spacer", tout << "Check invariant level: " << lvl << " " << result
+          << "\n" << mk_pp(fml, m) << "\n";);
     return result == l_false;
 }
 
diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index 34f1eb730..7263f8264 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -29,7 +29,7 @@ Revision History:
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/substitution/matcher.h"
 #include "ast/expr_functors.h"
-
+#include "smt/smt_solver.h"
 
 namespace spacer {
 void lemma_sanity_checker::operator()(lemma_ref &lemma) {
@@ -249,17 +249,17 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
         { eqs.push_back(m.mk_eq(m.mk_const(vsymbs.get(i)),
                                 m.mk_const(vsymbs.get(j)))); }
 
-    smt::kernel solver(m, m_ctx.get_manager().fparams2());
+    ref<solver> sol = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
     expr_ref_vector lits(m);
     for (unsigned i = 0, core_sz = core.size(); i < core_sz; ++i) {
         SASSERT(lits.size() == i);
-        solver.push();
-        solver.assert_expr(core.get(i));
+        sol->push();
+        sol->assert_expr(core.get(i));
         for (unsigned j = 0, eqs_sz = eqs.size(); j < eqs_sz; ++j) {
-            solver.push();
-            solver.assert_expr(eqs.get(j));
-            lbool res = solver.check();
-            solver.pop(1);
+            sol->push();
+            sol->assert_expr(eqs.get(j));
+            lbool res = sol->check_sat(0, nullptr);
+            sol->pop(1);
 
             if (res == l_false) {
                 TRACE("core_array_eq",
@@ -269,7 +269,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
                 break;
             }
         }
-        solver.pop(1);
+        sol->pop(1);
         if (lits.size() == i) { lits.push_back(core.get(i)); }
     }