diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index a90840d3b..9cda41b50 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -658,9 +658,7 @@ namespace sat {
             return;
         bool value = !l.sign();
         set_phase(l.var(), value);
-        if (m_best_phase[l.var()] != value)
-            m_best_phase_birthdate[l.var()] = m_stats.m_conflicts;
-        m_best_phase[l.var()] = value;
+        set_best_phase(l.var(), value);
     }
 
     void solver::set_phase(bool_var v, bool value) {
@@ -669,6 +667,12 @@ namespace sat {
         m_phase[v] = value;
     }
 
+    void solver::set_best_phase(bool_var v, bool value) {
+        if (m_best_phase[v] != value)
+            m_best_phase_birthdate[v] = m_stats.m_conflicts;
+        m_best_phase[v] = value;
+    }
+
     struct solver::cmp_activity {
         solver& s;
         cmp_activity(solver& s):s(s) {}
@@ -1404,9 +1408,7 @@ namespace sat {
         if (mdl.size() == m_best_phase.size()) {
             for (unsigned i = 0; i < m_best_phase.size(); ++i) {
                 bool is_true = l_true == mdl[i];
-                if (m_best_phase[i] != is_true)
-                    m_best_phase_birthdate[i] = m_stats.m_conflicts;
-                m_best_phase[i] = is_true;
+                set_best_phase(i, is_true);
             }
 
             if (r == l_true) {
@@ -2201,9 +2203,7 @@ namespace sat {
                 m_model[v] = value(v);
                 bool is_true = value(v) == l_true;
                 set_phase(v, is_true);
-                if (m_best_phase[v] != is_true)
-                    m_best_phase_birthdate[v] = m_stats.m_conflicts;
-                m_best_phase[v] = is_true;
+                set_best_phase(v, is_true);
             }
         }
         TRACE(sat_mc_bug, m_mc.display(tout););
@@ -2980,9 +2980,7 @@ namespace sat {
             IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n");
             for (unsigned i = 0; i < head; ++i) {
                 bool_var v = m_trail[i].var();
-                if (m_best_phase[v] != m_phase[v])
-                    m_best_phase_birthdate[v] = m_stats.m_conflicts;
-                m_best_phase[v] = m_phase[v];
+                set_best_phase(v, m_phase[v]);
             }
             set_has_new_best_phase(true);
         }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 5581668ef..622e551bb 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -377,6 +377,7 @@ namespace sat {
         bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
         void set_phase(literal l) override;
         void set_phase(bool_var v, bool value);
+        void set_best_phase(bool_var v, bool value);
         bool get_phase(bool_var b) { return m_phase.get(b, false); }
         bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); }
         uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); }
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index fc2c87f5a..034c34d79 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -288,14 +288,6 @@ namespace smt {
         m_imp->m_kernel.get_fparams().m_preprocess = f;
     }
 
-    void kernel::reset_aux_statistics() {
-        m_imp->m_kernel.m_aux_stats.reset();
-    }
-
-    void kernel::add_aux_statistics(::statistics const& st) {
-        m_imp->m_kernel.m_aux_stats.copy(st);
-    }
-
     context & kernel::get_context() {
         return m_imp->m_kernel;
     }
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index a1b2bfc18..9c4395cf8 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -304,10 +304,6 @@ namespace smt {
 
         void set_preprocess(bool f);
 
-        void reset_aux_statistics();
-
-        void add_aux_statistics(::statistics const& st);
-
         void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause);
 
         /**