1 files changed, 9 insertions, 16 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b45ccbac3..25f87de2c 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1748,23 +1748,16 @@ void CardinalityExtension::checkCombinedCardinality()
 }
 
 CardinalityExtension::Statistics::Statistics()
-    : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
-      d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
-      d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
-      d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
+    : d_clique_conflicts(smtStatisticsRegistry().registerInt(
+        "CardinalityExtension::Clique_Conflicts")),
+      d_clique_lemmas(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Clique_Lemmas")),
+      d_split_lemmas(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Split_Lemmas")),
+      d_max_model_size(smtStatisticsRegistry().registerInt(
+          "CardinalityExtension::Max_Model_Size"))
 {
-  smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
-  smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_split_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_max_model_size);
-}
-
-CardinalityExtension::Statistics::~Statistics()
-{
-  smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
-  smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
+  d_max_model_size.maxAssign(1);
 }
 
 }  // namespace uf