fix statistics-registry-related memory leaks

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 235ebb35485dbca42c554f95065101d0342f8eab..a6fe1088822ec84031886bd01c285929c7711ddc 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -188,8 +188,6 @@ int runCvc4(int argc, char* argv[]) {
   }
 
   Result asSatResult = lastResult.asSatisfiabilityResult();
-  
-
   int returnValue;
 
   switch(asSatResult.isSAT()) {
@@ -216,15 +214,18 @@ int runCvc4(int argc, char* argv[]) {
 
   // Remove the parser
   delete parser;
-ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
+
+  ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
   StatisticsRegistry::registerStat(&s_statSatResult);
 
   if(options.statistics){
     StatisticsRegistry::flushStatistics(cerr);
   }
 
-  return returnValue;
+  StatisticsRegistry::unregisterStat(&s_statSatResult);
+  StatisticsRegistry::unregisterStat(&s_statFilename);
 
+  return returnValue;
 }
 
 void doCommand(SmtEngine& smt, Command* cmd) {

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 7229b35657dfdda76f36a60a07f54d5e5b12ab8d..63c17f5130507ee3840d3b1cfdbb2ab8a044361c 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -126,7 +126,7 @@ class SatSolver : public SatInputInterface {
 
   /** Remember the options */
   Options* d_options;
-  
+
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
      sub-class for each solver. */
@@ -165,6 +165,17 @@ class SatSolver : public SatInputInterface {
       StatisticsRegistry::registerStat(&d_statMaxLiterals);
       StatisticsRegistry::registerStat(&d_statTotLiterals);
     }
+    ~Statistics() {
+      StatisticsRegistry::unregisterStat(&d_statStarts);
+      StatisticsRegistry::unregisterStat(&d_statDecisions);
+      StatisticsRegistry::unregisterStat(&d_statRndDecisions);
+      StatisticsRegistry::unregisterStat(&d_statPropagations);
+      StatisticsRegistry::unregisterStat(&d_statConflicts);
+      StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
+      StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
+      StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
+      StatisticsRegistry::unregisterStat(&d_statTotLiterals);
+    }
     void init(Minisat::SimpSolver* d_minisat){
       d_statStarts.setData(d_minisat->starts);
       d_statDecisions.setData(d_minisat->decisions);