1 files changed, 18 insertions, 37 deletions

diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 6dfce4254..833fa59b9 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -307,16 +307,10 @@ void ITECompressor::reset()
 void ITECompressor::garbageCollect() { reset(); }
 
 ITECompressor::Statistics::Statistics()
-    : d_compressCalls("ite-simp::compressCalls", 0),
-      d_skolemsAdded("ite-simp::skolems", 0)
+    : d_compressCalls(
+        smtStatisticsRegistry().registerInt("ite-simp::compressCalls")),
+      d_skolemsAdded(smtStatisticsRegistry().registerInt("ite-simp::skolems"))
 {
-  smtStatisticsRegistry()->registerStat(&d_compressCalls);
-  smtStatisticsRegistry()->registerStat(&d_skolemsAdded);
-}
-ITECompressor::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_compressCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded);
 }
 
 Node ITECompressor::push_back_boolean(Node original, Node compressed)
@@ -704,35 +698,22 @@ bool ITESimplifier::doneALotOfWorkHeuristic() const
 }
 
 ITESimplifier::Statistics::Statistics()
-    : d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
-      d_unexpected("ite-simp::unexpected", 0),
-      d_unsimplified("ite-simp::unsimplified", 0),
-      d_exactMatchFold("ite-simp::exactMatchFold", 0),
-      d_binaryPredFold("ite-simp::binaryPredFold", 0),
-      d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
-      d_simpITEVisits("ite-simp::simpITE.visits", 0),
-      d_inSmaller("ite-simp::inSmaller")
-{
-  smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded);
-  smtStatisticsRegistry()->registerStat(&d_unexpected);
-  smtStatisticsRegistry()->registerStat(&d_unsimplified);
-  smtStatisticsRegistry()->registerStat(&d_exactMatchFold);
-  smtStatisticsRegistry()->registerStat(&d_binaryPredFold);
-  smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds);
-  smtStatisticsRegistry()->registerStat(&d_simpITEVisits);
-  smtStatisticsRegistry()->registerStat(&d_inSmaller);
-}
-
-ITESimplifier::Statistics::~Statistics()
+    : d_maxNonConstantsFolded(
+        smtStatisticsRegistry().registerInt("ite-simp::maxNonConstantsFolded")),
+      d_unexpected(smtStatisticsRegistry().registerInt("ite-simp::unexpected")),
+      d_unsimplified(
+          smtStatisticsRegistry().registerInt("ite-simp::unsimplified")),
+      d_exactMatchFold(
+          smtStatisticsRegistry().registerInt("ite-simp::exactMatchFold")),
+      d_binaryPredFold(
+          smtStatisticsRegistry().registerInt("ite-simp::binaryPredFold")),
+      d_specialEqualityFolds(smtStatisticsRegistry().registerInt(
+          "ite-simp::specialEqualityFolds")),
+      d_simpITEVisits(
+          smtStatisticsRegistry().registerInt("ite-simp::simpITE.visits")),
+      d_inSmaller(smtStatisticsRegistry().registerHistogram<uint32_t>(
+          "ite-simp::inSmaller"))
 {
-  smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded);
-  smtStatisticsRegistry()->unregisterStat(&d_unexpected);
-  smtStatisticsRegistry()->unregisterStat(&d_unsimplified);
-  smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold);
-  smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold);
-  smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds);
-  smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits);
-  smtStatisticsRegistry()->unregisterStat(&d_inSmaller);
 }
 
 bool ITESimplifier::isConstantIte(TNode e)