Removing StatisticsRegistry's static functions current() and registerStat().

- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.

26 files changed, 412 insertions, 398 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 71ac18e84..5bbe29bc5 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -14,6 +14,7 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "theory/arith/approx_simplex.h"
 
 #include <cfloat>
 #include <cmath>
@@ -22,7 +23,7 @@
 
 #include "base/output.h"
 #include "cvc4autoconfig.h"
-#include "theory/arith/approx_simplex.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/cut_log.h"
 #include "theory/arith/matrix.h"
@@ -169,67 +170,67 @@ ApproximateStatistics::ApproximateStatistics()
   ,  d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0)
   ,  d_averageGuesses("z::approx::averageGuesses")
 {
-  // StatisticsRegistry::registerStat(&d_relaxCalls);
-  // StatisticsRegistry::registerStat(&d_relaxUnknowns);
-  // StatisticsRegistry::registerStat(&d_relaxFeasible);
-  // StatisticsRegistry::registerStat(&d_relaxInfeasible);
-  // StatisticsRegistry::registerStat(&d_relaxPivotsExhausted);
-
-  // StatisticsRegistry::registerStat(&d_mipCalls);
-  // StatisticsRegistry::registerStat(&d_mipUnknowns);
-  // StatisticsRegistry::registerStat(&d_mipBingo);
-  // StatisticsRegistry::registerStat(&d_mipClosed);
-  // StatisticsRegistry::registerStat(&d_mipBranchesExhausted);
-  // StatisticsRegistry::registerStat(&d_mipPivotsExhausted);
-  // StatisticsRegistry::registerStat(&d_mipExecExhausted);
-
-
-  // StatisticsRegistry::registerStat(&d_gmiGen);
-  // StatisticsRegistry::registerStat(&d_gmiReplay);
-  // StatisticsRegistry::registerStat(&d_mipGen);
-  // StatisticsRegistry::registerStat(&d_mipReplay);
-
-  StatisticsRegistry::registerStat(&d_branchMaxDepth);
-  //StatisticsRegistry::registerStat(&d_branchTotal);
-  //StatisticsRegistry::registerStat(&d_branchCuts);
-  StatisticsRegistry::registerStat(&d_branchesMaxOnAVar);
-
-  StatisticsRegistry::registerStat(&d_gaussianElimConstructTime);
-  StatisticsRegistry::registerStat(&d_gaussianElimConstruct);
-
-  StatisticsRegistry::registerStat(&d_averageGuesses);
+  // smtStatisticsRegistry()->registerStat(&d_relaxCalls);
+  // smtStatisticsRegistry()->registerStat(&d_relaxUnknowns);
+  // smtStatisticsRegistry()->registerStat(&d_relaxFeasible);
+  // smtStatisticsRegistry()->registerStat(&d_relaxInfeasible);
+  // smtStatisticsRegistry()->registerStat(&d_relaxPivotsExhausted);
+
+  // smtStatisticsRegistry()->registerStat(&d_mipCalls);
+  // smtStatisticsRegistry()->registerStat(&d_mipUnknowns);
+  // smtStatisticsRegistry()->registerStat(&d_mipBingo);
+  // smtStatisticsRegistry()->registerStat(&d_mipClosed);
+  // smtStatisticsRegistry()->registerStat(&d_mipBranchesExhausted);
+  // smtStatisticsRegistry()->registerStat(&d_mipPivotsExhausted);
+  // smtStatisticsRegistry()->registerStat(&d_mipExecExhausted);
+
+
+  // smtStatisticsRegistry()->registerStat(&d_gmiGen);
+  // smtStatisticsRegistry()->registerStat(&d_gmiReplay);
+  // smtStatisticsRegistry()->registerStat(&d_mipGen);
+  // smtStatisticsRegistry()->registerStat(&d_mipReplay);
+
+  smtStatisticsRegistry()->registerStat(&d_branchMaxDepth);
+  //smtStatisticsRegistry()->registerStat(&d_branchTotal);
+  //smtStatisticsRegistry()->registerStat(&d_branchCuts);
+  smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar);
+
+  smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime);
+  smtStatisticsRegistry()->registerStat(&d_gaussianElimConstruct);
+
+  smtStatisticsRegistry()->registerStat(&d_averageGuesses);
 }
 
 ApproximateStatistics::~ApproximateStatistics(){
-  // StatisticsRegistry::unregisterStat(&d_relaxCalls);
-  // StatisticsRegistry::unregisterStat(&d_relaxUnknowns);
-  // StatisticsRegistry::unregisterStat(&d_relaxFeasible);
-  // StatisticsRegistry::unregisterStat(&d_relaxInfeasible);
-  // StatisticsRegistry::unregisterStat(&d_relaxPivotsExhausted);
-
-  // StatisticsRegistry::unregisterStat(&d_mipCalls);
-  // StatisticsRegistry::unregisterStat(&d_mipUnknowns);
-  // StatisticsRegistry::unregisterStat(&d_mipBingo);
-  // StatisticsRegistry::unregisterStat(&d_mipClosed);
-  // StatisticsRegistry::unregisterStat(&d_mipBranchesExhausted);
-  // StatisticsRegistry::unregisterStat(&d_mipPivotsExhausted);
-  // StatisticsRegistry::unregisterStat(&d_mipExecExhausted);
-
-
-  // StatisticsRegistry::unregisterStat(&d_gmiGen);
-  // StatisticsRegistry::unregisterStat(&d_gmiReplay);
-  // StatisticsRegistry::unregisterStat(&d_mipGen);
-  // StatisticsRegistry::unregisterStat(&d_mipReplay);
-
-  StatisticsRegistry::unregisterStat(&d_branchMaxDepth);
-  //StatisticsRegistry::unregisterStat(&d_branchTotal);
-  //StatisticsRegistry::unregisterStat(&d_branchCuts);
-  StatisticsRegistry::unregisterStat(&d_branchesMaxOnAVar);
-
-  StatisticsRegistry::unregisterStat(&d_gaussianElimConstructTime);
-  StatisticsRegistry::unregisterStat(&d_gaussianElimConstruct);
-
-  StatisticsRegistry::unregisterStat(&d_averageGuesses);
+  // smtStatisticsRegistry()->unregisterStat(&d_relaxCalls);
+  // smtStatisticsRegistry()->unregisterStat(&d_relaxUnknowns);
+  // smtStatisticsRegistry()->unregisterStat(&d_relaxFeasible);
+  // smtStatisticsRegistry()->unregisterStat(&d_relaxInfeasible);
+  // smtStatisticsRegistry()->unregisterStat(&d_relaxPivotsExhausted);
+
+  // smtStatisticsRegistry()->unregisterStat(&d_mipCalls);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipUnknowns);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipBingo);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipClosed);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipBranchesExhausted);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipPivotsExhausted);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipExecExhausted);
+
+
+  // smtStatisticsRegistry()->unregisterStat(&d_gmiGen);
+  // smtStatisticsRegistry()->unregisterStat(&d_gmiReplay);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipGen);
+  // smtStatisticsRegistry()->unregisterStat(&d_mipReplay);
+
+  smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth);
+  //smtStatisticsRegistry()->unregisterStat(&d_branchTotal);
+  //smtStatisticsRegistry()->unregisterStat(&d_branchCuts);
+  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 064887787..97e6d6b3e 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -21,11 +21,11 @@
 #pragma once
 #include <vector>
 
-#include "expr/statistics_registry.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "util/dense_map.h"
 #include "util/rational.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 383c6b418..aac792377 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -21,6 +21,7 @@
 #include "expr/convenience_node_builders.h"
 #include "expr/expr.h"
 #include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
@@ -48,13 +49,13 @@ ArithStaticLearner::Statistics::Statistics():
   d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
   d_iteConstantApplications("theory::arith::iteConstantApplications", 0)
 {
-  StatisticsRegistry::registerStat(&d_iteMinMaxApplications);
-  StatisticsRegistry::registerStat(&d_iteConstantApplications);
+  smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications);
+  smtStatisticsRegistry()->registerStat(&d_iteConstantApplications);
 }
 
 ArithStaticLearner::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications);
-  StatisticsRegistry::unregisterStat(&d_iteConstantApplications);
+  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 2b0ee9dad..2aa9c9332 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -24,8 +24,8 @@
 
 #include "context/cdtrail_hashmap.h"
 #include "context/context.h"
-#include "expr/statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 737cc9e7b..d7b31e2e2 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -14,10 +14,11 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "theory/arith/attempt_solution_simplex.h"
 
 #include "base/output.h"
 #include "options/arith_options.h"
-#include "theory/arith/attempt_solution_simplex.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 
 using namespace std;
@@ -36,15 +37,15 @@ AttemptSolutionSDP::Statistics::Statistics():
   d_queueTime("theory::arith::attempt::queueTime"),
   d_conflicts("theory::arith::attempt::conflicts", 0)
 {
-  StatisticsRegistry::registerStat(&d_searchTime);
-  StatisticsRegistry::registerStat(&d_queueTime);
-  StatisticsRegistry::registerStat(&d_conflicts);
+  smtStatisticsRegistry()->registerStat(&d_searchTime);
+  smtStatisticsRegistry()->registerStat(&d_queueTime);
+  smtStatisticsRegistry()->registerStat(&d_conflicts);
 }
 
 AttemptSolutionSDP::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_searchTime);
-  StatisticsRegistry::unregisterStat(&d_queueTime);
-  StatisticsRegistry::unregisterStat(&d_conflicts);
+  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 88d29f6b0..49a2dda29 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -53,9 +53,9 @@
 
 #pragma once
 
-#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/approx_simplex.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -94,4 +94,3 @@ private:
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 964c92eb5..746121b70 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -13,10 +13,11 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "theory/arith/congruence_manager.h"
 
 #include "base/output.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint.h"
 
 namespace CVC4 {
@@ -45,23 +46,23 @@ ArithCongruenceManager::Statistics::Statistics():
   d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
   d_conflicts("theory::arith::congruence::conflicts", 0)
 {
-  StatisticsRegistry::registerStat(&d_watchedVariables);
-  StatisticsRegistry::registerStat(&d_watchedVariableIsZero);
-  StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero);
-  StatisticsRegistry::registerStat(&d_equalsConstantCalls);
-  StatisticsRegistry::registerStat(&d_propagations);
-  StatisticsRegistry::registerStat(&d_propagateConstraints);
-  StatisticsRegistry::registerStat(&d_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(){
-  StatisticsRegistry::unregisterStat(&d_watchedVariables);
-  StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero);
-  StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero);
-  StatisticsRegistry::unregisterStat(&d_equalsConstantCalls);
-  StatisticsRegistry::unregisterStat(&d_propagations);
-  StatisticsRegistry::unregisterStat(&d_propagateConstraints);
-  StatisticsRegistry::unregisterStat(&d_conflicts);
+  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 2fc9c47ed..138805b6e 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -24,12 +24,12 @@
 #include "context/cdo.h"
 #include "context/cdtrail_queue.h"
 #include "context/context.h"
-#include "expr/statistics_registry.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/partial_model.h"
 #include "theory/uf/equality_engine.h"
 #include "util/dense_map.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index f13565a7f..5dc0ba1ac 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -14,14 +14,15 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "theory/arith/constraint.h"
 
 #include <ostream>
 #include <algorithm>
 
 #include "base/output.h"
 #include "proof/proof.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/constraint.h"
 #include "theory/arith/normal_form.h"
 
 
@@ -893,13 +894,14 @@ ConstraintDatabase::Statistics::Statistics():
   d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
   d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
 {
-  StatisticsRegistry::registerStat(&d_unatePropagateCalls);
-  StatisticsRegistry::registerStat(&d_unatePropagateImplications);
+  smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls);
+  smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications);
 
 }
+
 ConstraintDatabase::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_unatePropagateCalls);
-  StatisticsRegistry::unregisterStat(&d_unatePropagateImplications);
+  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls);
+  smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications);
 }
 
 void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index f4d392995..054ab01e7 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -26,10 +26,10 @@
 #include <vector>
 
 #include "expr/kind.h"
-#include "expr/statistics_registry.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/dense_map.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index f8b8e0e7b..71ad6de45 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -13,12 +13,13 @@
  **
  ** A Diophantine equation solver for the theory of arithmetic.
  **/
+#include "theory/arith/dio_solver.h"
 
 #include <iostream>
 
 #include "base/output.h"
 #include "options/arith_options.h"
-#include "theory/arith/dio_solver.h"
+#include "smt/smt_statistics_registry.h"
 
 using namespace std;
 
@@ -56,25 +57,25 @@ DioSolver::Statistics::Statistics() :
   d_conflictTimer("theory::arith::dio::conflictTimer"),
   d_cutTimer("theory::arith::dio::cutTimer")
 {
-  StatisticsRegistry::registerStat(&d_conflictCalls);
-  StatisticsRegistry::registerStat(&d_cutCalls);
+  smtStatisticsRegistry()->registerStat(&d_conflictCalls);
+  smtStatisticsRegistry()->registerStat(&d_cutCalls);
 
-  StatisticsRegistry::registerStat(&d_cuts);
-  StatisticsRegistry::registerStat(&d_conflicts);
+  smtStatisticsRegistry()->registerStat(&d_cuts);
+  smtStatisticsRegistry()->registerStat(&d_conflicts);
 
-  StatisticsRegistry::registerStat(&d_conflictTimer);
-  StatisticsRegistry::registerStat(&d_cutTimer);
+  smtStatisticsRegistry()->registerStat(&d_conflictTimer);
+  smtStatisticsRegistry()->registerStat(&d_cutTimer);
 }
 
 DioSolver::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_conflictCalls);
-  StatisticsRegistry::unregisterStat(&d_cutCalls);
+  smtStatisticsRegistry()->unregisterStat(&d_conflictCalls);
+  smtStatisticsRegistry()->unregisterStat(&d_cutCalls);
 
-  StatisticsRegistry::unregisterStat(&d_cuts);
-  StatisticsRegistry::unregisterStat(&d_conflicts);
+  smtStatisticsRegistry()->unregisterStat(&d_cuts);
+  smtStatisticsRegistry()->unregisterStat(&d_conflicts);
 
-  StatisticsRegistry::unregisterStat(&d_conflictTimer);
-  StatisticsRegistry::unregisterStat(&d_cutTimer);
+  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 626160b03..ccaff47c7 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -28,10 +28,10 @@
 #include "context/cdo.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
-#include "expr/statistics_registry.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
 #include "util/rational.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 32f81ded8..907d5eefb 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -14,11 +14,13 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "theory/arith/dual_simplex.h"
 
 #include "base/output.h"
 #include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
-#include "theory/arith/dual_simplex.h"
+
 
 using namespace std;
 
@@ -40,21 +42,21 @@ DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
   d_searchTime("theory::arith::dual::searchTime"),
   d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots)
 {
-  StatisticsRegistry::registerStat(&d_statUpdateConflicts);
-  StatisticsRegistry::registerStat(&d_processSignalsTime);
-  StatisticsRegistry::registerStat(&d_simplexConflicts);
-  StatisticsRegistry::registerStat(&d_recentViolationCatches);
-  StatisticsRegistry::registerStat(&d_searchTime);
-  StatisticsRegistry::registerStat(&d_finalCheckPivotCounter);
+  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(){
-  StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
-  StatisticsRegistry::unregisterStat(&d_processSignalsTime);
-  StatisticsRegistry::unregisterStat(&d_simplexConflicts);
-  StatisticsRegistry::unregisterStat(&d_recentViolationCatches);
-  StatisticsRegistry::unregisterStat(&d_searchTime);
-  StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter);
+  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 d6bf57bb0..e5ab76da8 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -52,8 +52,8 @@
 
 #pragma once
 
-#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -111,4 +111,3 @@ private:
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp
index 14da973d8..e918f4c7d 100644
--- a/src/theory/arith/error_set.cpp
+++ b/src/theory/arith/error_set.cpp
@@ -15,8 +15,9 @@
  ** \todo document this file
  **/
 
-
 #include "theory/arith/error_set.h"
+
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 
 using namespace std;
@@ -134,21 +135,21 @@ ErrorSet::Statistics::Statistics():
   d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0),
   d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0)
 {
-  StatisticsRegistry::registerStat(&d_enqueues);
-  StatisticsRegistry::registerStat(&d_enqueuesCollection);
-  StatisticsRegistry::registerStat(&d_enqueuesDiffMode);
-  StatisticsRegistry::registerStat(&d_enqueuesVarOrderMode);
-  StatisticsRegistry::registerStat(&d_enqueuesCollectionDuplicates);
-  StatisticsRegistry::registerStat(&d_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(){
-  StatisticsRegistry::unregisterStat(&d_enqueues);
-  StatisticsRegistry::unregisterStat(&d_enqueuesCollection);
-  StatisticsRegistry::unregisterStat(&d_enqueuesDiffMode);
-  StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderMode);
-  StatisticsRegistry::unregisterStat(&d_enqueuesCollectionDuplicates);
-  StatisticsRegistry::unregisterStat(&d_enqueuesVarOrderModeDuplicates);
+  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, TableauSizes tabSizes, BoundCountingLookup lookups):
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index f12e38c12..fb3117a98 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -22,7 +22,6 @@
 
 #include <vector>
 
-#include "expr/statistics_registry.h"
 #include "options/arith_heuristic_pivot_rule.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
@@ -31,6 +30,7 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau_sizes.h"
 #include "util/bin_heap.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 229dc379c..888e29732 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -17,9 +17,10 @@
 #include "theory/arith/fc_simplex.h"
 
 #include "base/output.h"
-#include "expr/statistics_registry.h"
 #include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 
@@ -52,37 +53,37 @@ FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
   d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"),
   d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots)
 {
-  StatisticsRegistry::registerStat(&d_initialSignalsTime);
-  StatisticsRegistry::registerStat(&d_initialConflicts);
+  smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
+  smtStatisticsRegistry()->registerStat(&d_initialConflicts);
 
-  StatisticsRegistry::registerStat(&d_fcFoundUnsat);
-  StatisticsRegistry::registerStat(&d_fcFoundSat);
-  StatisticsRegistry::registerStat(&d_fcMissed);
+  smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat);
+  smtStatisticsRegistry()->registerStat(&d_fcFoundSat);
+  smtStatisticsRegistry()->registerStat(&d_fcMissed);
 
-  StatisticsRegistry::registerStat(&d_fcTimer);
-  StatisticsRegistry::registerStat(&d_fcFocusConstructionTimer);
+  smtStatisticsRegistry()->registerStat(&d_fcTimer);
+  smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer);
 
-  StatisticsRegistry::registerStat(&d_selectUpdateForDualLike);
-  StatisticsRegistry::registerStat(&d_selectUpdateForPrimal);
+  smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike);
+  smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal);
 
-  StatisticsRegistry::registerStat(&d_finalCheckPivotCounter);
+  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
 }
 
 FCSimplexDecisionProcedure::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_initialSignalsTime);
-  StatisticsRegistry::unregisterStat(&d_initialConflicts);
+  smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
+  smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
 
-  StatisticsRegistry::unregisterStat(&d_fcFoundUnsat);
-  StatisticsRegistry::unregisterStat(&d_fcFoundSat);
-  StatisticsRegistry::unregisterStat(&d_fcMissed);
+  smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat);
+  smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat);
+  smtStatisticsRegistry()->unregisterStat(&d_fcMissed);
 
-  StatisticsRegistry::unregisterStat(&d_fcTimer);
-  StatisticsRegistry::unregisterStat(&d_fcFocusConstructionTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_fcTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer);
 
-  StatisticsRegistry::unregisterStat(&d_selectUpdateForDualLike);
-  StatisticsRegistry::unregisterStat(&d_selectUpdateForPrimal);
+  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike);
+  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal);
 
-  StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter);
+  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 471804003..c416af1c6 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -54,9 +54,9 @@
 
 #include <stdint.h>
 
-#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
 #include "util/dense_map.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -255,4 +255,3 @@ private:
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index d8888bd75..6d86a1ab1 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -13,11 +13,12 @@
  **
  ** This implements the LinearEqualityModule.
  **/
-
+#include "theory/arith/linear_equality.h"
 
 #include "base/output.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
-#include "theory/arith/linear_equality.h"
+
 
 using namespace std;
 
@@ -76,31 +77,31 @@ LinearEqualityModule::Statistics::Statistics():
   d_weakenTime("theory::arith::weakening::time"),
   d_forceTime("theory::arith::forcing::time")
 {
-  StatisticsRegistry::registerStat(&d_statPivots);
-  StatisticsRegistry::registerStat(&d_statUpdates);
+  smtStatisticsRegistry()->registerStat(&d_statPivots);
+  smtStatisticsRegistry()->registerStat(&d_statUpdates);
 
-  StatisticsRegistry::registerStat(&d_pivotTime);
-  StatisticsRegistry::registerStat(&d_adjTime);
+  smtStatisticsRegistry()->registerStat(&d_pivotTime);
+  smtStatisticsRegistry()->registerStat(&d_adjTime);
 
-  StatisticsRegistry::registerStat(&d_weakeningAttempts);
-  StatisticsRegistry::registerStat(&d_weakeningSuccesses);
-  StatisticsRegistry::registerStat(&d_weakenings);
-  StatisticsRegistry::registerStat(&d_weakenTime);
-  StatisticsRegistry::registerStat(&d_forceTime);
+  smtStatisticsRegistry()->registerStat(&d_weakeningAttempts);
+  smtStatisticsRegistry()->registerStat(&d_weakeningSuccesses);
+  smtStatisticsRegistry()->registerStat(&d_weakenings);
+  smtStatisticsRegistry()->registerStat(&d_weakenTime);
+  smtStatisticsRegistry()->registerStat(&d_forceTime);
 }
 
 LinearEqualityModule::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_statPivots);
-  StatisticsRegistry::unregisterStat(&d_statUpdates);
-  StatisticsRegistry::unregisterStat(&d_pivotTime);
-  StatisticsRegistry::unregisterStat(&d_adjTime);
+  smtStatisticsRegistry()->unregisterStat(&d_statPivots);
+  smtStatisticsRegistry()->unregisterStat(&d_statUpdates);
+  smtStatisticsRegistry()->unregisterStat(&d_pivotTime);
+  smtStatisticsRegistry()->unregisterStat(&d_adjTime);
 
 
-  StatisticsRegistry::unregisterStat(&d_weakeningAttempts);
-  StatisticsRegistry::unregisterStat(&d_weakeningSuccesses);
-  StatisticsRegistry::unregisterStat(&d_weakenings);
-  StatisticsRegistry::unregisterStat(&d_weakenTime);
-  StatisticsRegistry::unregisterStat(&d_forceTime);
+  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 d7c9c038c..f3cf17d81 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -29,7 +29,6 @@
 
 #pragma once
 
-#include "expr/statistics_registry.h"
 #include "options/arith_options.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
@@ -38,6 +37,7 @@
 #include "theory/arith/simplex_update.h"
 #include "theory/arith/tableau.h"
 #include "util/maybe.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 765e6a00d..df32ec8a4 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -19,10 +19,10 @@
 #include <algorithm>
 
 #include "base/output.h"
-#include "expr/statistics_registry.h"
 #include "options/arith_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
-
+#include "util/statistics_registry.h"
 
 using namespace std;
 
@@ -56,46 +56,46 @@ SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots):
   d_selectUpdateForSOI("theory::arith::SOI::selectSOI"),
   d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots)
 {
-  StatisticsRegistry::registerStat(&d_initialSignalsTime);
-  StatisticsRegistry::registerStat(&d_initialConflicts);
+  smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
+  smtStatisticsRegistry()->registerStat(&d_initialConflicts);
 
-  StatisticsRegistry::registerStat(&d_soiFoundUnsat);
-  StatisticsRegistry::registerStat(&d_soiFoundSat);
-  StatisticsRegistry::registerStat(&d_soiMissed);
+  smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat);
+  smtStatisticsRegistry()->registerStat(&d_soiFoundSat);
+  smtStatisticsRegistry()->registerStat(&d_soiMissed);
 
-  StatisticsRegistry::registerStat(&d_soiConflicts);
-  StatisticsRegistry::registerStat(&d_hasToBeMinimal);
-  StatisticsRegistry::registerStat(&d_maybeNotMinimal);
+  smtStatisticsRegistry()->registerStat(&d_soiConflicts);
+  smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal);
+  smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal);
 
-  StatisticsRegistry::registerStat(&d_soiTimer);
-  StatisticsRegistry::registerStat(&d_soiFocusConstructionTimer);
+  smtStatisticsRegistry()->registerStat(&d_soiTimer);
+  smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer);
 
-  StatisticsRegistry::registerStat(&d_soiConflictMinimization);
+  smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization);
 
-  StatisticsRegistry::registerStat(&d_selectUpdateForSOI);
+  smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI);
 
-  StatisticsRegistry::registerStat(&d_finalCheckPivotCounter);
+  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
 }
 
 SumOfInfeasibilitiesSPD::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_initialSignalsTime);
-  StatisticsRegistry::unregisterStat(&d_initialConflicts);
+  smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
+  smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
 
-  StatisticsRegistry::unregisterStat(&d_soiFoundUnsat);
-  StatisticsRegistry::unregisterStat(&d_soiFoundSat);
-  StatisticsRegistry::unregisterStat(&d_soiMissed);
+  smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat);
+  smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat);
+  smtStatisticsRegistry()->unregisterStat(&d_soiMissed);
 
-  StatisticsRegistry::unregisterStat(&d_soiConflicts);
-  StatisticsRegistry::unregisterStat(&d_hasToBeMinimal);
-  StatisticsRegistry::unregisterStat(&d_maybeNotMinimal);
+  smtStatisticsRegistry()->unregisterStat(&d_soiConflicts);
+  smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal);
+  smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal);
 
-  StatisticsRegistry::unregisterStat(&d_soiTimer);
-  StatisticsRegistry::unregisterStat(&d_soiFocusConstructionTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_soiTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer);
 
-  StatisticsRegistry::unregisterStat(&d_soiConflictMinimization);
+  smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization);
 
-  StatisticsRegistry::unregisterStat(&d_selectUpdateForSOI);
-  StatisticsRegistry::unregisterStat(&d_finalCheckPivotCounter);
+  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 b08d7794b..73a2330a3 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -54,9 +54,9 @@
 
 #include <stdint.h>
 
-#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
 #include "util/dense_map.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -241,4 +241,3 @@ private:
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3c5c1c414..843feed01 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/theory_arith.h"
 
 #include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/theory_arith_private.h"
 
@@ -33,9 +34,13 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
                          const LogicInfo& logicInfo, SmtGlobals* globals)
     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
     , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
-{}
+    , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
+{
+  smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
+}
 
 TheoryArith::~TheoryArith(){
+  smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer);
   delete d_internal;
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index d26a120ae..c54414109 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -43,7 +43,7 @@ private:
 
   TheoryArithPrivate* d_internal;
 
-  KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer");
+  TimerStat d_ppRewriteTimer;
 
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index bf1810331..e6b14d2b1 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -33,11 +33,11 @@
 #include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/statistics_registry.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"  // for incrementalSolving()
 #include "smt/logic_exception.h"
 #include "smt/logic_request.h"
+#include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/arith/approx_simplex.h"
 #include "theory/arith/arith_ite_utils.h"
@@ -70,6 +70,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -328,190 +329,190 @@ TheoryArithPrivate::Statistics::Statistics()
   , d_mipProofsSuccessful("theory::arith::z::mip::proofs::successful", 0)
   , d_numBranchesFailed("theory::arith::z::mip::branch::proof::failed", 0)
 {
-  StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
-  StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
-
-  StatisticsRegistry::registerStat(&d_statUserVariables);
-  StatisticsRegistry::registerStat(&d_statAuxiliaryVariables);
-  StatisticsRegistry::registerStat(&d_statDisequalitySplits);
-  StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
-  StatisticsRegistry::registerStat(&d_simplifyTimer);
-  StatisticsRegistry::registerStat(&d_staticLearningTimer);
-
-  StatisticsRegistry::registerStat(&d_presolveTime);
-  StatisticsRegistry::registerStat(&d_newPropTime);
-
-  StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
-
-  StatisticsRegistry::registerStat(&d_initialTableauSize);
-  StatisticsRegistry::registerStat(&d_currSetToSmaller);
-  StatisticsRegistry::registerStat(&d_smallerSetToCurr);
-  StatisticsRegistry::registerStat(&d_restartTimer);
-
-  StatisticsRegistry::registerStat(&d_boundComputationTime);
-  StatisticsRegistry::registerStat(&d_boundComputations);
-  StatisticsRegistry::registerStat(&d_boundPropagations);
-
-  StatisticsRegistry::registerStat(&d_unknownChecks);
-  StatisticsRegistry::registerStat(&d_maxUnknownsInARow);
-  StatisticsRegistry::registerStat(&d_avgUnknownsInARow);
-  StatisticsRegistry::registerStat(&d_revertsOnConflicts);
-  StatisticsRegistry::registerStat(&d_commitsOnConflicts);
-  StatisticsRegistry::registerStat(&d_nontrivialSatChecks);
-
-
-  StatisticsRegistry::registerStat(&d_satPivots);
-  StatisticsRegistry::registerStat(&d_unsatPivots);
-  StatisticsRegistry::registerStat(&d_unknownPivots);
-
-  StatisticsRegistry::registerStat(&d_replayLogRecCount);
-  StatisticsRegistry::registerStat(&d_replayLogRecConflictEscalation);
-  StatisticsRegistry::registerStat(&d_replayLogRecEarlyExit);
-  StatisticsRegistry::registerStat(&d_replayBranchCloseFailures);
-  StatisticsRegistry::registerStat(&d_replayLeafCloseFailures);
-  StatisticsRegistry::registerStat(&d_replayBranchSkips);
-  StatisticsRegistry::registerStat(&d_mirCutsAttempted);
-  StatisticsRegistry::registerStat(&d_gmiCutsAttempted);
-  StatisticsRegistry::registerStat(&d_branchCutsAttempted);
-  StatisticsRegistry::registerStat(&d_cutsReconstructed);
-  StatisticsRegistry::registerStat(&d_cutsProven);
-  StatisticsRegistry::registerStat(&d_cutsProofFailed);
-  StatisticsRegistry::registerStat(&d_cutsReconstructionFailed);
-  StatisticsRegistry::registerStat(&d_mipReplayLemmaCalls);
-  StatisticsRegistry::registerStat(&d_mipExternalCuts);
-  StatisticsRegistry::registerStat(&d_mipExternalBranch);
-
-  StatisticsRegistry::registerStat(&d_inSolveInteger);
-  StatisticsRegistry::registerStat(&d_branchesExhausted);
-  StatisticsRegistry::registerStat(&d_execExhausted);
-  StatisticsRegistry::registerStat(&d_pivotsExhausted);
-  StatisticsRegistry::registerStat(&d_panicBranches);
-  StatisticsRegistry::registerStat(&d_relaxCalls);
-  StatisticsRegistry::registerStat(&d_relaxLinFeas);
-  StatisticsRegistry::registerStat(&d_relaxLinFeasFailures);
-  StatisticsRegistry::registerStat(&d_relaxLinInfeas);
-  StatisticsRegistry::registerStat(&d_relaxLinInfeasFailures);
-  StatisticsRegistry::registerStat(&d_relaxLinExhausted);
-  StatisticsRegistry::registerStat(&d_relaxOthers);
-
-  StatisticsRegistry::registerStat(&d_applyRowsDeleted);
-
-  StatisticsRegistry::registerStat(&d_replaySimplexTimer);
-  StatisticsRegistry::registerStat(&d_replayLogTimer);
-  StatisticsRegistry::registerStat(&d_solveIntTimer);
-  StatisticsRegistry::registerStat(&d_solveRealRelaxTimer);
-
-  StatisticsRegistry::registerStat(&d_solveIntCalls);
-  StatisticsRegistry::registerStat(&d_solveStandardEffort);
-
-  StatisticsRegistry::registerStat(&d_approxDisabled);
-
-  StatisticsRegistry::registerStat(&d_replayAttemptFailed);
-
-  StatisticsRegistry::registerStat(&d_cutsRejectedDuringReplay);
-  StatisticsRegistry::registerStat(&d_cutsRejectedDuringLemmas);
-
-  StatisticsRegistry::registerStat(&d_solveIntModelsAttempts);
-  StatisticsRegistry::registerStat(&d_solveIntModelsSuccessful);
-  StatisticsRegistry::registerStat(&d_mipTimer);
-  StatisticsRegistry::registerStat(&d_lpTimer);
-  StatisticsRegistry::registerStat(&d_mipProofsAttempted);
-  StatisticsRegistry::registerStat(&d_mipProofsSuccessful);
-  StatisticsRegistry::registerStat(&d_numBranchesFailed);
+  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(){
-  StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
-  StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
-
-  StatisticsRegistry::unregisterStat(&d_statUserVariables);
-  StatisticsRegistry::unregisterStat(&d_statAuxiliaryVariables);
-  StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
-  StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
-  StatisticsRegistry::unregisterStat(&d_simplifyTimer);
-  StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
-
-  StatisticsRegistry::unregisterStat(&d_presolveTime);
-  StatisticsRegistry::unregisterStat(&d_newPropTime);
-
-  StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
-
-  StatisticsRegistry::unregisterStat(&d_initialTableauSize);
-  StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
-  StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
-  StatisticsRegistry::unregisterStat(&d_restartTimer);
-
-  StatisticsRegistry::unregisterStat(&d_boundComputationTime);
-  StatisticsRegistry::unregisterStat(&d_boundComputations);
-  StatisticsRegistry::unregisterStat(&d_boundPropagations);
-
-  StatisticsRegistry::unregisterStat(&d_unknownChecks);
-  StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow);
-  StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow);
-  StatisticsRegistry::unregisterStat(&d_revertsOnConflicts);
-  StatisticsRegistry::unregisterStat(&d_commitsOnConflicts);
-  StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks);
-
-  StatisticsRegistry::unregisterStat(&d_satPivots);
-  StatisticsRegistry::unregisterStat(&d_unsatPivots);
-  StatisticsRegistry::unregisterStat(&d_unknownPivots);
-
-  StatisticsRegistry::unregisterStat(&d_replayLogRecCount);
-  StatisticsRegistry::unregisterStat(&d_replayLogRecConflictEscalation);
-  StatisticsRegistry::unregisterStat(&d_replayLogRecEarlyExit);
-  StatisticsRegistry::unregisterStat(&d_replayBranchCloseFailures);
-  StatisticsRegistry::unregisterStat(&d_replayLeafCloseFailures);
-  StatisticsRegistry::unregisterStat(&d_replayBranchSkips);
-  StatisticsRegistry::unregisterStat(&d_mirCutsAttempted);
-  StatisticsRegistry::unregisterStat(&d_gmiCutsAttempted);
-  StatisticsRegistry::unregisterStat(&d_branchCutsAttempted);
-  StatisticsRegistry::unregisterStat(&d_cutsReconstructed);
-  StatisticsRegistry::unregisterStat(&d_cutsProven);
-  StatisticsRegistry::unregisterStat(&d_cutsProofFailed);
-  StatisticsRegistry::unregisterStat(&d_cutsReconstructionFailed);
-  StatisticsRegistry::unregisterStat(&d_mipReplayLemmaCalls);
-  StatisticsRegistry::unregisterStat(&d_mipExternalCuts);
-  StatisticsRegistry::unregisterStat(&d_mipExternalBranch);
-
-
-  StatisticsRegistry::unregisterStat(&d_inSolveInteger);
-  StatisticsRegistry::unregisterStat(&d_branchesExhausted);
-  StatisticsRegistry::unregisterStat(&d_execExhausted);
-  StatisticsRegistry::unregisterStat(&d_pivotsExhausted);
-  StatisticsRegistry::unregisterStat(&d_panicBranches);
-  StatisticsRegistry::unregisterStat(&d_relaxCalls);
-  StatisticsRegistry::unregisterStat(&d_relaxLinFeas);
-  StatisticsRegistry::unregisterStat(&d_relaxLinFeasFailures);
-  StatisticsRegistry::unregisterStat(&d_relaxLinInfeas);
-  StatisticsRegistry::unregisterStat(&d_relaxLinInfeasFailures);
-  StatisticsRegistry::unregisterStat(&d_relaxLinExhausted);
-  StatisticsRegistry::unregisterStat(&d_relaxOthers);
-
-  StatisticsRegistry::unregisterStat(&d_applyRowsDeleted);
-
-  StatisticsRegistry::unregisterStat(&d_replaySimplexTimer);
-  StatisticsRegistry::unregisterStat(&d_replayLogTimer);
-  StatisticsRegistry::unregisterStat(&d_solveIntTimer);
-  StatisticsRegistry::unregisterStat(&d_solveRealRelaxTimer);
-
-  StatisticsRegistry::unregisterStat(&d_solveIntCalls);
-  StatisticsRegistry::unregisterStat(&d_solveStandardEffort);
-
-  StatisticsRegistry::unregisterStat(&d_approxDisabled);
-
-  StatisticsRegistry::unregisterStat(&d_replayAttemptFailed);
-
-  StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringReplay);
-  StatisticsRegistry::unregisterStat(&d_cutsRejectedDuringLemmas);
-
-
-  StatisticsRegistry::unregisterStat(&d_solveIntModelsAttempts);
-  StatisticsRegistry::unregisterStat(&d_solveIntModelsSuccessful);
-  StatisticsRegistry::unregisterStat(&d_mipTimer);
-  StatisticsRegistry::unregisterStat(&d_lpTimer);
-  StatisticsRegistry::unregisterStat(&d_mipProofsAttempted);
-  StatisticsRegistry::unregisterStat(&d_mipProofsSuccessful);
-  StatisticsRegistry::unregisterStat(&d_numBranchesFailed);
+  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){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 32c12eba7..1009dceb8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -31,7 +31,6 @@
 #include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/statistics_registry.h"
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
 #include "smt_util/boolean_simplification.h"
@@ -67,6 +66,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {