diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 2e8acfa89..e0b1458fb 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -26,6 +26,8 @@ using namespace std; namespace CVC4 { namespace theory { +std::hash_set<Node, NodeHashFunction> d_rewriteStack; + /** * TheoryEngine::rewrite() keeps a stack of things that are being pre- * and post-rewritten. Each element of the stack is a @@ -172,7 +174,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite Assert(response.node != rewriteStackTop.node); + //TODO: this is not thread-safe - should make this assertion dependent on sequential build +#ifdef CVC4_ASSERTIONS + Assert(d_rewriteStack.find(response.node) == d_rewriteStack.end()); + d_rewriteStack.insert(response.node); +#endif rewriteStackTop.node = rewriteTo(newTheoryId, response.node); +#ifdef CVC4_ASSERTIONS + d_rewriteStack.erase(response.node); +#endif break; } else if (response.status == REWRITE_DONE) { #ifdef CVC4_ASSERTIONS |