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.

30 files changed, 352 insertions, 626 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);
   };