1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 81fe00674..cc0b18ffe 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
@@ -696,15 +697,15 @@ CegInstantiation::Statistics::Statistics():
   d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
   d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0)
 {
-  StatisticsRegistry::registerStat(&d_cegqi_lemmas_ce);
-  StatisticsRegistry::registerStat(&d_cegqi_lemmas_refine);
-  StatisticsRegistry::registerStat(&d_cegqi_si_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
+  smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
+  smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
 }
 
 CegInstantiation::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_ce);
-  StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_refine);
-  StatisticsRegistry::unregisterStat(&d_cegqi_si_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce);
+  smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
+  smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
 }