1 files changed, 5 insertions, 12 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 2332fa9fd..42e4cb7b0 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -40,9 +40,10 @@ JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de,
       d_exploredThreshold(c),
       d_prvsIndex(c, 0),
       d_threshPrvsIndex(c, 0),
-      d_helpfulness("decision::jh::helpfulness", 0),
-      d_giveup("decision::jh::giveup", 0),
-      d_timestat("decision::jh::time"),
+      d_helpfulness(
+          smtStatisticsRegistry().registerInt("decision::jh::helpfulness")),
+      d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")),
+      d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")),
       d_assertions(uc),
       d_skolemAssertions(uc),
       d_skolemCache(uc),
@@ -54,18 +55,10 @@ JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de,
       d_weightCache(uc),
       d_startIndexCache(c)
 {
-  smtStatisticsRegistry()->registerStat(&d_helpfulness);
-  smtStatisticsRegistry()->registerStat(&d_giveup);
-  smtStatisticsRegistry()->registerStat(&d_timestat);
   Trace("decision") << "Justification heuristic enabled" << std::endl;
 }
 
-JustificationHeuristic::~JustificationHeuristic()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_helpfulness);
-  smtStatisticsRegistry()->unregisterStat(&d_giveup);
-  smtStatisticsRegistry()->unregisterStat(&d_timestat);
-}
+JustificationHeuristic::~JustificationHeuristic() {}
 
 cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch)
 {