diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 81391cb34..6d075ebcd 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -279,18 +279,6 @@ namespace {
             return const_cast<smt::kernel&>(m_context).get_context().get_fparams().m_max_conflicts;
         }
 
-        void reset_parallel_statistics() override {
-            m_context.reset_aux_statistics();
-        }
-
-        void add_parallel_statistics(statistics const& st) override {
-            m_context.add_aux_statistics(st);
-        }
-
-        void collect_parallel_statistics(statistics& st) const override {
-            m_context.collect_statistics(st);
-        }
-
         void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
             ast_manager& m = get_manager();
             auto& ctx = m_context.get_context();
diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp
index ae5b739f4..dcd844b09 100644
--- a/src/solver/parallel_tactical2.cpp
+++ b/src/solver/parallel_tactical2.cpp
@@ -1893,28 +1893,28 @@ public:
         for (auto& t : threads)
             t.join();
 
-        m_solver->reset_parallel_statistics();
+        m_solver->reset_statistics();
         statistics aux;
         for (auto* w : m_workers) {
             aux.reset();
             w->collect_statistics(aux);
-            m_solver->add_parallel_statistics(aux);
+            m_solver->add_statistics(aux);
         }
         aux.reset();
         m_batch_manager.collect_statistics(aux);
-        m_solver->add_parallel_statistics(aux);
+        m_solver->add_statistics(aux);
         if (m_core_minimizer_worker) {
             aux.reset();
             m_core_minimizer_worker->collect_statistics(aux);
-            m_solver->add_parallel_statistics(aux);
+            m_solver->add_statistics(aux);
         }
         for (auto* w : m_global_backbones_workers) {
             aux.reset();
             w->collect_statistics(aux);
-            m_solver->add_parallel_statistics(aux);
+            m_solver->add_statistics(aux);
         }
         m_stats.reset();
-        m_solver->collect_parallel_statistics(m_stats);
+        m_solver->collect_statistics(m_stats);
 
         m_manager.limit().reset_cancel();
 
diff --git a/src/solver/solver.h b/src/solver/solver.h
index d4118c4c2..f1de41880 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -57,7 +57,6 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p, symbol const& logic
 class solver : public check_sat_result, public user_propagator::core {
     params_ref  m_params;
     symbol      m_cancel_backup_file;
-    statistics  m_parallel_stats;
 public:
     struct scored_literal {
         expr_ref lit;
@@ -330,18 +329,6 @@ public:
 
     virtual unsigned get_max_conflicts() const { return UINT_MAX; }
 
-    virtual void reset_parallel_statistics() {
-        m_parallel_stats.reset();
-    }
-
-    virtual void add_parallel_statistics(statistics const& st) {
-        m_parallel_stats.copy(st);
-    }
-
-    virtual void collect_parallel_statistics(statistics& st) const {
-        st.copy(m_parallel_stats);
-        collect_statistics(st);
-    }
     
     virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;