Refactor / reimplement statistics (#6162)

This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.

110 files changed, 766 insertions, 1261 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index a56835480..f299459f8 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -154,29 +154,17 @@ struct CutScratchPad {
 };
 
 ApproximateStatistics::ApproximateStatistics()
-  :  d_branchMaxDepth("z::approx::branchMaxDepth",0)
-  ,  d_branchesMaxOnAVar("z::approx::branchesMaxOnAVar",0)
-  ,  d_gaussianElimConstructTime("z::approx::gaussianElimConstruct::time")
-  ,  d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0)
-  ,  d_averageGuesses("z::approx::averageGuesses")
+    : d_branchMaxDepth(
+        smtStatisticsRegistry().registerInt("z::approx::branchMaxDepth")),
+      d_branchesMaxOnAVar(
+          smtStatisticsRegistry().registerInt("z::approx::branchesMaxOnAVar")),
+      d_gaussianElimConstructTime(smtStatisticsRegistry().registerTimer(
+          "z::approx::gaussianElimConstruct::time")),
+      d_gaussianElimConstruct(smtStatisticsRegistry().registerInt(
+          "z::approx::gaussianElimConstruct::calls")),
+      d_averageGuesses(
+          smtStatisticsRegistry().registerAverage("z::approx::averageGuesses"))
 {
-  smtStatisticsRegistry()->registerStat(&d_branchMaxDepth);
-  smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar);
-
-  smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime);
-  smtStatisticsRegistry()->registerStat(&d_gaussianElimConstruct);
-
-  smtStatisticsRegistry()->registerStat(&d_averageGuesses);
-}
-
-ApproximateStatistics::~ApproximateStatistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth);
-  smtStatisticsRegistry()->unregisterStat(&d_branchesMaxOnAVar);
-
-  smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstructTime);
-  smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstruct);
-
-  smtStatisticsRegistry()->unregisterStat(&d_averageGuesses);
 }
 
 Integer ApproximateSimplex::s_defaultMaxDenom(1<<26);
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index f7266c578..aeced6f10 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -26,8 +26,7 @@
 #include "util/dense_map.h"
 #include "util/maybe.h"
 #include "util/rational.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -53,7 +52,6 @@ std::ostream& operator<<(std::ostream& out, MipResult res);
 class ApproximateStatistics {
  public:
   ApproximateStatistics();
-  ~ApproximateStatistics();
 
   IntStat d_branchMaxDepth;
   IntStat d_branchesMaxOnAVar;
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index d434315a3..07582f222 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -45,17 +45,12 @@ ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
 ArithStaticLearner::~ArithStaticLearner(){
 }
 
-ArithStaticLearner::Statistics::Statistics():
-  d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
-  d_iteConstantApplications("theory::arith::iteConstantApplications", 0)
+ArithStaticLearner::Statistics::Statistics()
+    : d_iteMinMaxApplications(smtStatisticsRegistry().registerInt(
+        "theory::arith::iteMinMaxApplications")),
+      d_iteConstantApplications(smtStatisticsRegistry().registerInt(
+          "theory::arith::iteConstantApplications"))
 {
-  smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications);
-  smtStatisticsRegistry()->registerStat(&d_iteConstantApplications);
-}
-
-ArithStaticLearner::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_iteMinMaxApplications);
-  smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications);
 }
 
 void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned)
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 053730ec8..7ff674b25 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -24,7 +24,7 @@
 #include "context/cdhashmap.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace context {
@@ -66,7 +66,6 @@ public:
     IntStat d_iteConstantApplications;
 
     Statistics();
-    ~Statistics();
   };
 
   Statistics d_statistics;
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index ccad9d866..d74385d3b 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -36,20 +36,14 @@ AttemptSolutionSDP::AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& er
   , d_statistics()
 { }
 
-AttemptSolutionSDP::Statistics::Statistics():
-  d_searchTime("theory::arith::attempt::searchTime"),
-  d_queueTime("theory::arith::attempt::queueTime"),
-  d_conflicts("theory::arith::attempt::conflicts", 0)
+AttemptSolutionSDP::Statistics::Statistics()
+    : d_searchTime(smtStatisticsRegistry().registerTimer(
+        "theory::arith::attempt::searchTime")),
+      d_queueTime(smtStatisticsRegistry().registerTimer(
+          "theory::arith::attempt::queueTime")),
+      d_conflicts(smtStatisticsRegistry().registerInt(
+          "theory::arith::attempt::conflicts"))
 {
-  smtStatisticsRegistry()->registerStat(&d_searchTime);
-  smtStatisticsRegistry()->registerStat(&d_queueTime);
-  smtStatisticsRegistry()->registerStat(&d_conflicts);
-}
-
-AttemptSolutionSDP::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_searchTime);
-  smtStatisticsRegistry()->unregisterStat(&d_queueTime);
-  smtStatisticsRegistry()->unregisterStat(&d_conflicts);
 }
 
 bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{
diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 25676a8b6..8c6b28b60 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -55,9 +55,9 @@
 
 #pragma once
 
-#include "theory/arith/simplex.h"
 #include "theory/arith/approx_simplex.h"
-#include "util/statistics_registry.h"
+#include "theory/arith/simplex.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -87,7 +87,6 @@ public:
     IntStat d_conflicts;
 
     Statistics();
-    ~Statistics();
   } d_statistics;
 };/* class AttemptSolutionSDP */
 
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index ff0b46338..23bdb20f6 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -90,32 +90,22 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee,
   d_pfee = pfee;
 }
 
-ArithCongruenceManager::Statistics::Statistics():
-  d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
-  d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
-  d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
-  d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
-  d_propagations("theory::arith::congruence::propagations", 0),
-  d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
-  d_conflicts("theory::arith::congruence::conflicts", 0)
+ArithCongruenceManager::Statistics::Statistics()
+    : d_watchedVariables(smtStatisticsRegistry().registerInt(
+        "theory::arith::congruence::watchedVariables")),
+      d_watchedVariableIsZero(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::watchedVariableIsZero")),
+      d_watchedVariableIsNotZero(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::watchedVariableIsNotZero")),
+      d_equalsConstantCalls(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::equalsConstantCalls")),
+      d_propagations(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::propagations")),
+      d_propagateConstraints(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::propagateConstraints")),
+      d_conflicts(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::conflicts"))
 {
-  smtStatisticsRegistry()->registerStat(&d_watchedVariables);
-  smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero);
-  smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero);
-  smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls);
-  smtStatisticsRegistry()->registerStat(&d_propagations);
-  smtStatisticsRegistry()->registerStat(&d_propagateConstraints);
-  smtStatisticsRegistry()->registerStat(&d_conflicts);
-}
-
-ArithCongruenceManager::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_watchedVariables);
-  smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero);
-  smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero);
-  smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_propagations);
-  smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints);
-  smtStatisticsRegistry()->unregisterStat(&d_conflicts);
 }
 
 ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index c8abba880..6032adcc8 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -24,14 +24,14 @@
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
 #include "context/cdtrail_queue.h"
-#include "theory/arith/arithvar.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/callbacks.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/trust_node.h"
 #include "theory/uf/equality_engine_notify.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -291,7 +291,6 @@ private:
     IntStat d_conflicts;
 
     Statistics();
-    ~Statistics();
   } d_statistics;
 
 };/* class ArithCongruenceManager */
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index eb2078c11..dcd699d88 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1003,18 +1003,12 @@ ConstraintDatabase::~ConstraintDatabase(){
   Assert(d_nodetoConstraintMap.empty());
 }
 
-ConstraintDatabase::Statistics::Statistics():
-  d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
-  d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
+ConstraintDatabase::Statistics::Statistics()
+    : d_unatePropagateCalls(smtStatisticsRegistry().registerInt(
+        "theory::arith::cd::unatePropagateCalls")),
+      d_unatePropagateImplications(smtStatisticsRegistry().registerInt(
+          "theory::arith::cd::unatePropagateImplications"))
 {
-  smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls);
-  smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications);
-
-}
-
-ConstraintDatabase::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications);
 }
 
 void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index bd27c6034..ecd5b10fb 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -92,7 +92,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/trust_node.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -1270,7 +1270,6 @@ private:
     IntStat d_unatePropagateImplications;
 
     Statistics();
-    ~Statistics();
   } d_statistics;
 
 }; /* ConstraintDatabase */
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index c54af4eed..1ad23f8ca 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -54,33 +54,19 @@ DioSolver::DioSolver(context::Context* ctxt)
       d_pureSubstitionIter(ctxt, 0),
       d_decompositionLemmaQueue(ctxt) {}
 
-DioSolver::Statistics::Statistics() :
-  d_conflictCalls("theory::arith::dio::conflictCalls",0),
-  d_cutCalls("theory::arith::dio::cutCalls",0),
-  d_cuts("theory::arith::dio::cuts",0),
-  d_conflicts("theory::arith::dio::conflicts",0),
-  d_conflictTimer("theory::arith::dio::conflictTimer"),
-  d_cutTimer("theory::arith::dio::cutTimer")
+DioSolver::Statistics::Statistics()
+    : d_conflictCalls(smtStatisticsRegistry().registerInt(
+        "theory::arith::dio::conflictCalls")),
+      d_cutCalls(
+          smtStatisticsRegistry().registerInt("theory::arith::dio::cutCalls")),
+      d_cuts(smtStatisticsRegistry().registerInt("theory::arith::dio::cuts")),
+      d_conflicts(
+          smtStatisticsRegistry().registerInt("theory::arith::dio::conflicts")),
+      d_conflictTimer(smtStatisticsRegistry().registerTimer(
+          "theory::arith::dio::conflictTimer")),
+      d_cutTimer(
+          smtStatisticsRegistry().registerTimer("theory::arith::dio::cutTimer"))
 {
-  smtStatisticsRegistry()->registerStat(&d_conflictCalls);
-  smtStatisticsRegistry()->registerStat(&d_cutCalls);
-
-  smtStatisticsRegistry()->registerStat(&d_cuts);
-  smtStatisticsRegistry()->registerStat(&d_conflicts);
-
-  smtStatisticsRegistry()->registerStat(&d_conflictTimer);
-  smtStatisticsRegistry()->registerStat(&d_cutTimer);
-}
-
-DioSolver::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_conflictCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_cutCalls);
-
-  smtStatisticsRegistry()->unregisterStat(&d_cuts);
-  smtStatisticsRegistry()->unregisterStat(&d_conflicts);
-
-  smtStatisticsRegistry()->unregisterStat(&d_conflictTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_cutTimer);
 }
 
 bool DioSolver::queueConditions(TrailIndex t){
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 5e020d66e..0fac563bb 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -28,8 +28,7 @@
 #include "context/cdqueue.h"
 #include "theory/arith/normal_form.h"
 #include "util/rational.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace context {
@@ -413,7 +412,6 @@ public:
     TimerStat d_cutTimer;
 
     Statistics();
-    ~Statistics();
   };
 
   Statistics d_statistics;
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 26bde0f62..13cc29a58 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -35,29 +35,21 @@ DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(LinearEqualityModule&
   , d_statistics(d_pivots)
 { }
 
-DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
-  d_statUpdateConflicts("theory::arith::dual::UpdateConflicts", 0),
-  d_processSignalsTime("theory::arith::dual::findConflictOnTheQueueTime"),
-  d_simplexConflicts("theory::arith::dual::simplexConflicts",0),
-  d_recentViolationCatches("theory::arith::dual::recentViolationCatches",0),
-  d_searchTime("theory::arith::dual::searchTime"),
-  d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots)
+DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots)
+    : d_statUpdateConflicts(smtStatisticsRegistry().registerInt(
+        "theory::arith::dual::UpdateConflicts")),
+      d_processSignalsTime(smtStatisticsRegistry().registerTimer(
+          "theory::arith::dual::findConflictOnTheQueueTime")),
+      d_simplexConflicts(smtStatisticsRegistry().registerInt(
+          "theory::arith::dual::simplexConflicts")),
+      d_recentViolationCatches(smtStatisticsRegistry().registerInt(
+          "theory::arith::dual::recentViolationCatches")),
+      d_searchTime(smtStatisticsRegistry().registerTimer(
+          "theory::arith::dual::searchTime")),
+      d_finalCheckPivotCounter(
+          smtStatisticsRegistry().registerReference<uint32_t>(
+              "theory::arith::dual::lastPivots", pivots))
 {
-  smtStatisticsRegistry()->registerStat(&d_statUpdateConflicts);
-  smtStatisticsRegistry()->registerStat(&d_processSignalsTime);
-  smtStatisticsRegistry()->registerStat(&d_simplexConflicts);
-  smtStatisticsRegistry()->registerStat(&d_recentViolationCatches);
-  smtStatisticsRegistry()->registerStat(&d_searchTime);
-  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
-}
-
-DualSimplexDecisionProcedure::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_statUpdateConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_processSignalsTime);
-  smtStatisticsRegistry()->unregisterStat(&d_simplexConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_recentViolationCatches);
-  smtStatisticsRegistry()->unregisterStat(&d_searchTime);
-  smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
 }
 
 Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index 7113bd329..e1021d2a5 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -56,7 +56,7 @@
 #pragma once
 
 #include "theory/arith/simplex.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -108,7 +108,6 @@ private:
     ReferenceStat<uint32_t> d_finalCheckPivotCounter;
 
     Statistics(uint32_t& pivots);
-    ~Statistics();
   } d_statistics;
 };/* class DualSimplexDecisionProcedure */
 
diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp
index c397efb9a..b7c35a7fd 100644
--- a/src/theory/arith/error_set.cpp
+++ b/src/theory/arith/error_set.cpp
@@ -128,29 +128,20 @@ void ErrorInformation::setAmount(const DeltaRational& am){
   (*d_amount) = am;
 }
 
-ErrorSet::Statistics::Statistics():
-  d_enqueues("theory::arith::pqueue::enqueues", 0),
-  d_enqueuesCollection("theory::arith::pqueue::enqueuesCollection", 0),
-  d_enqueuesDiffMode("theory::arith::pqueue::enqueuesDiffMode", 0),
-  d_enqueuesVarOrderMode("theory::arith::pqueue::enqueuesVarOrderMode", 0),
-  d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0),
-  d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0)
+ErrorSet::Statistics::Statistics()
+    : d_enqueues(
+        smtStatisticsRegistry().registerInt("theory::arith::pqueue::enqueues")),
+      d_enqueuesCollection(smtStatisticsRegistry().registerInt(
+          "theory::arith::pqueue::enqueuesCollection")),
+      d_enqueuesDiffMode(smtStatisticsRegistry().registerInt(
+          "theory::arith::pqueue::enqueuesDiffMode")),
+      d_enqueuesVarOrderMode(smtStatisticsRegistry().registerInt(
+          "theory::arith::pqueue::enqueuesVarOrderMode")),
+      d_enqueuesCollectionDuplicates(smtStatisticsRegistry().registerInt(
+          "theory::arith::pqueue::enqueuesCollectionDuplicates")),
+      d_enqueuesVarOrderModeDuplicates(smtStatisticsRegistry().registerInt(
+          "theory::arith::pqueue::enqueuesVarOrderModeDuplicates"))
 {
-  smtStatisticsRegistry()->registerStat(&d_enqueues);
-  smtStatisticsRegistry()->registerStat(&d_enqueuesCollection);
-  smtStatisticsRegistry()->registerStat(&d_enqueuesDiffMode);
-  smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderMode);
-  smtStatisticsRegistry()->registerStat(&d_enqueuesCollectionDuplicates);
-  smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderModeDuplicates);
-}
-
-ErrorSet::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_enqueues);
-  smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollection);
-  smtStatisticsRegistry()->unregisterStat(&d_enqueuesDiffMode);
-  smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderMode);
-  smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollectionDuplicates);
-  smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates);
 }
 
 ErrorSet::ErrorSet(ArithVariables& vars,
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 21cc557b6..5585bf76f 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -30,7 +30,7 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau_sizes.h"
 #include "util/bin_heap.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -407,7 +407,6 @@ private:
     IntStat d_enqueuesVarOrderModeDuplicates;
 
     Statistics();
-    ~Statistics();
   };
 
   Statistics d_statistics;
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 6ab5c05d7..de13f4eb9 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -20,7 +20,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 using namespace std;
 
@@ -28,62 +28,42 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-
-FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
-  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
-  , d_focusSize(0)
-  , d_focusErrorVar(ARITHVAR_SENTINEL)
-  , d_focusCoefficients()
-  , d_pivotBudget(0)
-  , d_prevWitnessImprovement(AntiProductive)
-  , d_witnessImprovementInARow(0)
-  , d_sgnDisagreements()
-  , d_statistics(d_pivots)
+FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(
+    LinearEqualityModule& linEq,
+    ErrorSet& errors,
+    RaiseConflict conflictChannel,
+    TempVarMalloc tvmalloc)
+    : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc),
+      d_focusSize(0),
+      d_focusErrorVar(ARITHVAR_SENTINEL),
+      d_focusCoefficients(),
+      d_pivotBudget(0),
+      d_prevWitnessImprovement(AntiProductive),
+      d_witnessImprovementInARow(0),
+      d_sgnDisagreements(),
+      d_statistics("theory::arith::FC::", d_pivots)
 { }
 
-FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
-  d_initialSignalsTime("theory::arith::FC::initialProcessTime"),
-  d_initialConflicts("theory::arith::FC::UpdateConflicts", 0),
-  d_fcFoundUnsat("theory::arith::FC::FoundUnsat", 0),
-  d_fcFoundSat("theory::arith::FC::FoundSat", 0),
-  d_fcMissed("theory::arith::FC::Missed", 0),
-  d_fcTimer("theory::arith::FC::Timer"),
-  d_fcFocusConstructionTimer("theory::arith::FC::Construction"),
-  d_selectUpdateForDualLike("theory::arith::FC::selectUpdateForDualLike"),
-  d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"),
-  d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots)
+FCSimplexDecisionProcedure::Statistics::Statistics(const std::string& name,
+                                                   uint32_t& pivots)
+    : d_initialSignalsTime(
+        smtStatisticsRegistry().registerTimer(name + "initialProcessTime")),
+      d_initialConflicts(
+          smtStatisticsRegistry().registerInt(name + "UpdateConflicts")),
+      d_fcFoundUnsat(smtStatisticsRegistry().registerInt(name + "FoundUnsat")),
+      d_fcFoundSat(smtStatisticsRegistry().registerInt(name + "FoundSat")),
+      d_fcMissed(smtStatisticsRegistry().registerInt(name + "Missed")),
+      d_fcTimer(smtStatisticsRegistry().registerTimer(name + "Timer")),
+      d_fcFocusConstructionTimer(
+          smtStatisticsRegistry().registerTimer(name + "Construction")),
+      d_selectUpdateForDualLike(smtStatisticsRegistry().registerTimer(
+          name + "selectUpdateForDualLike")),
+      d_selectUpdateForPrimal(smtStatisticsRegistry().registerTimer(
+          name + "selectUpdateForPrimal")),
+      d_finalCheckPivotCounter(
+          smtStatisticsRegistry().registerReference<uint32_t>(
+              name + "lastPivots", pivots))
 {
-  smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
-  smtStatisticsRegistry()->registerStat(&d_initialConflicts);
-
-  smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat);
-  smtStatisticsRegistry()->registerStat(&d_fcFoundSat);
-  smtStatisticsRegistry()->registerStat(&d_fcMissed);
-
-  smtStatisticsRegistry()->registerStat(&d_fcTimer);
-  smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer);
-
-  smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike);
-  smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal);
-
-  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
-}
-
-FCSimplexDecisionProcedure::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
-  smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
-
-  smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat);
-  smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat);
-  smtStatisticsRegistry()->unregisterStat(&d_fcMissed);
-
-  smtStatisticsRegistry()->unregisterStat(&d_fcTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer);
-
-  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike);
-  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal);
-
-  smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
 }
 
 Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 6c391393d..599b324ce 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -60,7 +60,7 @@
 #include "theory/arith/simplex.h"
 #include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -250,8 +250,7 @@ private:
 
     ReferenceStat<uint32_t> d_finalCheckPivotCounter;
 
-    Statistics(uint32_t& pivots);
-    ~Statistics();
+    Statistics(const std::string& name, uint32_t& pivots);
   } d_statistics;
 };/* class FCSimplexDecisionProcedure */
 
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 25364fc24..90c17be4a 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -27,7 +27,7 @@ namespace arith {
 InferenceManager::InferenceManager(TheoryArith& ta,
                                    ArithState& astate,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith")
+    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::")
 {
 }
 
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index c9d65a0fc..57dbdfc82 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -65,42 +65,26 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou
   d_trackCallback(this)
 {}
 
-LinearEqualityModule::Statistics::Statistics():
-  d_statPivots("theory::arith::pivots",0),
-  d_statUpdates("theory::arith::updates",0),
-  d_pivotTime("theory::arith::pivotTime"),
-  d_adjTime("theory::arith::adjTime"),
-  d_weakeningAttempts("theory::arith::weakening::attempts",0),
-  d_weakeningSuccesses("theory::arith::weakening::success",0),
-  d_weakenings("theory::arith::weakening::total",0),
-  d_weakenTime("theory::arith::weakening::time"),
-  d_forceTime("theory::arith::forcing::time")
+LinearEqualityModule::Statistics::Statistics()
+    : d_statPivots(
+        smtStatisticsRegistry().registerInt("theory::arith::pivots")),
+      d_statUpdates(
+          smtStatisticsRegistry().registerInt("theory::arith::updates")),
+      d_pivotTime(
+          smtStatisticsRegistry().registerTimer("theory::arith::pivotTime")),
+      d_adjTime(
+          smtStatisticsRegistry().registerTimer("theory::arith::adjTime")),
+      d_weakeningAttempts(smtStatisticsRegistry().registerInt(
+          "theory::arith::weakening::attempts")),
+      d_weakeningSuccesses(smtStatisticsRegistry().registerInt(
+          "theory::arith::weakening::success")),
+      d_weakenings(smtStatisticsRegistry().registerInt(
+          "theory::arith::weakening::total")),
+      d_weakenTime(smtStatisticsRegistry().registerTimer(
+          "theory::arith::weakening::time")),
+      d_forceTime(
+          smtStatisticsRegistry().registerTimer("theory::arith::forcing::time"))
 {
-  smtStatisticsRegistry()->registerStat(&d_statPivots);
-  smtStatisticsRegistry()->registerStat(&d_statUpdates);
-
-  smtStatisticsRegistry()->registerStat(&d_pivotTime);
-  smtStatisticsRegistry()->registerStat(&d_adjTime);
-
-  smtStatisticsRegistry()->registerStat(&d_weakeningAttempts);
-  smtStatisticsRegistry()->registerStat(&d_weakeningSuccesses);
-  smtStatisticsRegistry()->registerStat(&d_weakenings);
-  smtStatisticsRegistry()->registerStat(&d_weakenTime);
-  smtStatisticsRegistry()->registerStat(&d_forceTime);
-}
-
-LinearEqualityModule::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_statPivots);
-  smtStatisticsRegistry()->unregisterStat(&d_statUpdates);
-  smtStatisticsRegistry()->unregisterStat(&d_pivotTime);
-  smtStatisticsRegistry()->unregisterStat(&d_adjTime);
-
-
-  smtStatisticsRegistry()->unregisterStat(&d_weakeningAttempts);
-  smtStatisticsRegistry()->unregisterStat(&d_weakeningSuccesses);
-  smtStatisticsRegistry()->unregisterStat(&d_weakenings);
-  smtStatisticsRegistry()->unregisterStat(&d_weakenTime);
-  smtStatisticsRegistry()->unregisterStat(&d_forceTime);
 }
 
 void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index e07ed6051..276c8e63e 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -38,8 +38,7 @@
 #include "theory/arith/simplex_update.h"
 #include "theory/arith/tableau.h"
 #include "util/maybe.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -714,7 +713,6 @@ private:
     TimerStat d_forceTime;
 
     Statistics();
-    ~Statistics();
   };
   mutable Statistics d_statistics;
 
diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp
index fa06fa73e..b20214f59 100644
--- a/src/theory/arith/nl/stats.cpp
+++ b/src/theory/arith/nl/stats.cpp
@@ -23,17 +23,9 @@ namespace arith {
 namespace nl {
 
 NlStats::NlStats()
-    : d_mbrRuns("nl::mbrRuns", 0),
-      d_checkRuns("nl::checkRuns", 0)
+    : d_mbrRuns(smtStatisticsRegistry().registerInt("nl::mbrRuns")),
+      d_checkRuns(smtStatisticsRegistry().registerInt("nl::checkRuns"))
 {
-  smtStatisticsRegistry()->registerStat(&d_mbrRuns);
-  smtStatisticsRegistry()->registerStat(&d_checkRuns);
-}
-
-NlStats::~NlStats()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_mbrRuns);
-  smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
 }
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index 988b647a6..4f30031be 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -18,7 +18,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__STATS_H
 #define CVC5__THEORY__ARITH__NL__STATS_H
 
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -32,7 +32,6 @@ class NlStats
 {
  public:
   NlStats();
-  ~NlStats();
   /**
    * Number of calls to NonlinearExtension::modelBasedRefinement. Notice this
    * may make multiple calls to NonlinearExtension::checkLastCall.
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 88816b311..781f132d7 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -22,6 +22,7 @@
 #include "theory/arith/error_set.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/tableau.h"
+#include "util/statistics_value.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 9cbb5bac2..fe5b26eaa 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -62,8 +62,7 @@
 #include "theory/arith/partial_model.h"
 #include "util/dense_map.h"
 #include "util/result.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index fc1e06441..1b22bc81c 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -23,7 +23,7 @@
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
 #include "theory/arith/tableau.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 using namespace std;
 
@@ -31,72 +31,45 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-
-SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
-  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
-  , d_soiVar(ARITHVAR_SENTINEL)
-  , d_pivotBudget(0)
-  , d_prevWitnessImprovement(AntiProductive)
-  , d_witnessImprovementInARow(0)
-  , d_sgnDisagreements()
-  , d_statistics(d_pivots)
+SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq,
+                                                 ErrorSet& errors,
+                                                 RaiseConflict conflictChannel,
+                                                 TempVarMalloc tvmalloc)
+    : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc),
+      d_soiVar(ARITHVAR_SENTINEL),
+      d_pivotBudget(0),
+      d_prevWitnessImprovement(AntiProductive),
+      d_witnessImprovementInARow(0),
+      d_sgnDisagreements(),
+      d_statistics("theory::arith::SOI", d_pivots)
 { }
 
-SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots):
-  d_initialSignalsTime("theory::arith::SOI::initialProcessTime"),
-  d_initialConflicts("theory::arith::SOI::UpdateConflicts", 0),
-  d_soiFoundUnsat("theory::arith::SOI::FoundUnsat", 0),
-  d_soiFoundSat("theory::arith::SOI::FoundSat", 0),
-  d_soiMissed("theory::arith::SOI::Missed", 0),
-  d_soiConflicts("theory::arith::SOI::ConfMin::num", 0),
-  d_hasToBeMinimal("theory::arith::SOI::HasToBeMin", 0),
-  d_maybeNotMinimal("theory::arith::SOI::MaybeNotMin", 0),
-  d_soiTimer("theory::arith::SOI::Time"),
-  d_soiFocusConstructionTimer("theory::arith::SOI::Construction"),
-  d_soiConflictMinimization("theory::arith::SOI::Conflict::Minimization"),
-  d_selectUpdateForSOI("theory::arith::SOI::selectSOI"),
-  d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots)
+SumOfInfeasibilitiesSPD::Statistics::Statistics(const std::string& name,
+                                                uint32_t& pivots)
+    : d_initialSignalsTime(
+        smtStatisticsRegistry().registerTimer(name + "initialProcessTime")),
+      d_initialConflicts(
+          smtStatisticsRegistry().registerInt(name + "UpdateConflicts")),
+      d_soiFoundUnsat(smtStatisticsRegistry().registerInt(name + "FoundUnsat")),
+      d_soiFoundSat(smtStatisticsRegistry().registerInt(name + "FoundSat")),
+      d_soiMissed(smtStatisticsRegistry().registerInt(name + "Missed")),
+      d_soiConflicts(
+          smtStatisticsRegistry().registerInt(name + "ConfMin::num")),
+      d_hasToBeMinimal(
+          smtStatisticsRegistry().registerInt(name + "HasToBeMin")),
+      d_maybeNotMinimal(
+          smtStatisticsRegistry().registerInt(name + "MaybeNotMin")),
+      d_soiTimer(smtStatisticsRegistry().registerTimer(name + "Time")),
+      d_soiFocusConstructionTimer(
+          smtStatisticsRegistry().registerTimer(name + "Construction")),
+      d_soiConflictMinimization(smtStatisticsRegistry().registerTimer(
+          name + "Conflict::Minimization")),
+      d_selectUpdateForSOI(
+          smtStatisticsRegistry().registerTimer(name + "selectSOI")),
+      d_finalCheckPivotCounter(
+          smtStatisticsRegistry().registerReference<uint32_t>(
+              name + "lastPivots", pivots))
 {
-  smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
-  smtStatisticsRegistry()->registerStat(&d_initialConflicts);
-
-  smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat);
-  smtStatisticsRegistry()->registerStat(&d_soiFoundSat);
-  smtStatisticsRegistry()->registerStat(&d_soiMissed);
-
-  smtStatisticsRegistry()->registerStat(&d_soiConflicts);
-  smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal);
-  smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal);
-
-  smtStatisticsRegistry()->registerStat(&d_soiTimer);
-  smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer);
-
-  smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization);
-
-  smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI);
-
-  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
-}
-
-SumOfInfeasibilitiesSPD::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
-  smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
-
-  smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat);
-  smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat);
-  smtStatisticsRegistry()->unregisterStat(&d_soiMissed);
-
-  smtStatisticsRegistry()->unregisterStat(&d_soiConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal);
-  smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal);
-
-  smtStatisticsRegistry()->unregisterStat(&d_soiTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer);
-
-  smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization);
-
-  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForSOI);
-  smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
 }
 
 Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 7b2656752..5bff01d99 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -59,7 +59,7 @@
 #include "theory/arith/simplex.h"
 #include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -236,8 +236,7 @@ private:
 
     ReferenceStat<uint32_t> d_finalCheckPivotCounter;
 
-    Statistics(uint32_t& pivots);
-    ~Statistics();
+    Statistics(const std::string& name, uint32_t& pivots);
   } d_statistics;
 };/* class FCSimplexDecisionProcedure */
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4232d28dc..181a816c2 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -43,22 +43,20 @@ TheoryArith::TheoryArith(context::Context* c,
     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
       d_internal(
           new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
-      d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
+      d_ppRewriteTimer(smtStatisticsRegistry().registerTimer(
+          "theory::arith::ppRewriteTimer")),
       d_ppPfGen(pnm, c, "Arith::ppRewrite"),
       d_astate(*d_internal, c, u, valuation),
       d_im(*this, d_astate, pnm),
       d_nonlinearExtension(nullptr),
       d_arithPreproc(d_astate, d_im, pnm, logicInfo)
 {
-  smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
-
   // indicate we are using the theory state object and inference manager
   d_theoryState = &d_astate;
   d_inferManager = &d_im;
 }
 
 TheoryArith::~TheoryArith(){
-  smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer);
   delete d_internal;
 }
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 9a13944f3..e7ff27413 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -72,7 +72,7 @@
 #include "util/random.h"
 #include "util/rational.h"
 #include "util/result.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -171,7 +171,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_solveIntAttempts(0u),
       d_newFacts(false),
       d_previousStatus(Result::SAT_UNKNOWN),
-      d_statistics()
+      d_statistics("theory::arith::")
 {
 }
 
@@ -254,265 +254,154 @@ TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg)
 }
 TheoryArithPrivate::ModelException::~ModelException() {}
 
-TheoryArithPrivate::Statistics::Statistics()
-  : d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0)
-  , d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0)
-  , d_statUserVariables("theory::arith::UserVariables", 0)
-  , d_statAuxiliaryVariables("theory::arith::AuxiliaryVariables", 0)
-  , d_statDisequalitySplits("theory::arith::DisequalitySplits", 0)
-  , d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0)
-  , d_simplifyTimer("theory::arith::simplifyTimer")
-  , d_staticLearningTimer("theory::arith::staticLearningTimer")
-  , d_presolveTime("theory::arith::presolveTime")
-  , d_newPropTime("theory::arith::newPropTimer")
-  , d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0)
-  , d_initialTableauSize("theory::arith::initialTableauSize", 0)
-  , d_currSetToSmaller("theory::arith::currSetToSmaller", 0)
-  , d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0)
-  , d_restartTimer("theory::arith::restartTimer")
-  , d_boundComputationTime("theory::arith::bound::time")
-  , d_boundComputations("theory::arith::bound::boundComputations",0)
-  , d_boundPropagations("theory::arith::bound::boundPropagations",0)
-  , d_unknownChecks("theory::arith::status::unknowns", 0)
-  , d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0)
-  , d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow")
-  , d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0)
-  , d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0)
-  , d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
-  , d_replayLogRecCount("theory::arith::z::approx::replay::rec",0)
-  , d_replayLogRecConflictEscalation("theory::arith::z::approx::replay::rec::escalation",0)
-  , d_replayLogRecEarlyExit("theory::arith::z::approx::replay::rec::earlyexit",0)
-  , d_replayBranchCloseFailures("theory::arith::z::approx::replay::rec::branch::closefailures",0)
-  , d_replayLeafCloseFailures("theory::arith::z::approx::replay::rec::leaf::closefailures",0)
-  , d_replayBranchSkips("theory::arith::z::approx::replay::rec::branch::skips",0)
-  , d_mirCutsAttempted("theory::arith::z::approx::cuts::mir::attempted",0)
-  , d_gmiCutsAttempted("theory::arith::z::approx::cuts::gmi::attempted",0)
-  , d_branchCutsAttempted("theory::arith::z::approx::cuts::branch::attempted",0)
-  , d_cutsReconstructed("theory::arith::z::approx::cuts::reconstructed",0)
-  , d_cutsReconstructionFailed("theory::arith::z::approx::cuts::reconstructed::failed",0)
-  , d_cutsProven("theory::arith::z::approx::cuts::proofs",0)
-  , d_cutsProofFailed("theory::arith::z::approx::cuts::proofs::failed",0)
-  , d_mipReplayLemmaCalls("theory::arith::z::approx::external::calls",0)
-  , d_mipExternalCuts("theory::arith::z::approx::external::cuts",0)
-  , d_mipExternalBranch("theory::arith::z::approx::external::branches",0)
-  , d_inSolveInteger("theory::arith::z::approx::inSolverInteger",0)
-  , d_branchesExhausted("theory::arith::z::approx::exhausted::branches",0)
-  , d_execExhausted("theory::arith::z::approx::exhausted::exec",0)
-  , d_pivotsExhausted("theory::arith::z::approx::exhausted::pivots",0)
-  , d_panicBranches("theory::arith::z::arith::paniclemmas",0)
-  , d_relaxCalls("theory::arith::z::arith::relax::calls",0)
-  , d_relaxLinFeas("theory::arith::z::arith::relax::feasible::res",0)
-  , d_relaxLinFeasFailures("theory::arith::z::arith::relax::feasible::failures",0)
-  , d_relaxLinInfeas("theory::arith::z::arith::relax::infeasible",0)
-  , d_relaxLinInfeasFailures("theory::arith::z::arith::relax::infeasible::failures",0)
-  , d_relaxLinExhausted("theory::arith::z::arith::relax::exhausted",0)
-  , d_relaxOthers("theory::arith::z::arith::relax::other",0)
-  , d_applyRowsDeleted("theory::arith::z::arith::cuts::applyRowsDeleted",0)
-  , d_replaySimplexTimer("theory::arith::z::approx::replay::simplex::timer")
-  , d_replayLogTimer("theory::arith::z::approx::replay::log::timer")
-  , d_solveIntTimer("theory::arith::z::solveInt::timer")
-  , d_solveRealRelaxTimer("theory::arith::z::solveRealRelax::timer")
-  , d_solveIntCalls("theory::arith::z::solveInt::calls", 0)
-  , d_solveStandardEffort("theory::arith::z::solveInt::calls::standardEffort", 0)
-  , d_approxDisabled("theory::arith::z::approxDisabled", 0)
-  , d_replayAttemptFailed("theory::arith::z::replayAttemptFailed",0)
-  , d_cutsRejectedDuringReplay("theory::arith::z::approx::replay::cuts::rejected", 0)
-  , d_cutsRejectedDuringLemmas("theory::arith::z::approx::external::cuts::rejected", 0)
-  , d_satPivots("theory::arith::pivots::sat")
-  , d_unsatPivots("theory::arith::pivots::unsat")
-  , d_unknownPivots("theory::arith::pivots::unknown")
-  , d_solveIntModelsAttempts("theory::arith::z::solveInt::models::attempts", 0)
-  , d_solveIntModelsSuccessful("theory::arith::zzz::solveInt::models::successful", 0)
-  , d_mipTimer("theory::arith::z::approx::mip::timer")
-  , d_lpTimer("theory::arith::z::approx::lp::timer")
-  , d_mipProofsAttempted("theory::arith::z::mip::proofs::attempted", 0)
-  , d_mipProofsSuccessful("theory::arith::z::mip::proofs::successful", 0)
-  , d_numBranchesFailed("theory::arith::z::mip::branch::proof::failed", 0)
+TheoryArithPrivate::Statistics::Statistics(const std::string& name)
+    : d_statAssertUpperConflicts(
+        smtStatisticsRegistry().registerInt(name + "AssertUpperConflicts")),
+      d_statAssertLowerConflicts(
+          smtStatisticsRegistry().registerInt(name + "AssertLowerConflicts")),
+      d_statUserVariables(
+          smtStatisticsRegistry().registerInt(name + "UserVariables")),
+      d_statAuxiliaryVariables(
+          smtStatisticsRegistry().registerInt(name + "AuxiliaryVariables")),
+      d_statDisequalitySplits(
+          smtStatisticsRegistry().registerInt(name + "DisequalitySplits")),
+      d_statDisequalityConflicts(
+          smtStatisticsRegistry().registerInt(name + "DisequalityConflicts")),
+      d_simplifyTimer(
+          smtStatisticsRegistry().registerTimer(name + "simplifyTimer")),
+      d_staticLearningTimer(
+          smtStatisticsRegistry().registerTimer(name + "staticLearningTimer")),
+      d_presolveTime(
+          smtStatisticsRegistry().registerTimer(name + "presolveTime")),
+      d_newPropTime(
+          smtStatisticsRegistry().registerTimer(name + "newPropTimer")),
+      d_externalBranchAndBounds(smtStatisticsRegistry().registerInt(
+          name + "externalBranchAndBounds")),
+      d_initialTableauSize(
+          smtStatisticsRegistry().registerInt(name + "initialTableauSize")),
+      d_currSetToSmaller(
+          smtStatisticsRegistry().registerInt(name + "currSetToSmaller")),
+      d_smallerSetToCurr(
+          smtStatisticsRegistry().registerInt(name + "smallerSetToCurr")),
+      d_restartTimer(
+          smtStatisticsRegistry().registerTimer(name + "restartTimer")),
+      d_boundComputationTime(
+          smtStatisticsRegistry().registerTimer(name + "bound::time")),
+      d_boundComputations(smtStatisticsRegistry().registerInt(
+          name + "bound::boundComputations")),
+      d_boundPropagations(smtStatisticsRegistry().registerInt(
+          name + "bound::boundPropagations")),
+      d_unknownChecks(
+          smtStatisticsRegistry().registerInt(name + "status::unknowns")),
+      d_maxUnknownsInARow(smtStatisticsRegistry().registerInt(
+          name + "status::maxUnknownsInARow")),
+      d_avgUnknownsInARow(smtStatisticsRegistry().registerAverage(
+          name + "status::avgUnknownsInARow")),
+      d_revertsOnConflicts(smtStatisticsRegistry().registerInt(
+          name + "status::revertsOnConflicts")),
+      d_commitsOnConflicts(smtStatisticsRegistry().registerInt(
+          name + "status::commitsOnConflicts")),
+      d_nontrivialSatChecks(smtStatisticsRegistry().registerInt(
+          name + "status::nontrivialSatChecks")),
+      d_replayLogRecCount(
+          smtStatisticsRegistry().registerInt(name + "z::approx::replay::rec")),
+      d_replayLogRecConflictEscalation(smtStatisticsRegistry().registerInt(
+          name + "z::approx::replay::rec::escalation")),
+      d_replayLogRecEarlyExit(smtStatisticsRegistry().registerInt(
+          name + "z::approx::replay::rec::earlyexit")),
+      d_replayBranchCloseFailures(smtStatisticsRegistry().registerInt(
+          name + "z::approx::replay::rec::branch::closefailures")),
+      d_replayLeafCloseFailures(smtStatisticsRegistry().registerInt(
+          name + "z::approx::replay::rec::leaf::closefailures")),
+      d_replayBranchSkips(smtStatisticsRegistry().registerInt(
+          name + "z::approx::replay::rec::branch::skips")),
+      d_mirCutsAttempted(smtStatisticsRegistry().registerInt(
+          name + "z::approx::cuts::mir::attempted")),
+      d_gmiCutsAttempted(smtStatisticsRegistry().registerInt(
+          name + "z::approx::cuts::gmi::attempted")),
+      d_branchCutsAttempted(smtStatisticsRegistry().registerInt(
+          name + "z::approx::cuts::branch::attempted")),
+      d_cutsReconstructed(smtStatisticsRegistry().registerInt(
+          name + "z::approx::cuts::reconstructed")),
+      d_cutsReconstructionFailed(smtStatisticsRegistry().registerInt(
+          name + "z::approx::cuts::reconstructed::failed")),
+      d_cutsProven(smtStatisticsRegistry().registerInt(
+          name + "z::approx::cuts::proofs")),
+      d_cutsProofFailed(smtStatisticsRegistry().registerInt(
+          name + "z::approx::cuts::proofs::failed")),
+      d_mipReplayLemmaCalls(smtStatisticsRegistry().registerInt(
+          name + "z::approx::external::calls")),
+      d_mipExternalCuts(smtStatisticsRegistry().registerInt(
+          name + "z::approx::external::cuts")),
+      d_mipExternalBranch(smtStatisticsRegistry().registerInt(
+          name + "z::approx::external::branches")),
+      d_inSolveInteger(smtStatisticsRegistry().registerInt(
+          name + "z::approx::inSolverInteger")),
+      d_branchesExhausted(smtStatisticsRegistry().registerInt(
+          name + "z::approx::exhausted::branches")),
+      d_execExhausted(smtStatisticsRegistry().registerInt(
+          name + "z::approx::exhausted::exec")),
+      d_pivotsExhausted(smtStatisticsRegistry().registerInt(
+          name + "z::approx::exhausted::pivots")),
+      d_panicBranches(
+          smtStatisticsRegistry().registerInt(name + "z::arith::paniclemmas")),
+      d_relaxCalls(
+          smtStatisticsRegistry().registerInt(name + "z::arith::relax::calls")),
+      d_relaxLinFeas(smtStatisticsRegistry().registerInt(
+          name + "z::arith::relax::feasible::res")),
+      d_relaxLinFeasFailures(smtStatisticsRegistry().registerInt(
+          name + "z::arith::relax::feasible::failures")),
+      d_relaxLinInfeas(smtStatisticsRegistry().registerInt(
+          name + "z::arith::relax::infeasible")),
+      d_relaxLinInfeasFailures(smtStatisticsRegistry().registerInt(
+          name + "z::arith::relax::infeasible::failures")),
+      d_relaxLinExhausted(smtStatisticsRegistry().registerInt(
+          name + "z::arith::relax::exhausted")),
+      d_relaxOthers(
+          smtStatisticsRegistry().registerInt(name + "z::arith::relax::other")),
+      d_applyRowsDeleted(smtStatisticsRegistry().registerInt(
+          name + "z::arith::cuts::applyRowsDeleted")),
+      d_replaySimplexTimer(smtStatisticsRegistry().registerTimer(
+          name + "z::approx::replay::simplex::timer")),
+      d_replayLogTimer(smtStatisticsRegistry().registerTimer(
+          name + "z::approx::replay::log::timer")),
+      d_solveIntTimer(
+          smtStatisticsRegistry().registerTimer(name + "z::solveInt::timer")),
+      d_solveRealRelaxTimer(smtStatisticsRegistry().registerTimer(
+          name + "z::solveRealRelax::timer")),
+      d_solveIntCalls(
+          smtStatisticsRegistry().registerInt(name + "z::solveInt::calls")),
+      d_solveStandardEffort(smtStatisticsRegistry().registerInt(
+          name + "z::solveInt::calls::standardEffort")),
+      d_approxDisabled(
+          smtStatisticsRegistry().registerInt(name + "z::approxDisabled")),
+      d_replayAttemptFailed(
+          smtStatisticsRegistry().registerInt(name + "z::replayAttemptFailed")),
+      d_cutsRejectedDuringReplay(smtStatisticsRegistry().registerInt(
+          name + "z::approx::replay::cuts::rejected")),
+      d_cutsRejectedDuringLemmas(smtStatisticsRegistry().registerInt(
+          name + "z::approx::external::cuts::rejected")),
+      d_satPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
+          name + "pivots::sat")),
+      d_unsatPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
+          name + "pivots::unsat")),
+      d_unknownPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
+          name + "pivots::unknown")),
+      d_solveIntModelsAttempts(smtStatisticsRegistry().registerInt(
+          name + "z::solveInt::models::attempts")),
+      d_solveIntModelsSuccessful(smtStatisticsRegistry().registerInt(
+          name + "zzz::solveInt::models::successful")),
+      d_mipTimer(smtStatisticsRegistry().registerTimer(
+          name + "z::approx::mip::timer")),
+      d_lpTimer(
+          smtStatisticsRegistry().registerTimer(name + "z::approx::lp::timer")),
+      d_mipProofsAttempted(smtStatisticsRegistry().registerInt(
+          name + "z::mip::proofs::attempted")),
+      d_mipProofsSuccessful(smtStatisticsRegistry().registerInt(
+          name + "z::mip::proofs::successful")),
+      d_numBranchesFailed(smtStatisticsRegistry().registerInt(
+          name + "z::mip::branch::proof::failed"))
 {
-  smtStatisticsRegistry()->registerStat(&d_statAssertUpperConflicts);
-  smtStatisticsRegistry()->registerStat(&d_statAssertLowerConflicts);
-
-  smtStatisticsRegistry()->registerStat(&d_statUserVariables);
-  smtStatisticsRegistry()->registerStat(&d_statAuxiliaryVariables);
-  smtStatisticsRegistry()->registerStat(&d_statDisequalitySplits);
-  smtStatisticsRegistry()->registerStat(&d_statDisequalityConflicts);
-  smtStatisticsRegistry()->registerStat(&d_simplifyTimer);
-  smtStatisticsRegistry()->registerStat(&d_staticLearningTimer);
-
-  smtStatisticsRegistry()->registerStat(&d_presolveTime);
-  smtStatisticsRegistry()->registerStat(&d_newPropTime);
-
-  smtStatisticsRegistry()->registerStat(&d_externalBranchAndBounds);
-
-  smtStatisticsRegistry()->registerStat(&d_initialTableauSize);
-  smtStatisticsRegistry()->registerStat(&d_currSetToSmaller);
-  smtStatisticsRegistry()->registerStat(&d_smallerSetToCurr);
-  smtStatisticsRegistry()->registerStat(&d_restartTimer);
-
-  smtStatisticsRegistry()->registerStat(&d_boundComputationTime);
-  smtStatisticsRegistry()->registerStat(&d_boundComputations);
-  smtStatisticsRegistry()->registerStat(&d_boundPropagations);
-
-  smtStatisticsRegistry()->registerStat(&d_unknownChecks);
-  smtStatisticsRegistry()->registerStat(&d_maxUnknownsInARow);
-  smtStatisticsRegistry()->registerStat(&d_avgUnknownsInARow);
-  smtStatisticsRegistry()->registerStat(&d_revertsOnConflicts);
-  smtStatisticsRegistry()->registerStat(&d_commitsOnConflicts);
-  smtStatisticsRegistry()->registerStat(&d_nontrivialSatChecks);
-
-
-  smtStatisticsRegistry()->registerStat(&d_satPivots);
-  smtStatisticsRegistry()->registerStat(&d_unsatPivots);
-  smtStatisticsRegistry()->registerStat(&d_unknownPivots);
-
-  smtStatisticsRegistry()->registerStat(&d_replayLogRecCount);
-  smtStatisticsRegistry()->registerStat(&d_replayLogRecConflictEscalation);
-  smtStatisticsRegistry()->registerStat(&d_replayLogRecEarlyExit);
-  smtStatisticsRegistry()->registerStat(&d_replayBranchCloseFailures);
-  smtStatisticsRegistry()->registerStat(&d_replayLeafCloseFailures);
-  smtStatisticsRegistry()->registerStat(&d_replayBranchSkips);
-  smtStatisticsRegistry()->registerStat(&d_mirCutsAttempted);
-  smtStatisticsRegistry()->registerStat(&d_gmiCutsAttempted);
-  smtStatisticsRegistry()->registerStat(&d_branchCutsAttempted);
-  smtStatisticsRegistry()->registerStat(&d_cutsReconstructed);
-  smtStatisticsRegistry()->registerStat(&d_cutsProven);
-  smtStatisticsRegistry()->registerStat(&d_cutsProofFailed);
-  smtStatisticsRegistry()->registerStat(&d_cutsReconstructionFailed);
-  smtStatisticsRegistry()->registerStat(&d_mipReplayLemmaCalls);
-  smtStatisticsRegistry()->registerStat(&d_mipExternalCuts);
-  smtStatisticsRegistry()->registerStat(&d_mipExternalBranch);
-
-  smtStatisticsRegistry()->registerStat(&d_inSolveInteger);
-  smtStatisticsRegistry()->registerStat(&d_branchesExhausted);
-  smtStatisticsRegistry()->registerStat(&d_execExhausted);
-  smtStatisticsRegistry()->registerStat(&d_pivotsExhausted);
-  smtStatisticsRegistry()->registerStat(&d_panicBranches);
-  smtStatisticsRegistry()->registerStat(&d_relaxCalls);
-  smtStatisticsRegistry()->registerStat(&d_relaxLinFeas);
-  smtStatisticsRegistry()->registerStat(&d_relaxLinFeasFailures);
-  smtStatisticsRegistry()->registerStat(&d_relaxLinInfeas);
-  smtStatisticsRegistry()->registerStat(&d_relaxLinInfeasFailures);
-  smtStatisticsRegistry()->registerStat(&d_relaxLinExhausted);
-  smtStatisticsRegistry()->registerStat(&d_relaxOthers);
-
-  smtStatisticsRegistry()->registerStat(&d_applyRowsDeleted);
-
-  smtStatisticsRegistry()->registerStat(&d_replaySimplexTimer);
-  smtStatisticsRegistry()->registerStat(&d_replayLogTimer);
-  smtStatisticsRegistry()->registerStat(&d_solveIntTimer);
-  smtStatisticsRegistry()->registerStat(&d_solveRealRelaxTimer);
-
-  smtStatisticsRegistry()->registerStat(&d_solveIntCalls);
-  smtStatisticsRegistry()->registerStat(&d_solveStandardEffort);
-
-  smtStatisticsRegistry()->registerStat(&d_approxDisabled);
-
-  smtStatisticsRegistry()->registerStat(&d_replayAttemptFailed);
-
-  smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringReplay);
-  smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringLemmas);
-
-  smtStatisticsRegistry()->registerStat(&d_solveIntModelsAttempts);
-  smtStatisticsRegistry()->registerStat(&d_solveIntModelsSuccessful);
-  smtStatisticsRegistry()->registerStat(&d_mipTimer);
-  smtStatisticsRegistry()->registerStat(&d_lpTimer);
-  smtStatisticsRegistry()->registerStat(&d_mipProofsAttempted);
-  smtStatisticsRegistry()->registerStat(&d_mipProofsSuccessful);
-  smtStatisticsRegistry()->registerStat(&d_numBranchesFailed);
-}
-
-TheoryArithPrivate::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_statAssertUpperConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_statAssertLowerConflicts);
-
-  smtStatisticsRegistry()->unregisterStat(&d_statUserVariables);
-  smtStatisticsRegistry()->unregisterStat(&d_statAuxiliaryVariables);
-  smtStatisticsRegistry()->unregisterStat(&d_statDisequalitySplits);
-  smtStatisticsRegistry()->unregisterStat(&d_statDisequalityConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_simplifyTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_staticLearningTimer);
-
-  smtStatisticsRegistry()->unregisterStat(&d_presolveTime);
-  smtStatisticsRegistry()->unregisterStat(&d_newPropTime);
-
-  smtStatisticsRegistry()->unregisterStat(&d_externalBranchAndBounds);
-
-  smtStatisticsRegistry()->unregisterStat(&d_initialTableauSize);
-  smtStatisticsRegistry()->unregisterStat(&d_currSetToSmaller);
-  smtStatisticsRegistry()->unregisterStat(&d_smallerSetToCurr);
-  smtStatisticsRegistry()->unregisterStat(&d_restartTimer);
-
-  smtStatisticsRegistry()->unregisterStat(&d_boundComputationTime);
-  smtStatisticsRegistry()->unregisterStat(&d_boundComputations);
-  smtStatisticsRegistry()->unregisterStat(&d_boundPropagations);
-
-  smtStatisticsRegistry()->unregisterStat(&d_unknownChecks);
-  smtStatisticsRegistry()->unregisterStat(&d_maxUnknownsInARow);
-  smtStatisticsRegistry()->unregisterStat(&d_avgUnknownsInARow);
-  smtStatisticsRegistry()->unregisterStat(&d_revertsOnConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_commitsOnConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_nontrivialSatChecks);
-
-  smtStatisticsRegistry()->unregisterStat(&d_satPivots);
-  smtStatisticsRegistry()->unregisterStat(&d_unsatPivots);
-  smtStatisticsRegistry()->unregisterStat(&d_unknownPivots);
-
-  smtStatisticsRegistry()->unregisterStat(&d_replayLogRecCount);
-  smtStatisticsRegistry()->unregisterStat(&d_replayLogRecConflictEscalation);
-  smtStatisticsRegistry()->unregisterStat(&d_replayLogRecEarlyExit);
-  smtStatisticsRegistry()->unregisterStat(&d_replayBranchCloseFailures);
-  smtStatisticsRegistry()->unregisterStat(&d_replayLeafCloseFailures);
-  smtStatisticsRegistry()->unregisterStat(&d_replayBranchSkips);
-  smtStatisticsRegistry()->unregisterStat(&d_mirCutsAttempted);
-  smtStatisticsRegistry()->unregisterStat(&d_gmiCutsAttempted);
-  smtStatisticsRegistry()->unregisterStat(&d_branchCutsAttempted);
-  smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructed);
-  smtStatisticsRegistry()->unregisterStat(&d_cutsProven);
-  smtStatisticsRegistry()->unregisterStat(&d_cutsProofFailed);
-  smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructionFailed);
-  smtStatisticsRegistry()->unregisterStat(&d_mipReplayLemmaCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_mipExternalCuts);
-  smtStatisticsRegistry()->unregisterStat(&d_mipExternalBranch);
-
-
-  smtStatisticsRegistry()->unregisterStat(&d_inSolveInteger);
-  smtStatisticsRegistry()->unregisterStat(&d_branchesExhausted);
-  smtStatisticsRegistry()->unregisterStat(&d_execExhausted);
-  smtStatisticsRegistry()->unregisterStat(&d_pivotsExhausted);
-  smtStatisticsRegistry()->unregisterStat(&d_panicBranches);
-  smtStatisticsRegistry()->unregisterStat(&d_relaxCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeas);
-  smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeasFailures);
-  smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeas);
-  smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeasFailures);
-  smtStatisticsRegistry()->unregisterStat(&d_relaxLinExhausted);
-  smtStatisticsRegistry()->unregisterStat(&d_relaxOthers);
-
-  smtStatisticsRegistry()->unregisterStat(&d_applyRowsDeleted);
-
-  smtStatisticsRegistry()->unregisterStat(&d_replaySimplexTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_replayLogTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_solveIntTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_solveRealRelaxTimer);
-
-  smtStatisticsRegistry()->unregisterStat(&d_solveIntCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_solveStandardEffort);
-
-  smtStatisticsRegistry()->unregisterStat(&d_approxDisabled);
-
-  smtStatisticsRegistry()->unregisterStat(&d_replayAttemptFailed);
-
-  smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringReplay);
-  smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringLemmas);
-
-
-  smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsAttempts);
-  smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsSuccessful);
-  smtStatisticsRegistry()->unregisterStat(&d_mipTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_lpTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_mipProofsAttempted);
-  smtStatisticsRegistry()->unregisterStat(&d_mipProofsSuccessful);
-  smtStatisticsRegistry()->unregisterStat(&d_numBranchesFailed);
 }
 
 bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){
@@ -2406,8 +2295,7 @@ void TheoryArithPrivate::subsumption(
 
 std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){
   ++(d_statistics.d_replayLogRecCount);
-  Debug("approx::replayLogRec") << "replayLogRec()"
-                                << d_statistics.d_replayLogRecCount.get() << std::endl;
+  Debug("approx::replayLogRec") << "replayLogRec()" << std::endl;
 
   size_t rpvars_size = d_replayVariables.size();
   size_t rpcons_size = d_replayConstraints.size();
@@ -2842,7 +2730,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
   TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer);
 
   ++(d_statistics.d_solveIntCalls);
-  d_statistics.d_inSolveInteger.set(1);
+  d_statistics.d_inSolveInteger = 1;
 
   if(!Theory::fullEffort(effortLevel)){
     d_solveIntAttempts++;
@@ -2971,7 +2859,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
     }
   }
 
-  d_statistics.d_inSolveInteger.set(0);
+  d_statistics.d_inSolveInteger = 0;
 }
 
 SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
@@ -4324,7 +4212,7 @@ bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){
 void TheoryArithPrivate::presolve(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
 
-  d_statistics.d_initialTableauSize.set(d_tableau.size());
+  d_statistics.d_initialTableauSize = d_tableau.size();
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 408d94397..e23451167 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -53,7 +53,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 #include "util/result.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -856,10 +856,9 @@ private:
     IntStat d_cutsRejectedDuringReplay;
     IntStat d_cutsRejectedDuringLemmas;
 
-    IntegralHistogramStat<uint32_t> d_satPivots;
-    IntegralHistogramStat<uint32_t> d_unsatPivots;
-    IntegralHistogramStat<uint32_t> d_unknownPivots;
-
+    HistogramStat<uint32_t> d_satPivots;
+    HistogramStat<uint32_t> d_unsatPivots;
+    HistogramStat<uint32_t> d_unknownPivots;
 
     IntStat d_solveIntModelsAttempts;
     IntStat d_solveIntModelsSuccessful;
@@ -871,10 +870,7 @@ private:
 
     IntStat d_numBranchesFailed;
 
-
-
-    Statistics();
-    ~Statistics();
+    Statistics(const std::string& name);
   };
 
 
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 164b9b058..4dc7201fb 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -43,26 +43,31 @@ Info::~Info() {
   in_stores->deleteSelf();
 }
 
-ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix)
-    : ct(c), bck(b), info_map(),
-      d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"),
-      d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"),
-      d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"),
-      d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"),
-      d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0),
-      d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0),
-      d_maxList(statisticsPrefix + "theory::arrays::maxList",0),
-      d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) {
+ArrayInfo::ArrayInfo(context::Context* c,
+                     Backtracker<TNode>* b,
+                     std::string statisticsPrefix)
+    : ct(c),
+      bck(b),
+      info_map(),
+      d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
+          statisticsPrefix + "mergeInfoTimer")),
+      d_avgIndexListLength(smtStatisticsRegistry().registerAverage(
+          statisticsPrefix + "avgIndexListLength")),
+      d_avgStoresListLength(smtStatisticsRegistry().registerAverage(
+          statisticsPrefix + "avgStoresListLength")),
+      d_avgInStoresListLength(smtStatisticsRegistry().registerAverage(
+          statisticsPrefix + "avgInStoresListLength")),
+      d_listsCount(
+          smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")),
+      d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix
+                                                           + "callsMergeInfo")),
+      d_maxList(
+          smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")),
+      d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>(
+          statisticsPrefix + "infoTableSize", info_map))
+{
   emptyList = new(true) CTNodeList(ct);
   emptyInfo = new Info(ct, bck);
-  smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
-  smtStatisticsRegistry()->registerStat(&d_avgIndexListLength);
-  smtStatisticsRegistry()->registerStat(&d_avgStoresListLength);
-  smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
-  smtStatisticsRegistry()->registerStat(&d_listsCount);
-  smtStatisticsRegistry()->registerStat(&d_callsMergeInfo);
-  smtStatisticsRegistry()->registerStat(&d_maxList);
-  smtStatisticsRegistry()->registerStat(&d_tableSize);
 }
 
 ArrayInfo::~ArrayInfo() {
@@ -75,14 +80,6 @@ ArrayInfo::~ArrayInfo() {
   }
   emptyList->deleteSelf();
   delete emptyInfo;
-  smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength);
-  smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength);
-  smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength);
-  smtStatisticsRegistry()->unregisterStat(&d_listsCount);
-  smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo);
-  smtStatisticsRegistry()->unregisterStat(&d_maxList);
-  smtStatisticsRegistry()->unregisterStat(&d_tableSize);
 }
 
 bool inList(const CTNodeList* l, const TNode el) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index bbb9e8c62..15f27eb96 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -25,8 +25,7 @@
 #include "context/backtrackable.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -117,7 +116,7 @@ private:
   IntStat d_listsCount;
   IntStat d_callsMergeInfo;
   IntStat d_maxList;
-  SizeStat<CNodeInfoMap > d_tableSize;
+  SizeStat<CNodeInfoMap> d_tableSize;
 
   /**
    * checks if a certain element is in the list l
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index 48755b7ea..fc3f67cf0 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -29,10 +29,9 @@ namespace arrays {
 InferenceManager::InferenceManager(Theory& t,
                                    TheoryState& state,
                                    ProofNodeManager* pnm)
-    : TheoryInferenceManager(t, state, pnm, "theory::arrays", false),
-      d_lemmaPg(pnm ? new EagerProofGenerator(pnm,
-                                              state.getUserContext(),
-                                              "ArrayLemmaProofGenerator")
+    : TheoryInferenceManager(t, state, pnm, "theory::arrays::", false),
+      d_lemmaPg(pnm ? new EagerProofGenerator(
+                    pnm, state.getUserContext(), "ArrayLemmaProofGenerator")
                     : nullptr)
 {
 }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index ee95b3c82..1a1090f68 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -62,30 +62,34 @@ TheoryArrays::TheoryArrays(context::Context* c,
                            ProofNodeManager* pnm,
                            std::string name)
     : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name),
-      d_numRow(name + "theory::arrays::number of Row lemmas", 0),
-      d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
-      d_numProp(name + "theory::arrays::number of propagations", 0),
-      d_numExplain(name + "theory::arrays::number of explanations", 0),
-      d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear",
-                     0),
-      d_numSharedArrayVarSplits(
-          name + "theory::arrays::number of shared array var splits", 0),
-      d_numGetModelValSplits(
-          name + "theory::arrays::number of getModelVal splits", 0),
-      d_numGetModelValConflicts(
-          name + "theory::arrays::number of getModelVal conflicts", 0),
-      d_numSetModelValSplits(
-          name + "theory::arrays::number of setModelVal splits", 0),
-      d_numSetModelValConflicts(
-          name + "theory::arrays::number of setModelVal conflicts", 0),
-      d_ppEqualityEngine(u, name + "theory::arrays::pp", true),
+      d_numRow(
+          smtStatisticsRegistry().registerInt(name + "number of Row lemmas")),
+      d_numExt(
+          smtStatisticsRegistry().registerInt(name + "number of Ext lemmas")),
+      d_numProp(
+          smtStatisticsRegistry().registerInt(name + "number of propagations")),
+      d_numExplain(
+          smtStatisticsRegistry().registerInt(name + "number of explanations")),
+      d_numNonLinear(smtStatisticsRegistry().registerInt(
+          name + "number of calls to setNonLinear")),
+      d_numSharedArrayVarSplits(smtStatisticsRegistry().registerInt(
+          name + "number of shared array var splits")),
+      d_numGetModelValSplits(smtStatisticsRegistry().registerInt(
+          name + "number of getModelVal splits")),
+      d_numGetModelValConflicts(smtStatisticsRegistry().registerInt(
+          name + "number of getModelVal conflicts")),
+      d_numSetModelValSplits(smtStatisticsRegistry().registerInt(
+          name + "number of setModelVal splits")),
+      d_numSetModelValConflicts(smtStatisticsRegistry().registerInt(
+          name + "number of setModelVal conflicts")),
+      d_ppEqualityEngine(u, name + "pp", true),
       d_ppFacts(u),
       d_state(c, u, valuation),
       d_im(*this, d_state, pnm),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_isPreRegistered(c),
-      d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
+      d_mayEqualEqualityEngine(c, name + "mayEqual", true),
       d_notify(*this),
       d_backtracker(c),
       d_infoMap(c, &d_backtracker, name),
@@ -112,17 +116,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
       d_dstrat(new TheoryArraysDecisionStrategy(this)),
       d_dstratInit(false)
 {
-  smtStatisticsRegistry()->registerStat(&d_numRow);
-  smtStatisticsRegistry()->registerStat(&d_numExt);
-  smtStatisticsRegistry()->registerStat(&d_numProp);
-  smtStatisticsRegistry()->registerStat(&d_numExplain);
-  smtStatisticsRegistry()->registerStat(&d_numNonLinear);
-  smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits);
-  smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits);
-  smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts);
-  smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits);
-  smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts);
-
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
@@ -147,16 +140,6 @@ TheoryArrays::~TheoryArrays() {
     it2->second->deleteSelf();
   }
   delete d_constReadsContext;
-  smtStatisticsRegistry()->unregisterStat(&d_numRow);
-  smtStatisticsRegistry()->unregisterStat(&d_numExt);
-  smtStatisticsRegistry()->unregisterStat(&d_numProp);
-  smtStatisticsRegistry()->unregisterStat(&d_numExplain);
-  smtStatisticsRegistry()->unregisterStat(&d_numNonLinear);
-  smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits);
-  smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits);
-  smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits);
-  smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
 }
 
 TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
@@ -166,7 +149,7 @@ ProofRuleChecker* TheoryArrays::getProofChecker() { return &d_checker; }
 bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
-  esi.d_name = d_instanceName + "theory::arrays::ee";
+  esi.d_name = d_instanceName + "ee";
   return true;
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 188573152..7cf8d52e3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -32,7 +32,7 @@
 #include "theory/theory.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -138,7 +138,7 @@ class TheoryArrays : public Theory {
                Valuation valuation,
                const LogicInfo& logicInfo,
                ProofNodeManager* pnm = nullptr,
-               std::string name = "");
+               std::string name = "theory::arrays::");
   ~TheoryArrays();
 
   //--------------------------------- initialization
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 6e3b38d8d..3d1a94f22 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -16,6 +16,7 @@
 #include "theory/bags/bags_rewriter.h"
 
 #include "theory/bags/normal_form.h"
+#include "util/statistics_registry.h"
 
 using namespace cvc5::kind;
 
@@ -38,7 +39,7 @@ BagsRewriteResponse::BagsRewriteResponse(const BagsRewriteResponse& r)
 {
 }
 
-BagsRewriter::BagsRewriter(IntegralHistogramStat<Rewrite>* statistics)
+BagsRewriter::BagsRewriter(HistogramStat<Rewrite>* statistics)
     : d_statistics(statistics)
 {
   d_nm = NodeManager::currentNM();
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 10fa65aa5..54c1d7253 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -20,8 +20,7 @@
 
 #include "theory/bags/rewrites.h"
 #include "theory/theory_rewriter.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -43,7 +42,7 @@ struct BagsRewriteResponse
 class BagsRewriter : public TheoryRewriter
 {
  public:
-  BagsRewriter(IntegralHistogramStat<Rewrite>* statistics = nullptr);
+  BagsRewriter(HistogramStat<Rewrite>* statistics = nullptr);
 
   /**
    * postRewrite nodes with kinds: MK_BAG, BAG_COUNT, UNION_MAX, UNION_DISJOINT,
@@ -219,7 +218,7 @@ class BagsRewriter : public TheoryRewriter
   Node d_zero;
   Node d_one;
   /** Reference to the rewriter statistics. */
-  IntegralHistogramStat<Rewrite>* d_statistics;
+  HistogramStat<Rewrite>* d_statistics;
 }; /* class TheoryBagsRewriter */
 
 }  // namespace bags
diff --git a/src/theory/bags/bags_statistics.cpp b/src/theory/bags/bags_statistics.cpp
index 018dbb231..5c351f0ac 100644
--- a/src/theory/bags/bags_statistics.cpp
+++ b/src/theory/bags/bags_statistics.cpp
@@ -21,14 +21,10 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-BagsStatistics::BagsStatistics() : d_rewrites("theory::bags::rewrites")
+BagsStatistics::BagsStatistics()
+    : d_rewrites(smtStatisticsRegistry().registerHistogram<Rewrite>(
+        "theory::bags::rewrites"))
 {
-  smtStatisticsRegistry()->registerStat(&d_rewrites);
-}
-
-BagsStatistics::~BagsStatistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_rewrites);
 }
 
 }  // namespace bags
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index c0bca3444..d2eb33dbe 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -19,8 +19,7 @@
 #define CVC5__THEORY__BAGS_STATISTICS_H
 
 #include "theory/bags/rewrites.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -33,10 +32,9 @@ class BagsStatistics
 {
  public:
   BagsStatistics();
-  ~BagsStatistics();
 
   /** Counts the number of applications of each type of rewrite rule */
-  IntegralHistogramStat<Rewrite> d_rewrites;
+  HistogramStat<Rewrite> d_rewrites;
 };
 
 }  // namespace bags
diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 797ec0f4d..cc163e6cf 100644
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -27,7 +27,7 @@ namespace bags {
 InferenceManager::InferenceManager(Theory& t,
                                    SolverState& s,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, s, pnm, "theory::bags"), d_state(s)
+    : InferenceManagerBuffered(t, s, pnm, "theory::bags::"), d_state(s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index bded82b4b..e6080ed4f 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -532,8 +532,6 @@ void AbstractionModule::finalizeSignatures()
     d_funcToSignature[abs_func] = signature;
   }
 
-  d_statistics.d_numFunctionsAbstracted.set(d_signatureToFunc.size());
-
   Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted "
                           << d_signatureToFunc.size() << " signatures. \n";
 }
@@ -1090,19 +1088,14 @@ AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode
   return d_data.find(signature)->second;
 }
 
-AbstractionModule::Statistics::Statistics(const std::string& name)
-    : d_numFunctionsAbstracted(name + "::abstraction::NumFunctionsAbstracted",
-                               0),
-      d_numArgsSkolemized(name + "::abstraction::NumArgsSkolemized", 0),
-      d_abstractionTime(name + "::abstraction::AbstractionTime")
+AbstractionModule::Statistics::Statistics(
+    const std::string& name, const NodeNodeMap& functionsAbstracted)
+    : d_numFunctionsAbstracted(
+        smtStatisticsRegistry().registerSize<NodeNodeMap>(
+            name + "NumFunctionsAbstracted", functionsAbstracted)),
+      d_numArgsSkolemized(
+          smtStatisticsRegistry().registerInt(name + "NumArgsSkolemized")),
+      d_abstractionTime(
+          smtStatisticsRegistry().registerTimer(name + "AbstractionTime"))
 {
-  smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
-  smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
-  smtStatisticsRegistry()->registerStat(&d_abstractionTime);
-}
-
-AbstractionModule::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted);
-  smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized);
-  smtStatisticsRegistry()->unregisterStat(&d_abstractionTime);
 }
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index b099a33cd..67a04bfea 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -23,8 +23,7 @@
 
 #include "expr/node.h"
 #include "theory/substitutions.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -33,13 +32,23 @@ namespace bv {
 typedef std::vector<TNode> ArgsVec;
 
 class AbstractionModule {
+  using NodeVecMap =
+      std::unordered_map<Node, std::vector<Node>, NodeHashFunction>;
+  using NodeTNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
+  using TNodeTNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
+  using NodeNodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+  using TNodeNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
+  using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+  using IntNodeMap = std::unordered_map<unsigned, Node>;
+  using IndexMap = std::unordered_map<unsigned, unsigned>;
+  using SkolemMap = std::unordered_map<unsigned, std::vector<Node> >;
+  using SignatureMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
 
   struct Statistics {
-    IntStat d_numFunctionsAbstracted;
+    SizeStat<NodeNodeMap> d_numFunctionsAbstracted;
     IntStat d_numArgsSkolemized;
     TimerStat d_abstractionTime;
-    Statistics(const std::string& name);
-    ~Statistics();
+    Statistics(const std::string& name, const NodeNodeMap& functionsAbstracted);
   };
 
 
@@ -126,17 +135,6 @@ class AbstractionModule {
 
   };
 
-  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
-  typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
-  typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
-  typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef std::unordered_map<unsigned, Node> IntNodeMap;
-  typedef std::unordered_map<unsigned, unsigned> IndexMap;
-  typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap;
-  typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
-
   ArgsTable d_argsTable;
 
   // mapping between signature and uninterpreted function symbol used to
@@ -197,21 +195,22 @@ class AbstractionModule {
   Statistics d_statistics;
 
 public:
-  AbstractionModule(const std::string& name)
-    : d_argsTable()
-    , d_signatureToFunc()
-    , d_funcToSignature()
-    , d_assertionToSignature()
-    , d_signatures()
-    , d_sigToGeneralization()
-    , d_skolems()
-    , d_signatureIndices()
-    , d_signatureSkolems()
-    , d_addedLemmas()
-    , d_lemmaAtoms()
-    , d_inputAtoms()
-    , d_statistics(name)
-  {}
+ AbstractionModule(const std::string& name)
+     : d_argsTable(),
+       d_signatureToFunc(),
+       d_funcToSignature(),
+       d_assertionToSignature(),
+       d_signatures(),
+       d_sigToGeneralization(),
+       d_skolems(),
+       d_signatureIndices(),
+       d_signatureSkolems(),
+       d_addedLemmas(),
+       d_lemmaAtoms(),
+       d_inputAtoms(),
+       d_statistics(name + "abstraction::", d_signatureToFunc)
+ {
+ }
   /**
    * returns true if there are new uninterepreted functions symbols in the output
    *
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 8c80f9d19..0907e8005 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -148,24 +148,25 @@ AigBitblaster::AigBitblaster()
     case options::SatSolverMode::MINISAT:
     {
       prop::BVSatSolverInterface* minisat =
-          prop::SatSolverFactory::createMinisat(
-              d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
+          prop::SatSolverFactory::createMinisat(d_nullContext.get(),
+                                                smtStatisticsRegistry(),
+                                                "theory::bv::AigBitblaster::");
       d_notify.reset(new MinisatEmptyNotify());
       minisat->setNotify(d_notify.get());
       solver = minisat;
       break;
     }
     case options::SatSolverMode::CADICAL:
-      solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
-                                                     "AigBitblaster");
+      solver = prop::SatSolverFactory::createCadical(
+          smtStatisticsRegistry(), "theory::bv::AigBitblaster::");
       break;
     case options::SatSolverMode::CRYPTOMINISAT:
       solver = prop::SatSolverFactory::createCryptoMinisat(
-          smtStatisticsRegistry(), "AigBitblaster");
+          smtStatisticsRegistry(), "theory::bv::AigBitblaster::");
       break;
     case options::SatSolverMode::KISSAT:
-      solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
-                                                    "AigBitblaster");
+      solver = prop::SatSolverFactory::createKissat(
+          smtStatisticsRegistry(), "theory::bv::AigBitblaster::");
       break;
     default: CVC5_FATAL() << "Unknown SAT solver type";
   }
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index fcd33e775..9871f2a92 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -47,23 +47,25 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
     {
       prop::BVSatSolverInterface* minisat =
           prop::SatSolverFactory::createMinisat(
-              d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster");
+              d_nullContext.get(),
+              smtStatisticsRegistry(),
+              "theory::bv::EagerBitblaster::");
       d_notify.reset(new MinisatEmptyNotify());
       minisat->setNotify(d_notify.get());
       solver = minisat;
       break;
     }
     case options::SatSolverMode::CADICAL:
-      solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
-                                                     "EagerBitblaster");
+      solver = prop::SatSolverFactory::createCadical(
+          smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
       break;
     case options::SatSolverMode::CRYPTOMINISAT:
       solver = prop::SatSolverFactory::createCryptoMinisat(
-          smtStatisticsRegistry(), "EagerBitblaster");
+          smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
       break;
     case options::SatSolverMode::KISSAT:
-      solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
-                                                    "EagerBitblaster");
+      solver = prop::SatSolverFactory::createKissat(
+          smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
       break;
     default: Unreachable() << "Unknown SAT solver type";
   }
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 12f584442..6a5372e04 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -73,10 +73,10 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
       d_emptyNotify(emptyNotify),
       d_fullModelAssertionLevel(c, 0),
       d_name(name),
-      d_statistics(name)
+      d_statistics(name + "::")
 {
-  d_satSolver.reset(
-      prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
+  d_satSolver.reset(prop::SatSolverFactory::createMinisat(
+      c, smtStatisticsRegistry(), name + "::"));
 
   ResourceManager* rm = smt::currentResourceManager();
   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
@@ -362,33 +362,22 @@ void TLazyBitblaster::getConflict(std::vector<TNode>& conflict)
   }
 }
 
-TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
-  d_numTermClauses(prefix + "::NumTermSatClauses", 0),
-  d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
-  d_numTerms(prefix + "::NumBitblastedTerms", 0),
-  d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
-  d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
-  d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
-  d_bitblastTimer(prefix + "::BitblastTimer")
+TLazyBitblaster::Statistics::Statistics(const std::string& prefix)
+    : d_numTermClauses(
+        smtStatisticsRegistry().registerInt(prefix + "NumTermSatClauses")),
+      d_numAtomClauses(
+          smtStatisticsRegistry().registerInt(prefix + "NumAtomSatClauses")),
+      d_numTerms(
+          smtStatisticsRegistry().registerInt(prefix + "NumBitblastedTerms")),
+      d_numAtoms(
+          smtStatisticsRegistry().registerInt(prefix + "NumBitblastedAtoms")),
+      d_numExplainedPropagations(smtStatisticsRegistry().registerInt(
+          prefix + "NumExplainedPropagations")),
+      d_numBitblastingPropagations(smtStatisticsRegistry().registerInt(
+          prefix + "NumBitblastingPropagations")),
+      d_bitblastTimer(
+          smtStatisticsRegistry().registerTimer(prefix + "BitblastTimer"))
 {
-  smtStatisticsRegistry()->registerStat(&d_numTermClauses);
-  smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
-  smtStatisticsRegistry()->registerStat(&d_numTerms);
-  smtStatisticsRegistry()->registerStat(&d_numAtoms);
-  smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations);
-  smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations);
-  smtStatisticsRegistry()->registerStat(&d_bitblastTimer);
-}
-
-
-TLazyBitblaster::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numTermClauses);
-  smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses);
-  smtStatisticsRegistry()->unregisterStat(&d_numTerms);
-  smtStatisticsRegistry()->unregisterStat(&d_numAtoms);
-  smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations);
-  smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations);
-  smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer);
 }
 
 bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 7ca2063a3..15cbe1558 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -161,7 +161,6 @@ class TLazyBitblaster : public TBitblaster<Node>
     IntStat d_numBitblastingPropagations;
     TimerStat d_bitblastTimer;
     Statistics(const std::string& name);
-    ~Statistics();
   };
   std::string d_name;
 
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index f3d2a0832..5d3e99253 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -351,31 +351,21 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
 }
 
 QuickXPlain::Statistics::Statistics(const std::string& name)
-  : d_xplainTime(name + "::QuickXplain::Time")
-  , d_numSolved(name + "::QuickXplain::NumSolved", 0)
-  , d_numUnknown(name + "::QuickXplain::NumUnknown", 0)
-  , d_numUnknownWasUnsat(name + "::QuickXplain::NumUnknownWasUnsat", 0)
-  , d_numConflictsMinimized(name + "::QuickXplain::NumConflictsMinimized", 0)
-  , d_finalPeriod(name + "::QuickXplain::FinalPeriod", 0)
-  , d_avgMinimizationRatio(name + "::QuickXplain::AvgMinRatio")
+    : d_xplainTime(
+        smtStatisticsRegistry().registerTimer(name + "QuickXplain::Time")),
+      d_numSolved(
+          smtStatisticsRegistry().registerInt(name + "QuickXplain::NumSolved")),
+      d_numUnknown(smtStatisticsRegistry().registerInt(
+          name + "QuickXplain::NumUnknown")),
+      d_numUnknownWasUnsat(smtStatisticsRegistry().registerInt(
+          name + "QuickXplain::NumUnknownWasUnsat")),
+      d_numConflictsMinimized(smtStatisticsRegistry().registerInt(
+          name + "QuickXplain::NumConflictsMinimized")),
+      d_finalPeriod(smtStatisticsRegistry().registerInt(
+          name + "QuickXplain::FinalPeriod")),
+      d_avgMinimizationRatio(smtStatisticsRegistry().registerAverage(
+          name + "QuickXplain::AvgMinRatio"))
 {
-  smtStatisticsRegistry()->registerStat(&d_xplainTime);
-  smtStatisticsRegistry()->registerStat(&d_numSolved);
-  smtStatisticsRegistry()->registerStat(&d_numUnknown);
-  smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat);
-  smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized);
-  smtStatisticsRegistry()->registerStat(&d_finalPeriod);
-  smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio);
-}
-
-QuickXPlain::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_xplainTime);
-  smtStatisticsRegistry()->unregisterStat(&d_numSolved);
-  smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
-  smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat);
-  smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized);
-  smtStatisticsRegistry()->unregisterStat(&d_finalPeriod);
-  smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio);  
 }
 
 }  // namespace bv
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 57bcca261..f22f298ac 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -25,8 +25,7 @@
 #include "expr/node.h"
 #include "prop/sat_solver_types.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -121,7 +120,6 @@ class QuickXPlain
     IntStat d_finalPeriod;
     AverageStat d_avgMinimizationRatio;
     Statistics(const std::string& name);
-    ~Statistics();
   };
   BVQuickCheck* d_solver;
   unsigned long d_budget;
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 1a3eb0a4b..a9d46f068 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -52,11 +52,11 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
   {
     case options::SatSolverMode::CRYPTOMINISAT:
       d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
-          smtStatisticsRegistry(), "BVSolverBitblast"));
+          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
       break;
     default:
       d_satSolver.reset(prop::SatSolverFactory::createCadical(
-          smtStatisticsRegistry(), "BVSolverBitblast"));
+          smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
   }
   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
                                         d_nullRegistrar.get(),
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index a36c4d4fb..a8670e1a6 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -124,33 +124,21 @@ void BVSolverLazy::spendResource(Resource r)
 }
 
 BVSolverLazy::Statistics::Statistics()
-    : d_avgConflictSize("theory::bv::lazy::AvgBVConflictSize"),
-      d_solveSubstitutions("theory::bv::lazy::NumSolveSubstitutions", 0),
-      d_solveTimer("theory::bv::lazy::solveTimer"),
-      d_numCallsToCheckFullEffort("theory::bv::lazy::NumFullCheckCalls", 0),
-      d_numCallsToCheckStandardEffort("theory::bv::lazy::NumStandardCheckCalls",
-                                      0),
-      d_weightComputationTimer("theory::bv::lazy::weightComputationTimer"),
-      d_numMultSlice("theory::bv::lazy::NumMultSliceApplied", 0)
+    : d_avgConflictSize(smtStatisticsRegistry().registerAverage(
+        "theory::bv::lazy::AvgBVConflictSize")),
+      d_solveSubstitutions(smtStatisticsRegistry().registerInt(
+          "theory::bv::lazy::NumSolveSubstitutions")),
+      d_solveTimer(smtStatisticsRegistry().registerTimer(
+          "theory::bv::lazy::solveTimer")),
+      d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
+          "theory::bv::lazy::NumFullCheckCalls")),
+      d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt(
+          "theory::bv::lazy::NumStandardCheckCalls")),
+      d_weightComputationTimer(smtStatisticsRegistry().registerTimer(
+          "theory::bv::lazy::weightComputationTimer")),
+      d_numMultSlice(smtStatisticsRegistry().registerInt(
+          "theory::bv::lazy::NumMultSliceApplied"))
 {
-  smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
-  smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
-  smtStatisticsRegistry()->registerStat(&d_solveTimer);
-  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
-  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
-  smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
-  smtStatisticsRegistry()->registerStat(&d_numMultSlice);
-}
-
-BVSolverLazy::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
-  smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
-  smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
-  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
-  smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
 }
 
 void BVSolverLazy::preRegisterTerm(TNode node)
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 42f59eda4..e11f525f3 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -119,7 +119,6 @@ class BVSolverLazy : public BVSolver
     TimerStat d_weightComputationTimer;
     IntStat d_numMultSlice;
     Statistics();
-    ~Statistics();
   };
 
   Statistics d_statistics;
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 254a9b13e..4c050b3f0 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -750,34 +750,23 @@ Node AlgebraicSolver::getModelValue(TNode node) {
 }
 
 AlgebraicSolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
-  , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
-  , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
-  , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
-  , d_numSat("theory::bv::algebraic::NumSat", 0)
-  , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
-  , d_solveTime("theory::bv::algebraic::SolveTime")
-  , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
+    : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+        "theory::bv::algebraic::NumCallsToCheck")),
+      d_numSimplifiesToTrue(smtStatisticsRegistry().registerInt(
+          "theory::bv::algebraic::NumSimplifiesToTrue")),
+      d_numSimplifiesToFalse(smtStatisticsRegistry().registerInt(
+          "theory::bv::algebraic::NumSimplifiesToFalse")),
+      d_numUnsat(smtStatisticsRegistry().registerInt(
+          "theory::bv::algebraic::NumUnsat")),
+      d_numSat(
+          smtStatisticsRegistry().registerInt("theory::bv::algebraic::NumSat")),
+      d_numUnknown(smtStatisticsRegistry().registerInt(
+          "theory::bv::algebraic::NumUnknown")),
+      d_solveTime(smtStatisticsRegistry().registerTimer(
+          "theory::bv::algebraic::SolveTime")),
+      d_useHeuristic(smtStatisticsRegistry().registerValue<double>(
+          "theory::bv::algebraic::UseHeuristic", 0.2))
 {
-  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
-  smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse);
-  smtStatisticsRegistry()->registerStat(&d_numUnsat);
-  smtStatisticsRegistry()->registerStat(&d_numSat);
-  smtStatisticsRegistry()->registerStat(&d_numUnknown);
-  smtStatisticsRegistry()->registerStat(&d_solveTime);
-  smtStatisticsRegistry()->registerStat(&d_useHeuristic);
-}
-
-AlgebraicSolver::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue);
-  smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse);
-  smtStatisticsRegistry()->unregisterStat(&d_numUnsat);
-  smtStatisticsRegistry()->unregisterStat(&d_numSat);
-  smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
-  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
-  smtStatisticsRegistry()->unregisterStat(&d_useHeuristic);
 }
 
 bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) {
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 93fe9d21d..670adafa3 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -163,9 +163,8 @@ class AlgebraicSolver : public SubtheorySolver
     IntStat d_numSat;
     IntStat d_numUnknown;
     TimerStat d_solveTime;
-    BackedStat<double> d_useHeuristic;
+    ValueStat<double> d_useHeuristic;
     Statistics();
-    ~Statistics();
   };
 
   std::unique_ptr<SubstitutionMap> d_modelMap;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 70c9d9de6..b86809a91 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -54,15 +54,11 @@ BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv)
 BitblastSolver::~BitblastSolver() {}
 
 BitblastSolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
-  , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+    : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+        "theory::bv::BitblastSolver::NumCallsToCheck")),
+      d_numBBLemmas(smtStatisticsRegistry().registerInt(
+          "theory::bv::BitblastSolver::NumTimesLemmasBB"))
 {
-  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
-}
-BitblastSolver::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas);
 }
 
 void BitblastSolver::setAbstraction(AbstractionModule* abs) {
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index a3238ae61..903a5136e 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -41,7 +41,6 @@ class BitblastSolver : public SubtheorySolver
     IntStat d_numCallstoCheck;
     IntStat d_numBBLemmas;
     Statistics();
-    ~Statistics();
   };
   /** Bitblaster */
   std::unique_ptr<TLazyBitblaster> d_bitblaster;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 0a391f474..7f3099f8c 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -484,12 +484,9 @@ void CoreSolver::addTermToEqualityEngine(TNode node)
 }
 
 CoreSolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
+    : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+        "theory::bv::CoreSolver::NumCallsToCheck"))
 {
-  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
-}
-CoreSolver::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
 }
 
 void CoreSolver::checkExtf(Theory::Effort e)
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 2400eb31b..52d9e739a 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -58,7 +58,6 @@ class CoreSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
-    ~Statistics();
   };
 
   // NotifyClass: handles call-back from congruence closure module
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 3613584fe..10b9a346e 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -246,15 +246,9 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact)
 }
 
 InequalitySolver::Statistics::Statistics()
-    : d_numCallstoCheck("theory::bv::inequality::NumCallsToCheck", 0),
-      d_solveTime("theory::bv::inequality::SolveTime")
+    : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+        "theory::bv::inequality::NumCallsToCheck")),
+      d_solveTime(smtStatisticsRegistry().registerTimer(
+          "theory::bv::inequality::SolveTime"))
 {
-  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->registerStat(&d_solveTime);
-}
-
-InequalitySolver::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
-  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
 }
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index b554062c0..65eee95e1 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -49,7 +49,6 @@ class InequalitySolver : public SubtheorySolver
     IntStat d_numCallstoCheck;
     TimerStat d_solveTime;
     Statistics();
-    ~Statistics();
   };
 
   context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 107d6313c..06f837c7f 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -39,7 +39,7 @@ TheoryBV::TheoryBV(context::Context* c,
       d_internal(nullptr),
       d_rewriter(),
       d_state(c, u, valuation),
-      d_im(*this, d_state, nullptr, "theory::bv"),
+      d_im(*this, d_state, nullptr, "theory::bv::"),
       d_notify(d_im)
 {
   switch (options::bvSolver())
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 412c824aa..72906929b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -29,7 +29,7 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index e459ec05b..393813590 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -33,7 +33,7 @@ namespace datatypes {
 InferenceManager::InferenceManager(Theory& t,
                                    TheoryState& state,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, state, pnm, "theory::datatypes"),
+    : InferenceManagerBuffered(t, state, pnm, "theory::datatypes::"),
       d_pnm(pnm),
       d_ipc(pnm == nullptr ? nullptr
                            : new InferProofCons(state.getSatContext(), pnm)),
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index d5ce5ab79..b1f35821f 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -26,32 +26,21 @@ namespace cvc5 {
 namespace theory {
 
 EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory)
-    : conflicts(getStatsPrefix(theory) + "::conflicts", 0),
-      propagations(getStatsPrefix(theory) + "::propagations", 0),
-      lemmas(getStatsPrefix(theory) + "::lemmas", 0),
-      requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
-      restartDemands(getStatsPrefix(theory) + "::restartDemands", 0),
-      trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0),
-      trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0)
+    : conflicts(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                    + "conflicts")),
+      propagations(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                       + "propagations")),
+      lemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                 + "lemmas")),
+      requirePhase(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                       + "requirePhase")),
+      restartDemands(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                         + "restartDemands")),
+      trustedConflicts(smtStatisticsRegistry().registerInt(
+          getStatsPrefix(theory) + "trustedConflicts")),
+      trustedLemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+                                                        + "trustedLemmas"))
 {
-  smtStatisticsRegistry()->registerStat(&conflicts);
-  smtStatisticsRegistry()->registerStat(&propagations);
-  smtStatisticsRegistry()->registerStat(&lemmas);
-  smtStatisticsRegistry()->registerStat(&requirePhase);
-  smtStatisticsRegistry()->registerStat(&restartDemands);
-  smtStatisticsRegistry()->registerStat(&trustedConflicts);
-  smtStatisticsRegistry()->registerStat(&trustedLemmas);
-}
-
-EngineOutputChannel::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&conflicts);
-  smtStatisticsRegistry()->unregisterStat(&propagations);
-  smtStatisticsRegistry()->unregisterStat(&lemmas);
-  smtStatisticsRegistry()->unregisterStat(&requirePhase);
-  smtStatisticsRegistry()->unregisterStat(&restartDemands);
-  smtStatisticsRegistry()->unregisterStat(&trustedConflicts);
-  smtStatisticsRegistry()->unregisterStat(&trustedLemmas);
 }
 
 EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index ff9bdfa64..dcf8fba55 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 #include "theory/output_channel.h"
 #include "theory/theory_id.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -89,7 +89,6 @@ class EngineOutputChannel : public theory::OutputChannel
   {
    public:
     Statistics(theory::TheoryId theory);
-    ~Statistics();
     /** Number of calls to conflict, propagate, lemma, requirePhase,
      * restartDemands */
     IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 80a5c539b..4bcb761a5 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -122,7 +122,7 @@ TheoryFp::TheoryFp(context::Context* c,
       d_floatToRealMap(u),
       d_abstractionMap(u),
       d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::fp", false)
+      d_im(*this, d_state, pnm, "theory::fp::", false)
 {
   // indicate we are using the default theory state and inference manager
   d_theoryState = &d_state;
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 42fe40faf..534d59aeb 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -27,9 +27,9 @@ namespace theory {
 InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
                                                    TheoryState& state,
                                                    ProofNodeManager* pnm,
-                                                   const std::string& name,
+                                                   const std::string& statsName,
                                                    bool cacheLemmas)
-    : TheoryInferenceManager(t, state, pnm, name, cacheLemmas),
+    : TheoryInferenceManager(t, state, pnm, statsName, cacheLemmas),
       d_processingPendingLemmas(false)
 {
 }
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 5dd01b802..080033562 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -35,7 +35,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   InferenceManagerBuffered(Theory& t,
                            TheoryState& state,
                            ProofNodeManager* pnm,
-                           const std::string& name,
+                           const std::string& statsName,
                            bool cacheLemmas = true);
   virtual ~InferenceManagerBuffered() {}
   /**
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 2264127cf..0279a72ca 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 #include "theory/inference_id.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 7ab0f1b8f..266de9a53 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/cegqi/vts_term_cache.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_module.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 5f83578df..0415d4271 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -742,23 +742,15 @@ InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q)
 }
 
 Instantiate::Statistics::Statistics()
-    : d_instantiations("Instantiate::Instantiations_Total", 0),
-      d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
-      d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
-      d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0)
+    : d_instantiations(smtStatisticsRegistry().registerInt(
+        "Instantiate::Instantiations_Total")),
+      d_inst_duplicate(
+          smtStatisticsRegistry().registerInt("Instantiate::Duplicate_Inst")),
+      d_inst_duplicate_eq(smtStatisticsRegistry().registerInt(
+          "Instantiate::Duplicate_Inst_Eq")),
+      d_inst_duplicate_ent(smtStatisticsRegistry().registerInt(
+          "Instantiate::Duplicate_Inst_Entailed"))
 {
-  smtStatisticsRegistry()->registerStat(&d_instantiations);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
-}
-
-Instantiate::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
-  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index f420c0f62..42bff316a 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -26,7 +26,7 @@
 #include "theory/inference_id.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/quant_util.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -290,7 +290,6 @@ class Instantiate : public QuantifiersUtil
     IntStat d_inst_duplicate_eq;
     IntStat d_inst_duplicate_ent;
     Statistics();
-    ~Statistics();
   }; /* class Instantiate::Statistics */
   Statistics d_statistics;
 
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 791f843fa..cff9fde0b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2270,17 +2270,12 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
   }
 }
 
-QuantConflictFind::Statistics::Statistics():
-  d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
-  d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
+QuantConflictFind::Statistics::Statistics()
+    : d_inst_rounds(
+        smtStatisticsRegistry().registerInt("QuantConflictFind::Inst_Rounds")),
+      d_entailment_checks(smtStatisticsRegistry().registerInt(
+          "QuantConflictFind::Entailment_Checks"))
 {
-  smtStatisticsRegistry()->registerStat(&d_inst_rounds);
-  smtStatisticsRegistry()->registerStat(&d_entailment_checks);
-}
-
-QuantConflictFind::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_entailment_checks);
 }
 
 TNode QuantConflictFind::getZero( Kind k ) {
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index b533a3f12..5a36452fe 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -287,7 +287,6 @@ public:
     IntStat d_inst_rounds;
     IntStat d_entailment_checks;
     Statistics();
-    ~Statistics();
   };
   Statistics d_statistics;
   /** Identify this module */
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 0f7c65924..67f8f6f8e 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -28,7 +28,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     QuantifiersRegistry& qr,
     TermRegistry& tr,
     ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
+    : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers::"),
       d_instantiate(new Instantiate(state, *this, qr, tr, pnm)),
       d_skolemize(new Skolemize(state, tr, pnm))
 {
diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp
index e3c17fd77..59fdb1808 100644
--- a/src/theory/quantifiers/quantifiers_statistics.cpp
+++ b/src/theory/quantifiers/quantifiers_statistics.cpp
@@ -22,42 +22,27 @@ namespace theory {
 namespace quantifiers {
 
 QuantifiersStatistics::QuantifiersStatistics()
-    : d_time("theory::QuantifiersEngine::time"),
-      d_qcf_time("theory::QuantifiersEngine::time_qcf"),
-      d_ematching_time("theory::QuantifiersEngine::time_ematching"),
-      d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
-      d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
-      d_instantiation_rounds_lc(
-          "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
-      d_triggers("QuantifiersEngine::Triggers", 0),
-      d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
-      d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
-      d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
+    : d_time(smtStatisticsRegistry().registerTimer(
+        "theory::QuantifiersEngine::time")),
+      d_qcf_time(smtStatisticsRegistry().registerTimer(
+          "theory::QuantifiersEngine::time_qcf")),
+      d_ematching_time(smtStatisticsRegistry().registerTimer(
+          "theory::QuantifiersEngine::time_ematching")),
+      d_num_quant(smtStatisticsRegistry().registerInt(
+          "QuantifiersEngine::Num_Quantifiers")),
+      d_instantiation_rounds(smtStatisticsRegistry().registerInt(
+          "QuantifiersEngine::Rounds_Instantiation_Full")),
+      d_instantiation_rounds_lc(smtStatisticsRegistry().registerInt(
+          "QuantifiersEngine::Rounds_Instantiation_Last_Call")),
+      d_triggers(
+          smtStatisticsRegistry().registerInt("QuantifiersEngine::Triggers")),
+      d_simple_triggers(smtStatisticsRegistry().registerInt(
+          "QuantifiersEngine::Triggers_Simple")),
+      d_multi_triggers(smtStatisticsRegistry().registerInt(
+          "QuantifiersEngine::Triggers_Multi")),
+      d_red_alpha_equiv(smtStatisticsRegistry().registerInt(
+          "QuantifiersEngine::Reductions_Alpha_Equivalence"))
 {
-  smtStatisticsRegistry()->registerStat(&d_time);
-  smtStatisticsRegistry()->registerStat(&d_qcf_time);
-  smtStatisticsRegistry()->registerStat(&d_ematching_time);
-  smtStatisticsRegistry()->registerStat(&d_num_quant);
-  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
-  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
-  smtStatisticsRegistry()->registerStat(&d_triggers);
-  smtStatisticsRegistry()->registerStat(&d_simple_triggers);
-  smtStatisticsRegistry()->registerStat(&d_multi_triggers);
-  smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
-}
-
-QuantifiersStatistics::~QuantifiersStatistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_time);
-  smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
-  smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
-  smtStatisticsRegistry()->unregisterStat(&d_num_quant);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
-  smtStatisticsRegistry()->unregisterStat(&d_triggers);
-  smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
-  smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
-  smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h
index f03d27ee3..438efd30f 100644
--- a/src/theory/quantifiers/quantifiers_statistics.h
+++ b/src/theory/quantifiers/quantifiers_statistics.h
@@ -18,8 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
 #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
 
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -33,7 +32,6 @@ class QuantifiersStatistics
 {
  public:
   QuantifiersStatistics();
-  ~QuantifiersStatistics();
   TimerStat d_time;
   TimerStat d_qcf_time;
   TimerStat d_ematching_time;
diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp
index 4fe0e9bbc..19d799eb3 100644
--- a/src/theory/quantifiers/sygus/sygus_stats.cpp
+++ b/src/theory/quantifiers/sygus/sygus_stats.cpp
@@ -22,40 +22,26 @@ namespace theory {
 namespace quantifiers {
 
 SygusStatistics::SygusStatistics()
-    : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0),
-      d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0),
-      d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0),
-      d_solutions("SynthConjecture::solutions", 0),
-      d_filtered_solutions("SynthConjecture::filtered_solutions", 0),
-      d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print",
-                                 0),
-      d_enumTermsRewrite("SygusEnumerator::enumTermsRewrite", 0),
-      d_enumTermsExampleEval("SygusEnumerator::enumTermsEvalExamples", 0),
-      d_enumTerms("SygusEnumerator::enumTerms", 0)
+    : d_cegqi_lemmas_ce(
+        smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_ce")),
+      d_cegqi_lemmas_refine(smtStatisticsRegistry().registerInt(
+          "SynthEngine::cegqi_lemmas_refine")),
+      d_cegqi_si_lemmas(
+          smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_si")),
+      d_solutions(
+          smtStatisticsRegistry().registerInt("SynthConjecture::solutions")),
+      d_filtered_solutions(smtStatisticsRegistry().registerInt(
+          "SynthConjecture::filtered_solutions")),
+      d_candidate_rewrites_print(smtStatisticsRegistry().registerInt(
+          "SynthConjecture::candidate_rewrites_print")),
+      d_enumTermsRewrite(smtStatisticsRegistry().registerInt(
+          "SygusEnumerator::enumTermsRewrite")),
+      d_enumTermsExampleEval(smtStatisticsRegistry().registerInt(
+          "SygusEnumerator::enumTermsEvalExamples")),
+      d_enumTerms(
+          smtStatisticsRegistry().registerInt("SygusEnumerator::enumTerms"))
 
 {
-  smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
-  smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
-  smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_solutions);
-  smtStatisticsRegistry()->registerStat(&d_filtered_solutions);
-  smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print);
-  smtStatisticsRegistry()->registerStat(&d_enumTermsRewrite);
-  smtStatisticsRegistry()->registerStat(&d_enumTermsExampleEval);
-  smtStatisticsRegistry()->registerStat(&d_enumTerms);
-}
-
-SygusStatistics::~SygusStatistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce);
-  smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
-  smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_solutions);
-  smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions);
-  smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print);
-  smtStatisticsRegistry()->unregisterStat(&d_enumTermsRewrite);
-  smtStatisticsRegistry()->unregisterStat(&d_enumTermsExampleEval);
-  smtStatisticsRegistry()->unregisterStat(&d_enumTerms);
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h
index 20b0633aa..6236547f9 100644
--- a/src/theory/quantifiers/sygus/sygus_stats.h
+++ b/src/theory/quantifiers/sygus/sygus_stats.h
@@ -18,7 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
 #define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
 
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -31,7 +31,6 @@ class SygusStatistics
 {
  public:
   SygusStatistics();
-  ~SygusStatistics();
   /** Number of counterexample lemmas */
   IntStat d_cegqi_lemmas_ce;
   /** Number of refinement lemmas */
diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp
index 4b714419f..2f21a50e1 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.cpp
+++ b/src/theory/quantifiers/term_tuple_enumerator.cpp
@@ -31,7 +31,7 @@
 #include "theory/quantifiers/term_pools.h"
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 301299f11..22b77c4fb 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -50,7 +50,7 @@ TheorySep::TheorySep(context::Context* c,
       d_lemmas_produced_c(u),
       d_bounds_init(false),
       d_state(c, u, valuation),
-      d_im(*this, d_state, nullptr, "theory::sep"),
+      d_im(*this, d_state, nullptr, "theory::sep::"),
       d_notify(*this),
       d_reduce(u),
       d_spatial_assertions(c)
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 2b90a46a3..3b8ec8b6b 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -28,7 +28,7 @@
 #include "theory/theory.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index a2d7b33a5..73c6db35f 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -28,7 +28,7 @@ namespace sets {
 InferenceManager::InferenceManager(Theory& t,
                                    SolverState& s,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, s, pnm, "theory::sets"), d_state(s)
+    : InferenceManagerBuffered(t, s, pnm, "theory::sets::"), d_state(s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 9e87e17a5..b9c331acc 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -29,7 +29,8 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
                                          context::UserContext* userContext,
                                          ProofNodeManager* pnm)
     : ContextNotifyObj(context),
-      d_statSharedTerms("theory::shared_terms", 0),
+      d_statSharedTerms(
+          smtStatisticsRegistry().registerInt("theory::shared_terms")),
       d_addedSharedTermsSize(context, 0),
       d_termsToTheories(context),
       d_alreadyNotifiedMap(context),
@@ -44,12 +45,6 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
       d_pfee(nullptr),
       d_pnm(pnm)
 {
-  smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
-}
-
-SharedTermsDatabase::~SharedTermsDatabase()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
 }
 
 void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index efc2b2154..655c2aa88 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -28,7 +28,7 @@
 #include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_equality_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -163,7 +163,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
                       context::Context* context,
                       context::UserContext* userContext,
                       ProofNodeManager* pnm);
-  ~SharedTermsDatabase();
 
   //-------------------------------------------- initialization
   /** Called to set the equality engine. */
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 7bb8bd3c1..e00668997 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -19,6 +19,7 @@
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/theory_strings_preprocess.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 8797e3fcd..2351e7bf3 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -23,6 +23,7 @@
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "util/statistics_registry.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 06bd4acc2..3dbb6b89b 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -35,7 +35,7 @@ InferenceManager::InferenceManager(Theory& t,
                                    ExtTheory& e,
                                    SequencesStatistics& statistics,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, s, pnm, "theory::strings", false),
+    : InferenceManagerBuffered(t, s, pnm, "theory::strings::", false),
       d_state(s),
       d_termReg(tr),
       d_extt(e),
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 05c218fa4..38fc6fc8f 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -22,6 +22,7 @@
 #include "theory/ext_theory.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/theory_model.h"
+#include "util/statistics_value.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index fa372771b..431f488a5 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -24,6 +24,7 @@
 #include "theory/strings/strings_rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -32,7 +33,7 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-SequencesRewriter::SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics)
+SequencesRewriter::SequencesRewriter(HistogramStat<Rewrite>* statistics)
     : d_statistics(statistics), d_stringsEntail(*this)
 {
 }
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 1564a5ebc..97db2c7f4 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -33,7 +33,7 @@ namespace strings {
 class SequencesRewriter : public TheoryRewriter
 {
  public:
-  SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics);
+  SequencesRewriter(HistogramStat<Rewrite>* statistics);
 
  protected:
   /** rewrite regular expression concatenation
@@ -288,7 +288,7 @@ class SequencesRewriter : public TheoryRewriter
   static Node canonicalStrForSymbolicLength(Node n, TypeNode stype);
 
   /** Reference to the rewriter statistics. */
-  IntegralHistogramStat<Rewrite>* d_statistics;
+  HistogramStat<Rewrite>* d_statistics;
 
   /** Instance of the entailment checker for strings. */
   StringsEntail d_stringsEntail;
diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp
index b27df959e..2c4834de2 100644
--- a/src/theory/strings/sequences_stats.cpp
+++ b/src/theory/strings/sequences_stats.cpp
@@ -22,44 +22,29 @@ namespace theory {
 namespace strings {
 
 SequencesStatistics::SequencesStatistics()
-    : d_checkRuns("theory::strings::checkRuns", 0),
-      d_strategyRuns("theory::strings::strategyRuns", 0),
-      d_inferencesNoPf("theory::strings::inferencesNoPf"),
-      d_cdSimplifications("theory::strings::cdSimplifications"),
-      d_reductions("theory::strings::reductions"),
-      d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"),
-      d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"),
-      d_rewrites("theory::strings::rewrites"),
-      d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
-      d_conflictsEager("theory::strings::conflictsEager", 0),
-      d_conflictsInfer("theory::strings::conflictsInfer", 0)
+    : d_checkRuns(
+        smtStatisticsRegistry().registerInt("theory::strings::checkRuns")),
+      d_strategyRuns(
+          smtStatisticsRegistry().registerInt("theory::strings::strategyRuns")),
+      d_inferencesNoPf(smtStatisticsRegistry().registerHistogram<InferenceId>(
+          "theory::strings::inferencesNoPf")),
+      d_cdSimplifications(smtStatisticsRegistry().registerHistogram<Kind>(
+          "theory::strings::cdSimplifications")),
+      d_reductions(smtStatisticsRegistry().registerHistogram<Kind>(
+          "theory::strings::reductions")),
+      d_regexpUnfoldingsPos(smtStatisticsRegistry().registerHistogram<Kind>(
+          "theory::strings::regexpUnfoldingsPos")),
+      d_regexpUnfoldingsNeg(smtStatisticsRegistry().registerHistogram<Kind>(
+          "theory::strings::regexpUnfoldingsNeg")),
+      d_rewrites(smtStatisticsRegistry().registerHistogram<Rewrite>(
+          "theory::strings::rewrites")),
+      d_conflictsEqEngine(smtStatisticsRegistry().registerInt(
+          "theory::strings::conflictsEqEngine")),
+      d_conflictsEager(smtStatisticsRegistry().registerInt(
+          "theory::strings::conflictsEager")),
+      d_conflictsInfer(smtStatisticsRegistry().registerInt(
+          "theory::strings::conflictsInfer"))
 {
-  smtStatisticsRegistry()->registerStat(&d_checkRuns);
-  smtStatisticsRegistry()->registerStat(&d_strategyRuns);
-  smtStatisticsRegistry()->registerStat(&d_inferencesNoPf);
-  smtStatisticsRegistry()->registerStat(&d_cdSimplifications);
-  smtStatisticsRegistry()->registerStat(&d_reductions);
-  smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos);
-  smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg);
-  smtStatisticsRegistry()->registerStat(&d_rewrites);
-  smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
-  smtStatisticsRegistry()->registerStat(&d_conflictsEager);
-  smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
-}
-
-SequencesStatistics::~SequencesStatistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
-  smtStatisticsRegistry()->unregisterStat(&d_strategyRuns);
-  smtStatisticsRegistry()->unregisterStat(&d_inferencesNoPf);
-  smtStatisticsRegistry()->unregisterStat(&d_cdSimplifications);
-  smtStatisticsRegistry()->unregisterStat(&d_reductions);
-  smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos);
-  smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg);
-  smtStatisticsRegistry()->unregisterStat(&d_rewrites);
-  smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
-  smtStatisticsRegistry()->unregisterStat(&d_conflictsEager);
-  smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
 }
 
 }
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index e442fcc0c..398b8894d 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -21,8 +21,7 @@
 #include "expr/kind.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/rewrites.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -53,7 +52,6 @@ class SequencesStatistics
 {
  public:
   SequencesStatistics();
-  ~SequencesStatistics();
   /** Number of calls to run a check where strategy is present */
   IntStat d_checkRuns;
   /** Number of calls to run the strategy */
@@ -65,29 +63,29 @@ class SequencesStatistics
    * TheoryInferenceManager, i.e.
    * (theory::strings::inferences{Facts,Lemmas,Conflicts}).
    */
-  IntegralHistogramStat<InferenceId> d_inferencesNoPf;
+  HistogramStat<InferenceId> d_inferencesNoPf;
   /**
    * Counts the number of applications of each type of context-dependent
    * simplification. The sum of this map is equal to the number of EXTF or
    * EXTF_N inferences.
    */
-  IntegralHistogramStat<Kind> d_cdSimplifications;
+  HistogramStat<Kind> d_cdSimplifications;
   /**
    * Counts the number of applications of each type of reduction. The sum of
    * this map is equal to the number of REDUCTION inferences (when
    * options::stringLazyPreproc is true).
    */
-  IntegralHistogramStat<Kind> d_reductions;
+  HistogramStat<Kind> d_reductions;
   /**
    * Counts the number of applications of each type of regular expression
    * positive (resp. negative) unfoldings. The sum of this map is equal to the
    * number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences.
    */
-  IntegralHistogramStat<Kind> d_regexpUnfoldingsPos;
-  IntegralHistogramStat<Kind> d_regexpUnfoldingsNeg;
+  HistogramStat<Kind> d_regexpUnfoldingsPos;
+  HistogramStat<Kind> d_regexpUnfoldingsNeg;
   //--------------- end of inferences
   /** Counts the number of applications of each type of rewrite rule */
-  IntegralHistogramStat<Rewrite> d_rewrites;
+  HistogramStat<Rewrite> d_rewrites;
   //--------------- conflicts, partition of calls to OutputChannel::conflict
   /** Number of equality engine conflicts */
   IntStat d_conflictsEqEngine;
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 4ef3f7c96..41a8ac448 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -26,7 +26,7 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-StringsRewriter::StringsRewriter(IntegralHistogramStat<Rewrite>* statistics)
+StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics)
     : SequencesRewriter(statistics)
 {
 }
diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h
index bfe780535..70a1cccf0 100644
--- a/src/theory/strings/strings_rewriter.h
+++ b/src/theory/strings/strings_rewriter.h
@@ -32,7 +32,7 @@ namespace strings {
 class StringsRewriter : public SequencesRewriter
 {
  public:
-  StringsRewriter(IntegralHistogramStat<Rewrite>* statistics);
+  StringsRewriter(HistogramStat<Rewrite>* statistics);
 
   RewriteResponse postRewrite(TNode node) override;
 
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 5e6b27e1b..1cc0736fb 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -25,6 +25,7 @@
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/word.h"
+#include "util/statistics_registry.h"
 
 using namespace cvc5;
 using namespace cvc5::kind;
@@ -41,7 +42,7 @@ struct QInternalVarAttributeId
 typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
 
 StringsPreprocess::StringsPreprocess(SkolemCache* sc,
-                                     IntegralHistogramStat<Kind>* statReductions)
+                                     HistogramStat<Kind>* statReductions)
     : d_sc(sc), d_statReductions(statReductions)
 {
 }
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index fe190532d..7f0efe50f 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -40,7 +40,7 @@ namespace strings {
 class StringsPreprocess {
  public:
   StringsPreprocess(SkolemCache* sc,
-                    IntegralHistogramStat<Kind>* statReductions = nullptr);
+                    HistogramStat<Kind>* statReductions = nullptr);
   ~StringsPreprocess();
   /** The reduce routine
    *
@@ -82,7 +82,7 @@ class StringsPreprocess {
   /** pointer to the skolem cache used by this class */
   SkolemCache* d_sc;
   /** Reference to the statistics for the theory of strings/sequences. */
-  IntegralHistogramStat<Kind>* d_statReductions;
+  HistogramStat<Kind>* d_statReductions;
   /** visited cache */
   std::map<Node, Node> d_visited;
   /**
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 78a83c4da..859356341 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -75,9 +75,10 @@ Theory::Theory(TheoryId id,
       d_sharedTermsIndex(satContext, 0),
       d_careGraph(nullptr),
       d_instanceName(name),
-      d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
-      d_computeCareGraphTime(getStatsPrefix(id) + name
-                             + "::computeCareGraphTime"),
+      d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id)
+                                                        + name + "checkTime")),
+      d_computeCareGraphTime(smtStatisticsRegistry().registerTimer(
+          getStatsPrefix(id) + name + "computeCareGraphTime")),
       d_sharedTerms(satContext),
       d_out(&out),
       d_valuation(valuation),
@@ -88,13 +89,9 @@ Theory::Theory(TheoryId id,
       d_quantEngine(nullptr),
       d_pnm(pnm)
 {
-  smtStatisticsRegistry()->registerStat(&d_checkTime);
-  smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
 }
 
 Theory::~Theory() {
-  smtStatisticsRegistry()->unregisterStat(&d_checkTime);
-  smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
 }
 
 bool Theory::needsEqualityEngine(EeSetupInfo& esi)
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3d3ec0627..247ebcf46 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -35,8 +35,7 @@
 #include "theory/theory_id.h"
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 79f9c660f..b4ad09d77 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -218,10 +218,9 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_outMgr(outMgr),
       d_pnm(pnm),
       d_lazyProof(
-          d_pnm != nullptr
-              ? new LazyCDProof(
-                    d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
-              : nullptr),
+          d_pnm != nullptr ? new LazyCDProof(
+              d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
+                           : nullptr),
       d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
       d_tc(nullptr),
       d_sharedSolver(nullptr),
@@ -240,7 +239,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_propagatedLiterals(context),
       d_propagatedLiteralsIndex(context, 0),
       d_atomRequests(context),
-      d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+      d_combineTheoriesTime(smtStatisticsRegistry().registerTimer(
+          "TheoryEngine::combineTheoriesTime")),
       d_true(),
       d_false(),
       d_interrupted(false),
@@ -261,7 +261,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
     d_sortInfer.reset(new SortInference);
   }
 
-  smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }
@@ -275,8 +274,6 @@ TheoryEngine::~TheoryEngine() {
       delete d_theoryOut[theoryId];
     }
   }
-
-  smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
 }
 
 void TheoryEngine::interrupt() { d_interrupted = true; }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index dcf4ff2c8..3eacdaa20 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -37,7 +37,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace cvc5 {
diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index d3f225f79..d9b25bf98 100644
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -59,23 +59,23 @@ std::string getStatsPrefix(TheoryId theoryId)
 {
   switch (theoryId)
   {
-    case THEORY_BUILTIN: return "theory::builtin"; break;
-    case THEORY_BOOL: return "theory::bool"; break;
-    case THEORY_UF: return "theory::uf"; break;
-    case THEORY_ARITH: return "theory::arith"; break;
-    case THEORY_BV: return "theory::bv"; break;
-    case THEORY_FP: return "theory::fp"; break;
-    case THEORY_ARRAYS: return "theory::arrays"; break;
-    case THEORY_DATATYPES: return "theory::datatypes"; break;
-    case THEORY_SEP: return "theory::sep"; break;
-    case THEORY_SETS: return "theory::sets"; break;
-    case THEORY_BAGS: return "theory::bags"; break;
-    case THEORY_STRINGS: return "theory::strings"; break;
-    case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
+    case THEORY_BUILTIN: return "theory::builtin::"; break;
+    case THEORY_BOOL: return "theory::bool::"; break;
+    case THEORY_UF: return "theory::uf::"; break;
+    case THEORY_ARITH: return "theory::arith::"; break;
+    case THEORY_BV: return "theory::bv::"; break;
+    case THEORY_FP: return "theory::fp::"; break;
+    case THEORY_ARRAYS: return "theory::arrays::"; break;
+    case THEORY_DATATYPES: return "theory::datatypes::"; break;
+    case THEORY_SEP: return "theory::sep::"; break;
+    case THEORY_SETS: return "theory::sets::"; break;
+    case THEORY_BAGS: return "theory::bags::"; break;
+    case THEORY_STRINGS: return "theory::strings::"; break;
+    case THEORY_QUANTIFIERS: return "theory::quantifiers::"; break;
 
     default: break;
   }
-  return "unknown";
+  return "unknown::";
 }
 
 TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set)
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index e52321c49..3bc7351fe 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -31,7 +31,7 @@ namespace theory {
 TheoryInferenceManager::TheoryInferenceManager(Theory& t,
                                                TheoryState& state,
                                                ProofNodeManager* pnm,
-                                               const std::string& name,
+                                               const std::string& statsName,
                                                bool cacheLemmas)
     : d_theory(t),
       d_theoryState(state),
@@ -45,23 +45,20 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t,
       d_numConflicts(0),
       d_numCurrentLemmas(0),
       d_numCurrentFacts(0),
-      d_conflictIdStats(name + "::inferencesConflict"),
-      d_factIdStats(name + "::inferencesFact"),
-      d_lemmaIdStats(name + "::inferencesLemma")
+      d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+          statsName + "inferencesConflict")),
+      d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+          statsName + "inferencesFact")),
+      d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+          statsName + "inferencesLemma"))
 {
   // don't add true lemma
   Node truen = NodeManager::currentNM()->mkConst(true);
   d_lemmasSent.insert(truen);
-  smtStatisticsRegistry()->registerStat(&d_conflictIdStats);
-  smtStatisticsRegistry()->registerStat(&d_factIdStats);
-  smtStatisticsRegistry()->registerStat(&d_lemmaIdStats);
 }
 
 TheoryInferenceManager::~TheoryInferenceManager()
 {
-  smtStatisticsRegistry()->unregisterStat(&d_conflictIdStats);
-  smtStatisticsRegistry()->unregisterStat(&d_factIdStats);
-  smtStatisticsRegistry()->unregisterStat(&d_lemmaIdStats);
 }
 
 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 89c4aec3f..a785af186 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -26,8 +26,7 @@
 #include "theory/inference_id.h"
 #include "theory/output_channel.h"
 #include "theory/trust_node.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 
@@ -79,8 +78,8 @@ class TheoryInferenceManager
    * @param state The state of the theory
    * @param pnm The proof node manager, which if non-null, enables proofs for
    * this inference manager
-   * @param name The name of the inference manager, which is used for giving
-   * unique names for statistics,
+   * @param statsName The name of the inference manager, which is used for
+   * giving unique names for statistics,
    * @param cacheLemmas Whether all lemmas sent using this theory inference
    * manager are added to a user-context dependent cache. This means that
    * only lemmas that are unique after rewriting are sent to the theory engine
@@ -89,7 +88,7 @@ class TheoryInferenceManager
   TheoryInferenceManager(Theory& t,
                          TheoryState& state,
                          ProofNodeManager* pnm,
-                         const std::string& name,
+                         const std::string& statsName,
                          bool cacheLemmas = true);
   virtual ~TheoryInferenceManager();
   //--------------------------------------- initialization
@@ -454,11 +453,11 @@ class TheoryInferenceManager
   /** The number of internal facts added since the last call to reset. */
   uint32_t d_numCurrentFacts;
   /** Statistics for conflicts sent via this inference manager. */
-  IntegralHistogramStat<InferenceId> d_conflictIdStats;
+  HistogramStat<InferenceId> d_conflictIdStats;
   /** Statistics for facts sent via this inference manager. */
-  IntegralHistogramStat<InferenceId> d_factIdStats;
+  HistogramStat<InferenceId> d_factIdStats;
   /** Statistics for lemmas sent via this inference manager. */
-  IntegralHistogramStat<InferenceId> d_lemmaIdStats;
+  HistogramStat<InferenceId> d_lemmaIdStats;
 };
 
 }  // namespace theory
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b45ccbac3..25f87de2c 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1748,23 +1748,16 @@ void CardinalityExtension::checkCombinedCardinality()
 }
 
 CardinalityExtension::Statistics::Statistics()
-    : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
-      d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
-      d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
-      d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
+    : d_clique_conflicts(smtStatisticsRegistry().registerInt(
+        "CardinalityExtension::Clique_Conflicts")),
+      d_clique_lemmas(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Clique_Lemmas")),
+      d_split_lemmas(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Split_Lemmas")),
+      d_max_model_size(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Max_Model_Size"))
 {
-  smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
-  smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_split_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_max_model_size);
-}
-
-CardinalityExtension::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
+  d_max_model_size.maxAssign(1);
 }
 
 }  // namespace uf
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 53c850897..70db9257f 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -22,7 +22,7 @@
 #include "context/context.h"
 #include "theory/decision_strategy.h"
 #include "theory/theory.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -397,7 +397,6 @@ class CardinalityExtension
     IntStat d_split_lemmas;
     IntStat d_max_model_size;
     Statistics();
-    ~Statistics();
   };
   /** statistics class */
   Statistics d_statistics;
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index fe7b0ab84..7124a8890 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -29,23 +29,14 @@ namespace cvc5 {
 namespace theory {
 namespace eq {
 
-EqualityEngine::Statistics::Statistics(std::string name)
-    : d_mergesCount(name + "::mergesCount", 0),
-      d_termsCount(name + "::termsCount", 0),
-      d_functionTermsCount(name + "::functionTermsCount", 0),
-      d_constantTermsCount(name + "::constantTermsCount", 0)
+EqualityEngine::Statistics::Statistics(const std::string& name)
+    : d_mergesCount(smtStatisticsRegistry().registerInt(name + "mergesCount")),
+      d_termsCount(smtStatisticsRegistry().registerInt(name + "termsCount")),
+      d_functionTermsCount(
+          smtStatisticsRegistry().registerInt(name + "functionTermsCount")),
+      d_constantTermsCount(
+          smtStatisticsRegistry().registerInt(name + "constantTermsCount"))
 {
-  smtStatisticsRegistry()->registerStat(&d_mergesCount);
-  smtStatisticsRegistry()->registerStat(&d_termsCount);
-  smtStatisticsRegistry()->registerStat(&d_functionTermsCount);
-  smtStatisticsRegistry()->registerStat(&d_constantTermsCount);
-}
-
-EqualityEngine::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_mergesCount);
-  smtStatisticsRegistry()->unregisterStat(&d_termsCount);
-  smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount);
-  smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount);
 }
 
 /**
@@ -128,7 +119,7 @@ EqualityEngine::EqualityEngine(context::Context* context,
       d_assertedEqualitiesCount(context, 0),
       d_equalityTriggersCount(context, 0),
       d_subtermEvaluatesSize(context, 0),
-      d_stats(name),
+      d_stats(name + "::"),
       d_inPropagate(false),
       d_constantsAreTriggers(constantsAreTriggers),
       d_anyTermsAreTriggers(anyTermTriggers),
@@ -158,7 +149,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
       d_assertedEqualitiesCount(context, 0),
       d_equalityTriggersCount(context, 0),
       d_subtermEvaluatesSize(context, 0),
-      d_stats(name),
+      d_stats(name + "::"),
       d_inPropagate(false),
       d_constantsAreTriggers(constantsAreTriggers),
       d_anyTermsAreTriggers(anyTermTriggers),
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index d8a8f3916..8676e446e 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -34,7 +34,7 @@
 #include "theory/uf/equality_engine_iterator.h"
 #include "theory/uf/equality_engine_notify.h"
 #include "theory/uf/equality_engine_types.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -109,9 +109,7 @@ class EqualityEngine : public context::ContextNotifyObj {
     /** Number of constant terms managed by the system */
     IntStat d_constantTermsCount;
 
-    Statistics(std::string name);
-
-    ~Statistics();
+    Statistics(const std::string& name);
   };/* struct EqualityEngine::statistics */
 
 private:
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 49b056f5a..65ed4d542 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -164,21 +164,20 @@ void SymmetryBreaker::Template::reset() {
   d_reps.clear();
 }
 
-SymmetryBreaker::SymmetryBreaker(context::Context* context,
-                                 std::string name) :
-  ContextNotifyObj(context),
-  d_assertionsToRerun(context),
-  d_rerunningAssertions(false),
-  d_phi(),
-  d_phiSet(),
-  d_permutations(),
-  d_terms(),
-  d_template(),
-  d_normalizationCache(),
-  d_termEqs(),
-  d_termEqsOnly(),
-  d_name(name),
-  d_stats(d_name)
+SymmetryBreaker::SymmetryBreaker(context::Context* context, std::string name)
+    : ContextNotifyObj(context),
+      d_assertionsToRerun(context),
+      d_rerunningAssertions(false),
+      d_phi(),
+      d_phiSet(),
+      d_permutations(),
+      d_terms(),
+      d_template(),
+      d_normalizationCache(),
+      d_termEqs(),
+      d_termEqsOnly(),
+      d_name(name),
+      d_stats(d_name + "theory::uf::symmetry_breaker::")
 {
 }
 
@@ -750,33 +749,20 @@ void SymmetryBreaker::selectTerms(const Permutation& p) {
   }
 }
 
-SymmetryBreaker::Statistics::Statistics(std::string name)
-  : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
-  , d_units(name + "theory::uf::symmetry_breaker::units", 0)
-  , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
-  , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
-  , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
-  , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
-  , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
-{
-  smtStatisticsRegistry()->registerStat(&d_clauses);
-  smtStatisticsRegistry()->registerStat(&d_units);
-  smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
-  smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
-  smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
-  smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
-  smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
-}
-
-SymmetryBreaker::Statistics::~Statistics()
+SymmetryBreaker::Statistics::Statistics(const std::string& name)
+    : d_clauses(smtStatisticsRegistry().registerInt(name + "clauses")),
+      d_units(smtStatisticsRegistry().registerInt(name + "units")),
+      d_permutationSetsConsidered(smtStatisticsRegistry().registerInt(
+          name + "permutationSetsConsidered")),
+      d_permutationSetsInvariant(smtStatisticsRegistry().registerInt(
+          name + "permutationSetsInvariant")),
+      d_invariantByPermutationsTimer(smtStatisticsRegistry().registerTimer(
+          name + "timers::invariantByPermutations")),
+      d_selectTermsTimer(
+          smtStatisticsRegistry().registerTimer(name + "timers::selectTerms")),
+      d_initNormalizationTimer(smtStatisticsRegistry().registerTimer(
+          name + "timers::initNormalization"))
 {
-  smtStatisticsRegistry()->unregisterStat(&d_clauses);
-  smtStatisticsRegistry()->unregisterStat(&d_units);
-  smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
-  smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
-  smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
 }
 
 SymmetryBreaker::Terms::iterator
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index eb78f9101..b5d0fbdf9 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -52,8 +52,7 @@
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "smt/smt_statistics_registry.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
 
 namespace cvc5 {
 namespace theory {
@@ -147,8 +146,7 @@ private:
     /** time spent in initial round of normalization */
     TimerStat d_initNormalizationTimer;
 
-    Statistics(std::string name);
-    ~Statistics();
+    Statistics(const std::string& name);
   };
 
   Statistics d_stats;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9fa86f402..5d91faa87 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -53,7 +53,7 @@ TheoryUF::TheoryUF(context::Context* c,
       d_functionsTerms(c),
       d_symb(u, instanceName),
       d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::uf", false),
+      d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false),
       d_notify(d_im, *this)
 {
   d_true = NodeManager::currentNM()->mkConst( true );