From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 26 Mar 2018 19:34:05 +0000 (-0700)
Subject: Fix memory leak in bvminisat (#1710)
X-Git-Tag: cvc5-1.0.0~5206
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b5b4e7c9df5bd9d5959c7c92a5b28c951881d49;p=cvc5.git

Fix memory leak in bvminisat (#1710)

While reviewing #1695, I realized that bvminisat is leaking memory for
each call to setNotify(). This commit uses std::unique_ptr to fix the
issue. It also adds std::unique_ptr to manage d_minisat.
---

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index e3632c08d..2aefbf11e 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -27,19 +27,17 @@ namespace prop {
 BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
 : context::ContextNotifyObj(mainSatContext, false),
   d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
-  d_minisatNotify(0),
+  d_minisatNotify(nullptr),
   d_assertionsCount(0),
   d_assertionsRealCount(mainSatContext, 0),
   d_lastPropagation(mainSatContext, 0),
   d_statistics(registry, name)
 {
-  d_statistics.init(d_minisat);
+  d_statistics.init(d_minisat.get());
 }
 
 
 BVMinisatSatSolver::~BVMinisatSatSolver() {
-  delete d_minisat;
-  delete d_minisatNotify;
 }
 
 void BVMinisatSatSolver::MinisatNotify::notify(
@@ -54,8 +52,8 @@ void BVMinisatSatSolver::MinisatNotify::notify(
 }
 
 void BVMinisatSatSolver::setNotify(Notify* notify) {
-  d_minisatNotify = new MinisatNotify(notify);
-  d_minisat->setNotify(d_minisatNotify);
+  d_minisatNotify.reset(new MinisatNotify(notify));
+  d_minisat->setNotify(d_minisatNotify.get());
 }
 
 ClauseId BVMinisatSatSolver::addClause(SatClause& clause,
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 4395cdf6d..6081296cb 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -18,6 +18,8 @@
 
 #pragma once
 
+#include <memory>
+
 #include "context/cdo.h"
 #include "proof/clause_id.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
@@ -49,8 +51,8 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
     void safePoint(unsigned amount) override { d_notify->safePoint(amount); }
   };
 
-  BVMinisat::SimpSolver* d_minisat;
-  MinisatNotify* d_minisatNotify;
+	std::unique_ptr<BVMinisat::SimpSolver> d_minisat;
+	std::unique_ptr<MinisatNotify> d_minisatNotify;
 
   unsigned d_assertionsCount;
   context::CDO<unsigned> d_assertionsRealCount;