From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 1 Aug 2019 20:07:18 +0000 (-0700)
Subject: Fix memory leak in rewriter (debug mode). (#3141)
X-Git-Tag: cvc5-1.0.0~4058
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08c1ed76932102948bca5157a5da64033ea1c408;p=cvc5.git

Fix memory leak in rewriter (debug mode). (#3141)

s_rewriteStack in rewriter.cpp was not properly cleaned up. This commit
wraps s_rewriteStack in a std::unique_ptr to automatically free the
memory.
---

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 3f9405785..045ac3f39 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -35,7 +35,8 @@ static TheoryId theoryOf(TNode node) {
 }
 
 #ifdef CVC4_ASSERTIONS
-static thread_local std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL;
+static thread_local std::unique_ptr<std::unordered_set<Node, NodeHashFunction>>
+    s_rewriteStack = nullptr;
 #endif /* CVC4_ASSERTIONS */
 
 class RewriterInitializer {
@@ -93,8 +94,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 #ifdef CVC4_ASSERTIONS
   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
-  if(s_rewriteStack == NULL) {
-    s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>();
+  if (s_rewriteStack == nullptr)
+  {
+    s_rewriteStack.reset(new std::unordered_set<Node, NodeHashFunction>());
   }
 #endif
 
@@ -255,9 +257,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
 void Rewriter::clearCaches() {
 #ifdef CVC4_ASSERTIONS
-  if(s_rewriteStack != NULL) {
-    delete s_rewriteStack;
-    s_rewriteStack = NULL;
+  if (s_rewriteStack != nullptr)
+  {
+    s_rewriteStack.reset(nullptr);
   }
 #endif
   Rewriter::clearCachesInternal();