From a982d0ab03118e31c40052c9beae6ffaec5318aa Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 11 Jun 2012 17:31:13 +0000
Subject: [PATCH] OK, now the rewrite issues are fixed

---
 .../bv/theory_bv_rewrite_rules_normalization.h     |  8 ++++----
 src/theory/bv/theory_bv_rewriter.cpp               | 14 +++++++++++---
 src/theory/rewriter.cpp                            |  4 +++-
 3 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index f5577e2ed..6ac9da7cb 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -300,10 +300,10 @@ Node RewriteRule<MultSimplify>::apply(TNode node) {
     TNode current = node[i];
     if (current.getKind() == kind::CONST_BITVECTOR) {
       BitVector value = current.getConst<BitVector>();
-      if(value == BitVector(size, (unsigned) 0)) {
+      constant = constant * value;
+      if(constant == BitVector(size, (unsigned) 0)) {
         return utils::mkConst(size, 0); 
       }
-      constant = constant * current.getConst<BitVector>();
     } else {
       children.push_back(current); 
     }
@@ -543,8 +543,8 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
     newRight = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenRight);
   }
 
-  Assert(newLeft == Rewriter::rewrite(newLeft));
-  Assert(newRight == Rewriter::rewrite(newRight));
+  //  Assert(newLeft == Rewriter::rewrite(newLeft));
+  //  Assert(newRight == Rewriter::rewrite(newRight));
 
   if (newLeft == newRight) {
     Assert (newLeft == utils::mkConst(size, (unsigned)0));
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 85ccbc787..25cbae68c 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -525,13 +525,21 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
         RewriteRule<SimplifyEq>,
-        RewriteRule<ReflexivityEq>,
-        RewriteRule<SolveEq>
+        RewriteRule<ReflexivityEq>
         >::apply(node);
 
+    if(RewriteRule<SolveEq>::applies(resultNode)) {
+      resultNode = RewriteRule<SolveEq>::run<false>(resultNode);
+      if (resultNode != node) {
+        return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+      }
+    }
+
     if(RewriteRule<BitwiseEq>::applies(resultNode)) {
       resultNode = RewriteRule<BitwiseEq>::run<false>(resultNode);
-      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+      if (resultNode != node) {
+        return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+      }
     }
 
     return RewriteResponse(REWRITE_DONE, resultNode); 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 7d5f541c0..0c5cada09 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -163,6 +163,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node 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
+          Assert(response.node != rewriteStackTop.node);
           rewriteStackTop.node = rewriteTo(newTheoryId, response.node);
           break;
         } else if (response.status == REWRITE_DONE) {
@@ -173,7 +174,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 	  rewriteStackTop.node = response.node;
           break;
         }
-        // Check for trivial rewrite loop of size 2
+        // Check for trivial rewrite loops of size 1 or 2
+        Assert(response.node != rewriteStackTop.node);
         Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node);
 	rewriteStackTop.node = response.node;
       }
-- 
2.30.2