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 3f9405785de63fc2bbd91714f725e40176011fce..045ac3f3975061366e65cad5bbd9388b422d4b54 100644 (file)
--- 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();