diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 7e19bf520..0054c8d65 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -239,7 +239,7 @@ namespace sat {
             else {
                 model_converter::entry & e = mc.mk(model_converter::ELIM_VAR, v);
                 TRACE("save_elim", tout << "marking as deleted: " << v << " l: " << l << " r: " << r << "\n";);
-                m_solver.m_eliminated[v] = true;
+                m_solver.set_eliminated(v, true);
                 mc.insert(e, ~l, r);
                 mc.insert(e,  l, ~r);
             }
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 9c8e08d3d..1d7280a48 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -155,21 +155,6 @@ namespace smt {
         expr_ref_vector get_trail() {
             return m_kernel.get_trail();
         }
-
-        void set_activity(expr* lit, double act) {
-            SASSERT(m().is_bool(lit));
-            m().is_not(lit, lit);
-            if (!m_kernel.b_internalized(lit)) {
-                m_kernel.internalize(lit, false);
-            }
-            if (!m_kernel.b_internalized(lit)) {
-                return;
-            }
-            auto v = m_kernel.get_bool_var(lit);
-            double old_act = m_kernel.get_activity(v);
-            m_kernel.set_activity(v, act);
-            m_kernel.activity_changed(v, act > old_act);
-        }
         
         failure last_failure() const {
             return m_kernel.get_last_search_failure();
@@ -427,9 +412,5 @@ namespace smt {
         return m_imp->get_trail();
     }
 
-    void kernel::set_activity(expr* lit, double activity) {
-        m_imp->set_activity(lit, activity);
-    }
-
 
 };
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index b2b5632c9..2cf3f4e7b 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -229,11 +229,6 @@ namespace smt {
         */
         expr_ref_vector get_trail();
 
-        /**
-           \brief set activity of literal
-        */
-        void set_activity(expr* lit, double activity);
-
         /**
            \brief (For debubbing purposes) Prints the state of the kernel
         */