diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-08-01 13:07:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-01 13:07:18 -0700 |
commit | 08c1ed76932102948bca5157a5da64033ea1c408 (patch) | |
tree | d6a89eb68e583aa41f4f3b932275c8b72069b1a8 /src/theory/rewriter.cpp | |
parent | c1d9bed7f73db9567f635f59cde134795e65c9ba (diff) |
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.
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 14 |
1 files 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(); |