diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 193ef7705..1aaecf736 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -294,6 +294,10 @@ namespace smt {
             return m_fparams;
         }
 
+        smt_params const& get_fparams() const {
+            return m_fparams;
+        }
+
         params_ref const & get_params() {
             return m_params;
         }
@@ -1921,4 +1925,3 @@ namespace smt {
     std::ostream& operator<<(std::ostream& out, enode_pp const& p);
 
 };
-
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 034c34d79..1e49a8d3c 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -292,6 +292,10 @@ namespace smt {
         return m_imp->m_kernel;
     }
 
+    context const& kernel::get_context() const {
+        return m_imp->m_kernel;
+    }
+
     void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
         m_imp->m_kernel.get_levels(vars, depth);
     }
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index 9c4395cf8..0a6faaa09 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -344,6 +344,6 @@ namespace smt {
            \warning This method should not be used in new code.
         */
         context & get_context();
+        context const& get_context() const;
     };
 };
-
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 7409b5851..e3e15ea9a 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -221,7 +221,7 @@ namespace {
 
         expr_ref_vector get_assigned_literals() override {
             expr_ref_vector result(m);
-            auto& ctx = const_cast<smt::kernel&>(m_context).get_context();
+            auto const& ctx = m_context.get_context();
             for (auto lit : ctx.assigned_literals()) {
                 expr* atom = ctx.bool_var2expr(lit.var());
                 if (!atom)
@@ -232,7 +232,7 @@ namespace {
         }
 
         unsigned get_assign_level(expr* e) const override {
-            auto& ctx = const_cast<smt::kernel&>(m_context).get_context();
+            auto const& ctx = m_context.get_context();
             expr* atom = e;
             get_manager().is_not(e, atom);
             if (!ctx.b_internalized(atom))
@@ -241,18 +241,18 @@ namespace {
         }
 
         bool is_relevant(expr* e) const override {
-            auto& ctx = const_cast<smt::kernel&>(m_context).get_context();
+            auto const& ctx = m_context.get_context();
             expr* atom = e;
             get_manager().is_not(e, atom);
             return ctx.b_internalized(atom) && ctx.is_relevant(atom);
         }
 
         unsigned get_num_bool_vars() const override {
-            return const_cast<smt::kernel&>(m_context).get_context().get_num_bool_vars();
+            return m_context.get_context().get_num_bool_vars();
         }
 
         sat::bool_var get_bool_var(expr* e) const override {
-            auto& ctx = const_cast<smt::kernel&>(m_context).get_context();
+            auto const& ctx = m_context.get_context();
             expr* atom = e;
             get_manager().is_not(e, atom);
             return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var;
@@ -263,7 +263,7 @@ namespace {
         }
 
         void setup_for_parallel() override {
-            const_cast<smt::kernel&>(m_context).get_context().setup_for_parallel();
+            m_context.get_context().setup_for_parallel();
         }
 
         void set_preprocess(bool f) override {
@@ -271,12 +271,12 @@ namespace {
         }
 
         void set_max_conflicts(unsigned max_conflicts) override {
-            auto& ctx = const_cast<smt::kernel&>(m_context).get_context();
+            auto& ctx = m_context.get_context();
             ctx.get_fparams().m_max_conflicts = max_conflicts;
         }
 
         unsigned get_max_conflicts() const override {
-            return const_cast<smt::kernel&>(m_context).get_context().get_fparams().m_max_conflicts;
+            return m_context.get_context().get_fparams().m_max_conflicts;
         }
 
         void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
@@ -676,4 +676,3 @@ public:
 solver_factory * mk_smt_solver_factory() {
     return alloc(smt_solver_factory);
 }
-