Added a very fruitful assertion to the rewriter: checks that rewriting after "REWRITE_DONE" is idempotent

Found several problems where this is not the case and fixed them

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);