1 files changed, 18 insertions, 32 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp
index 4fe0e9bbc..19d799eb3 100644
--- a/src/theory/quantifiers/sygus/sygus_stats.cpp
+++ b/src/theory/quantifiers/sygus/sygus_stats.cpp
@@ -22,40 +22,26 @@ namespace theory {
 namespace quantifiers {
 
 SygusStatistics::SygusStatistics()
-    : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0),
-      d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0),
-      d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0),
-      d_solutions("SynthConjecture::solutions", 0),
-      d_filtered_solutions("SynthConjecture::filtered_solutions", 0),
-      d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print",
-                                 0),
-      d_enumTermsRewrite("SygusEnumerator::enumTermsRewrite", 0),
-      d_enumTermsExampleEval("SygusEnumerator::enumTermsEvalExamples", 0),
-      d_enumTerms("SygusEnumerator::enumTerms", 0)
+    : d_cegqi_lemmas_ce(
+        smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_ce")),
+      d_cegqi_lemmas_refine(smtStatisticsRegistry().registerInt(
+          "SynthEngine::cegqi_lemmas_refine")),
+      d_cegqi_si_lemmas(
+          smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_si")),
+      d_solutions(
+          smtStatisticsRegistry().registerInt("SynthConjecture::solutions")),
+      d_filtered_solutions(smtStatisticsRegistry().registerInt(
+          "SynthConjecture::filtered_solutions")),
+      d_candidate_rewrites_print(smtStatisticsRegistry().registerInt(
+          "SynthConjecture::candidate_rewrites_print")),
+      d_enumTermsRewrite(smtStatisticsRegistry().registerInt(
+          "SygusEnumerator::enumTermsRewrite")),
+      d_enumTermsExampleEval(smtStatisticsRegistry().registerInt(
+          "SygusEnumerator::enumTermsEvalExamples")),
+      d_enumTerms(
+          smtStatisticsRegistry().registerInt("SygusEnumerator::enumTerms"))
 
 {
-  smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
-  smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
-  smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_solutions);
-  smtStatisticsRegistry()->registerStat(&d_filtered_solutions);
-  smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print);
-  smtStatisticsRegistry()->registerStat(&d_enumTermsRewrite);
-  smtStatisticsRegistry()->registerStat(&d_enumTermsExampleEval);
-  smtStatisticsRegistry()->registerStat(&d_enumTerms);
-}
-
-SygusStatistics::~SygusStatistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce);
-  smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
-  smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_solutions);
-  smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions);
-  smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print);
-  smtStatisticsRegistry()->unregisterStat(&d_enumTermsRewrite);
-  smtStatisticsRegistry()->unregisterStat(&d_enumTermsExampleEval);
-  smtStatisticsRegistry()->unregisterStat(&d_enumTerms);
 }
 
 }  // namespace quantifiers