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

3 files changed, 16 insertions, 5 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 197134b6a..4fa96c231 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -429,8 +429,11 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
 
   // If both constants are nonzero, combine on right, otherwise leave them where they are
   if (rightConst != zero) {
+    leftConst = zero;
     rightConst = rightConst - leftConst;
-    childrenRight.push_back(utils::mkConst(rightConst));
+    if (rightConst != zero) {
+      childrenRight.push_back(utils::mkConst(rightConst));
+    }
   }
   else if (leftConst != zero) {
     childrenLeft.push_back(utils::mkConst(leftConst));
@@ -540,6 +543,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
     newRight = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenRight);
   }
 
+  Assert(newLeft == Rewriter::rewrite(newLeft));
+  Assert(newRight == Rewriter::rewrite(newRight));
+
   if (newLeft == newRight) {
     Assert (newLeft == utils::mkConst(size, (unsigned)0));
     return utils::mkTrue();
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index d6de6edbd..47725444d 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -107,7 +107,7 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
       RewriteRule<UleZero>,
       RewriteRule<UleSelf>
       >::apply(node);
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+  return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }
 
 RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
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);