diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/theory/rewriter.cpp | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index c98429dd2..d89724cbd 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -40,7 +40,9 @@ static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = class RewriterInitializer { static RewriterInitializer s_rewriterInitializer; - RewriterInitializer() { Rewriter::init(); } + RewriterInitializer() { + Rewriter::init(); + } ~RewriterInitializer() { Rewriter::shutdown(); } };/* class RewriterInitializer */ @@ -190,7 +192,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Incorporate the children if necessary if (rewriteStackTop.node.getNumChildren() > 0) { - rewriteStackTop.node = rewriteStackTop.builder; + Node rewritten = rewriteStackTop.builder; + rewriteStackTop.node = rewritten; rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node); } @@ -208,7 +211,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end()); s_rewriteStack->insert(response.node); #endif - rewriteStackTop.node = rewriteTo(newTheoryId, response.node); + Node rewritten = rewriteTo(newTheoryId, response.node); + rewriteStackTop.node = rewritten; #ifdef CVC4_ASSERTIONS s_rewriteStack->erase(response.node); #endif |