From 08c1ed76932102948bca5157a5da64033ea1c408 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 1 Aug 2019 13:07:18 -0700
Subject: [PATCH] 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.
---
 src/theory/rewriter.cpp | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

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();
-- 
2.30.2