More minor improvements to synth-rr (#1597)

1 files changed, 11 insertions, 4 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 38cfb9ba7..fbafb8b8c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -357,20 +357,27 @@ void CegInstantiation::preregisterAssertion( Node n ) {
   }
 }
 
-CegInstantiation::Statistics::Statistics():
-  d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
-  d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
-  d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0)
+CegInstantiation::Statistics::Statistics()
+    : d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
+      d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
+      d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0),
+      d_solutions("CegConjecture::solutions", 0),
+      d_candidate_rewrites("CegConjecture::candidate_rewrites", 0)
+
 {
   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_candidate_rewrites);
 }
 
 CegInstantiation::Statistics::~Statistics(){
   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_candidate_rewrites);
 }
 
 }/* namespace CVC4::theory::quantifiers */