20 files changed, 134 insertions, 122 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index f05520306..842ff60b1 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -16,6 +16,7 @@
 
 #include "options/bv_options.h"
 #include "smt_util/dump.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
@@ -1047,13 +1048,13 @@ AbstractionModule::Statistics::Statistics()
   , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0)
   , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime")
 {
-  StatisticsRegistry::registerStat(&d_numFunctionsAbstracted);
-  StatisticsRegistry::registerStat(&d_numArgsSkolemized);
-  StatisticsRegistry::registerStat(&d_abstractionTime);
+  smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
+  smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
+  smtStatisticsRegistry()->registerStat(&d_abstractionTime);
 }
 
 AbstractionModule::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numFunctionsAbstracted);
-  StatisticsRegistry::unregisterStat(&d_numArgsSkolemized);
-  StatisticsRegistry::unregisterStat(&d_abstractionTime);
+  smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted);
+  smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized);
+  smtStatisticsRegistry()->unregisterStat(&d_abstractionTime);
 }
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 6b4d5a7dc..cba170d76 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -23,8 +23,8 @@
 #include <ext/hash_set>
 
 #include "expr/node.h"
-#include "expr/statistics_registry.h"
 #include "theory/substitutions.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index f07bd49f7..d84493daf 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -455,19 +455,19 @@ AigBitblaster::Statistics::Statistics()
   , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
   , d_solveTime("theory::bv::AigBitblaster::solveTime")
 {
-  StatisticsRegistry::registerStat(&d_numClauses); 
-  StatisticsRegistry::registerStat(&d_numVariables);
-  StatisticsRegistry::registerStat(&d_simplificationTime); 
-  StatisticsRegistry::registerStat(&d_cnfConversionTime);
-  StatisticsRegistry::registerStat(&d_solveTime); 
+  smtStatisticsRegistry()->registerStat(&d_numClauses); 
+  smtStatisticsRegistry()->registerStat(&d_numVariables);
+  smtStatisticsRegistry()->registerStat(&d_simplificationTime); 
+  smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+  smtStatisticsRegistry()->registerStat(&d_solveTime); 
 }
 
 AigBitblaster::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numClauses); 
-  StatisticsRegistry::unregisterStat(&d_numVariables);
-  StatisticsRegistry::unregisterStat(&d_simplificationTime); 
-  StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
-  StatisticsRegistry::unregisterStat(&d_solveTime); 
+  smtStatisticsRegistry()->unregisterStat(&d_numClauses); 
+  smtStatisticsRegistry()->unregisterStat(&d_numVariables);
+  smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); 
+  smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+  smtStatisticsRegistry()->unregisterStat(&d_solveTime); 
 }
 
 #else // CVC4_USE_ABC
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 6231b8e46..40ac3d560 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -15,9 +15,10 @@
  **/
 
 #include "theory/bv/bv_quick_check.h"
-#include "theory/bv/theory_bv_utils.h"
 
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/bitblaster_template.h"
+#include "theory/bv/theory_bv_utils.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -357,22 +358,21 @@ QuickXPlain::Statistics::Statistics(const std::string& name)
   , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0)
   , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio")
 {
-  StatisticsRegistry::registerStat(&d_xplainTime);
-  StatisticsRegistry::registerStat(&d_numSolved);
-  StatisticsRegistry::registerStat(&d_numUnknown);
-  StatisticsRegistry::registerStat(&d_numUnknownWasUnsat);
-  StatisticsRegistry::registerStat(&d_numConflictsMinimized);
-  StatisticsRegistry::registerStat(&d_finalPeriod);
-  StatisticsRegistry::registerStat(&d_avgMinimizationRatio);  
+  smtStatisticsRegistry()->registerStat(&d_xplainTime);
+  smtStatisticsRegistry()->registerStat(&d_numSolved);
+  smtStatisticsRegistry()->registerStat(&d_numUnknown);
+  smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat);
+  smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized);
+  smtStatisticsRegistry()->registerStat(&d_finalPeriod);
+  smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio);
 }
 
 QuickXPlain::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_xplainTime);
-  StatisticsRegistry::unregisterStat(&d_numSolved);
-  StatisticsRegistry::unregisterStat(&d_numUnknown);
-  StatisticsRegistry::unregisterStat(&d_numUnknownWasUnsat);
-  StatisticsRegistry::unregisterStat(&d_numConflictsMinimized);
-  StatisticsRegistry::unregisterStat(&d_finalPeriod);
-  StatisticsRegistry::unregisterStat(&d_avgMinimizationRatio);  
+  smtStatisticsRegistry()->unregisterStat(&d_xplainTime);
+  smtStatisticsRegistry()->unregisterStat(&d_numSolved);
+  smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
+  smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat);
+  smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized);
+  smtStatisticsRegistry()->unregisterStat(&d_finalPeriod);
+  smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio);  
 }
-
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 8ef49f786..8d2a62287 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -24,9 +24,9 @@
 
 #include "context/cdo.h"
 #include "expr/node.h"
-#include "expr/statistics_registry.h"
 #include "prop/sat_solver_types.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 4531be040..fc9d67cb4 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -13,11 +13,12 @@
  **
  ** Algebraic solver.
  **/
+#include "theory/bv/bv_subtheory_algebraic.h"
 
 #include "options/bv_options.h"
 #include "smt_util/boolean_simplification.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_quick_check.h"
-#include "theory/bv/bv_subtheory_algebraic.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
@@ -734,25 +735,25 @@ AlgebraicSolver::Statistics::Statistics()
   , d_solveTime("theory::bv::AlgebraicSolver::SolveTime")
   , d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2)
 {
-  StatisticsRegistry::registerStat(&d_numCallstoCheck);
-  StatisticsRegistry::registerStat(&d_numSimplifiesToTrue);
-  StatisticsRegistry::registerStat(&d_numSimplifiesToFalse);
-  StatisticsRegistry::registerStat(&d_numUnsat);
-  StatisticsRegistry::registerStat(&d_numSat);
-  StatisticsRegistry::registerStat(&d_numUnknown);
-  StatisticsRegistry::registerStat(&d_solveTime);
-  StatisticsRegistry::registerStat(&d_useHeuristic);
+  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
+  smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse);
+  smtStatisticsRegistry()->registerStat(&d_numUnsat);
+  smtStatisticsRegistry()->registerStat(&d_numSat);
+  smtStatisticsRegistry()->registerStat(&d_numUnknown);
+  smtStatisticsRegistry()->registerStat(&d_solveTime);
+  smtStatisticsRegistry()->registerStat(&d_useHeuristic);
 }
 
 AlgebraicSolver::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
-  StatisticsRegistry::unregisterStat(&d_numSimplifiesToTrue);
-  StatisticsRegistry::unregisterStat(&d_numSimplifiesToFalse);
-  StatisticsRegistry::unregisterStat(&d_numUnsat);
-  StatisticsRegistry::unregisterStat(&d_numSat);
-  StatisticsRegistry::unregisterStat(&d_numUnknown);
-  StatisticsRegistry::unregisterStat(&d_solveTime);
-  StatisticsRegistry::unregisterStat(&d_useHeuristic);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue);
+  smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse);
+  smtStatisticsRegistry()->unregisterStat(&d_numUnsat);
+  smtStatisticsRegistry()->unregisterStat(&d_numSat);
+  smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
+  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
+  smtStatisticsRegistry()->unregisterStat(&d_useHeuristic);
 }
 
 bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) {
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 1d0342c08..9f8cb580c 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -17,6 +17,7 @@
 #include "decision/decision_attributes.h"
 #include "options/decision_options.h"
 #include "options/bv_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/bv_quick_check.h"
@@ -55,12 +56,12 @@ BitblastSolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
   , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
 {
-  StatisticsRegistry::registerStat(&d_numCallstoCheck);
-  StatisticsRegistry::registerStat(&d_numBBLemmas);
+  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
 }
 BitblastSolver::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
-  StatisticsRegistry::unregisterStat(&d_numBBLemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas);
 }
 
 void BitblastSolver::setAbstraction(AbstractionModule* abs) {
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index ef4d24e82..ec257468e 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -18,6 +18,7 @@
 
 #include "options/bv_options.h"
 #include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/slicer.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -438,10 +439,10 @@ CoreSolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
   , d_slicerEnabled("theory::bv::CoreSolver::SlicerEnabled", false)
 {
-  StatisticsRegistry::registerStat(&d_numCallstoCheck);
-  StatisticsRegistry::registerStat(&d_slicerEnabled);
+  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->registerStat(&d_slicerEnabled);
 }
 CoreSolver::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
-  StatisticsRegistry::unregisterStat(&d_slicerEnabled);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->unregisterStat(&d_slicerEnabled);
 }
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 054e43b7c..7916d941e 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -17,6 +17,7 @@
 #include "theory/bv/bv_subtheory_inequality.h"
 
 #include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
@@ -228,8 +229,8 @@ bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact)
 InequalitySolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
 {
-  StatisticsRegistry::registerStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
 }
 InequalitySolver::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
 }
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 00e6f9ff8..66ad4fec0 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -11,11 +11,12 @@
  **
  ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
  **
- ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. 
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
  **/
 #include "theory/bv/bv_to_bool.h"
 
 #include "smt_util/node_visitor.h"
+#include "smt/smt_statistics_registry.h"
 
 using namespace std;
 using namespace CVC4;
@@ -31,7 +32,7 @@ BvToBoolPreprocessor::BvToBoolPreprocessor()
 {}
 
 void BvToBoolPreprocessor::addToLiftCache(TNode term, Node new_term) {
-  Assert (new_term != Node()); 
+  Assert (new_term != Node());
   Assert (!hasLiftCache(term));
   Assert (term.getType() == new_term.getType());
   d_liftCache[term] = new_term; 
@@ -239,13 +240,13 @@ BvToBoolPreprocessor::Statistics::Statistics()
   , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0)
   , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0)
 {
-  StatisticsRegistry::registerStat(&d_numTermsLifted);
-  StatisticsRegistry::registerStat(&d_numAtomsLifted);
-  StatisticsRegistry::registerStat(&d_numTermsForcedLifted);
+  smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
+  smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
+  smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
 }
 
 BvToBoolPreprocessor::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numTermsLifted);
-  StatisticsRegistry::unregisterStat(&d_numAtomsLifted);
-  StatisticsRegistry::unregisterStat(&d_numTermsForcedLifted);
+  smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
+  smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
+  smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
 }
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 46b2d5c6e..e6c126440 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -11,7 +11,7 @@
  **
  ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
  **
- ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. 
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
  **/
 
 #include "cvc4_private.h"
@@ -19,14 +19,14 @@
 #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
 #define __CVC4__THEORY__BV__BV_TO_BOOL_H
 
-#include "expr/statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; 
+typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
 
 class BvToBoolPreprocessor {
 
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 39606ca7c..000abe62b 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -19,6 +19,7 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
@@ -45,7 +46,8 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
 
-  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
+  d_satSolver = prop::SatSolverFactory::createMinisat(
+      d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
                                            d_nullContext, d_bv->globals());
 
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index b8173cb8b..34a9418dd 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -20,6 +20,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/rewriter.h"
@@ -46,7 +47,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
   , d_name(name)
   , d_statistics(name) {
 
-  d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
+  d_satSolver = prop::SatSolverFactory::createMinisat(
+      c, smtStatisticsRegistry(), name);
   d_nullRegistrar = new prop::NullRegistrar();
   d_nullContext = new context::Context();
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
@@ -307,24 +309,24 @@ TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
   d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
   d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
 {
-  StatisticsRegistry::registerStat(&d_numTermClauses);
-  StatisticsRegistry::registerStat(&d_numAtomClauses);
-  StatisticsRegistry::registerStat(&d_numTerms);
-  StatisticsRegistry::registerStat(&d_numAtoms);
-  StatisticsRegistry::registerStat(&d_numExplainedPropagations);
-  StatisticsRegistry::registerStat(&d_numBitblastingPropagations);
-  StatisticsRegistry::registerStat(&d_bitblastTimer);
+  smtStatisticsRegistry()->registerStat(&d_numTermClauses);
+  smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
+  smtStatisticsRegistry()->registerStat(&d_numTerms);
+  smtStatisticsRegistry()->registerStat(&d_numAtoms);
+  smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations);
+  smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations);
+  smtStatisticsRegistry()->registerStat(&d_bitblastTimer);
 }
 
 
 TLazyBitblaster::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numTermClauses);
-  StatisticsRegistry::unregisterStat(&d_numAtomClauses);
-  StatisticsRegistry::unregisterStat(&d_numTerms);
-  StatisticsRegistry::unregisterStat(&d_numAtoms);
-  StatisticsRegistry::unregisterStat(&d_numExplainedPropagations);
-  StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations);
-  StatisticsRegistry::unregisterStat(&d_bitblastTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_numTermClauses);
+  smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses);
+  smtStatisticsRegistry()->unregisterStat(&d_numTerms);
+  smtStatisticsRegistry()->unregisterStat(&d_numAtoms);
+  smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations);
+  smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations);
+  smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer);
 }
 
 bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
@@ -496,7 +498,8 @@ void TLazyBitblaster::clearSolver() {
 
   invalidateModelCache();
   // recreate sat solver
-  d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
+  d_satSolver = prop::SatSolverFactory::createMinisat(
+      d_ctx, smtStatisticsRegistry());
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
                                            d_nullContext, d_bv->globals());
 
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index d31ff50d1..0e6815f47 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -13,9 +13,10 @@
  **
  ** Bitvector theory.
  **/
+#include "theory/bv/slicer.h"
 
 #include "options/bv_options.h"
-#include "theory/bv/slicer.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
@@ -598,17 +599,17 @@ UnionFind::Statistics::Statistics():
   d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
   d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
 {
-  StatisticsRegistry::registerStat(&d_numRepresentatives);
-  StatisticsRegistry::registerStat(&d_numSplits);
-  StatisticsRegistry::registerStat(&d_numMerges);
-  StatisticsRegistry::registerStat(&d_avgFindDepth);
-  StatisticsRegistry::registerStat(&d_numAddedEqualities);
+  smtStatisticsRegistry()->registerStat(&d_numRepresentatives);
+  smtStatisticsRegistry()->registerStat(&d_numSplits);
+  smtStatisticsRegistry()->registerStat(&d_numMerges);
+  smtStatisticsRegistry()->registerStat(&d_avgFindDepth);
+  smtStatisticsRegistry()->registerStat(&d_numAddedEqualities);
 }
 
 UnionFind::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_numRepresentatives);
-  StatisticsRegistry::unregisterStat(&d_numSplits);
-  StatisticsRegistry::unregisterStat(&d_numMerges);
-  StatisticsRegistry::unregisterStat(&d_avgFindDepth);
-  StatisticsRegistry::unregisterStat(&d_numAddedEqualities);
+  smtStatisticsRegistry()->unregisterStat(&d_numRepresentatives);
+  smtStatisticsRegistry()->unregisterStat(&d_numSplits);
+  smtStatisticsRegistry()->unregisterStat(&d_numMerges);
+  smtStatisticsRegistry()->unregisterStat(&d_avgFindDepth);
+  smtStatisticsRegistry()->unregisterStat(&d_numAddedEqualities);
 }
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 5ecc2a788..68642784f 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -23,11 +23,10 @@
 #include <ext/hash_map>
 
 #include "expr/node.h"
-#include "expr/statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/bitvector.h"
 #include "util/index.h"
-
+#include "util/statistics_registry.h"
 
 #ifndef __CVC4__THEORY__BV__SLICER_BV_H
 #define __CVC4__THEORY__BV__SLICER_BV_H
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 0505035c7..4acd1b847 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -17,6 +17,7 @@
 
 #include "options/bv_options.h"
 #include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bv_eager_solver.h"
 #include "theory/bv/bv_subtheory_algebraic.h"
@@ -123,23 +124,23 @@ TheoryBV::Statistics::Statistics():
   d_weightComputationTimer("theory::bv::weightComputationTimer"),
   d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 {
-  StatisticsRegistry::registerStat(&d_avgConflictSize);
-  StatisticsRegistry::registerStat(&d_solveSubstitutions);
-  StatisticsRegistry::registerStat(&d_solveTimer);
-  StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort);
-  StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort);
-  StatisticsRegistry::registerStat(&d_weightComputationTimer);
-  StatisticsRegistry::registerStat(&d_numMultSlice);
+  smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
+  smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
+  smtStatisticsRegistry()->registerStat(&d_solveTimer);
+  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
+  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
+  smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
+  smtStatisticsRegistry()->registerStat(&d_numMultSlice);
 }
 
 TheoryBV::Statistics::~Statistics() {
-  StatisticsRegistry::unregisterStat(&d_avgConflictSize);
-  StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
-  StatisticsRegistry::unregisterStat(&d_solveTimer);
-  StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort);
-  StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort);
-  StatisticsRegistry::unregisterStat(&d_weightComputationTimer);
-  StatisticsRegistry::unregisterStat(&d_numMultSlice);
+  smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
+  smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
+  smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
+  smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
 }
 
 Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 8ded63c28..e7e4d464f 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -22,12 +22,12 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
-#include "expr/statistics_registry.h"
 #include "smt/smt_globals.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
 #include "util/hash.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index f5e2a2077..af080a970 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -22,10 +22,10 @@
 #include <sstream>
 
 #include "context/context.h"
-#include "expr/statistics_registry.h"
 #include "smt_util/command.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -328,7 +328,7 @@ class RewriteRule {
   //   /** Constructor */
   //   RuleStatistics()
   //   : d_ruleApplications(getStatName("theory::bv::RewriteRules::count"), 0) {
-  //     StatisticsRegistry::registerStat(&d_ruleApplications);
+  //     currentStatisticsRegistry()->registerStat(&d_ruleApplications);
   //   }
 
   //   /** Destructor */
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 2c82943ce..6e2fdf58e 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -36,14 +36,14 @@ RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND];
 void TheoryBVRewriter::init() {
    // s_allRules = new AllRewriteRules;
    // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer");
-   // StatisticsRegistry::registerStat(d_rewriteTimer); 
+   // smtStatisticsRegistry()->registerStat(d_rewriteTimer); 
    initializeRewrites();
 
 }
 
 void TheoryBVRewriter::shutdown() {
    // delete s_allRules;
-   // StatisticsRegistry::unregisterStat(d_rewriteTimer); 
+   // smtStatisticsRegistry()->unregisterStat(d_rewriteTimer); 
    //delete d_rewriteTimer;
 }
 
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 7e5d429fd..3f0fa8194 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -20,8 +20,8 @@
 #ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 #define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
-#include "expr/statistics_registry.h"
 #include "theory/rewriter.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {