From c6ea00f789ef354e93c67740016709d4105fc3be Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 29 Jun 2021 10:34:42 -0700
Subject: [PATCH] Fix statistics in AigBitblaster. (#6810)

Fixes #6788
---
 src/theory/bv/bitblast/aig_bitblaster.cpp | 28 ++++++++---------------
 src/theory/bv/bitblast/aig_bitblaster.h   |  1 -
 2 files changed, 10 insertions(+), 19 deletions(-)

diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 0907e8005..8fece032c 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -473,25 +473,17 @@ Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
 }
 
 AigBitblaster::Statistics::Statistics()
-  : d_numClauses("theory::bv::AigBitblaster::numClauses", 0)
-  , d_numVariables("theory::bv::AigBitblaster::numVariables", 0)
-  , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime")
-  , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
-  , d_solveTime("theory::bv::AigBitblaster::solveTime")
+    : d_numClauses(smtStatisticsRegistry().registerInt(
+        "theory::bv::AigBitblaster::numClauses")),
+      d_numVariables(smtStatisticsRegistry().registerInt(
+          "theory::bv::AigBitblaster::numVariables")),
+      d_simplificationTime(smtStatisticsRegistry().registerTimer(
+          "theory::bv::AigBitblaster::simplificationTime")),
+      d_cnfConversionTime(smtStatisticsRegistry().registerTimer(
+          "theory::bv::AigBitblaster::cnfConversionTime")),
+      d_solveTime(smtStatisticsRegistry().registerTimer(
+          "theory::bv::AigBitblaster::solveTime"))
 {
-  smtStatisticsRegistry()->registerStat(&d_numClauses); 
-  smtStatisticsRegistry()->registerStat(&d_numVariables);
-  smtStatisticsRegistry()->registerStat(&d_simplificationTime); 
-  smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
-  smtStatisticsRegistry()->registerStat(&d_solveTime); 
-}
-
-AigBitblaster::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_numClauses); 
-  smtStatisticsRegistry()->unregisterStat(&d_numVariables);
-  smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); 
-  smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
-  smtStatisticsRegistry()->unregisterStat(&d_solveTime); 
 }
 
 }  // namespace bv
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 39ecbc12c..bf184585f 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -99,7 +99,6 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
     TimerStat d_cnfConversionTime;
     TimerStat d_solveTime;
     Statistics();
-    ~Statistics();
   };
 
   Statistics d_statistics;
-- 
2.30.2