diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 9e69738d3..18274e060 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -160,15 +160,20 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Do the post-rewrite RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); // We continue with the response we got - rewriteStackTop.node = response.node; - TheoryId newTheoryId = Theory::theoryOf(rewriteStackTop.node); + TheoryId newTheoryId = Theory::theoryOf(response.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 - rewriteStackTop.node = rewriteTo(newTheoryId, rewriteStackTop.node); + rewriteStackTop.node = rewriteTo(newTheoryId, response.node); break; } else if (response.status == REWRITE_DONE) { +#ifdef CVC4_ASSERTIONS + RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); + Assert(r2.node == response.node); +#endif + rewriteStackTop.node = response.node; break; } + rewriteStackTop.node = response.node; } // We're done with the post rewrite, so we add to the cache Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node); |