From 778004b0fe366f6ecfb53a594bd5be335a2dc4b7 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Tue, 7 May 2013 16:32:07 -0400
Subject: [PATCH] one more fix for rewrites

---
 src/theory/bv/theory_bv_rewriter.cpp | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 621ae25c0..534347c4a 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -230,7 +230,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) {
   if (!prerewrite) {
     resultNode = LinearRewriteStrategy
       < RewriteRule<BitwiseSlicing>
-        >::apply(node);
+        >::apply(resultNode);
   
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -250,7 +250,7 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){
   if (!prerewrite) {
     resultNode = LinearRewriteStrategy
       < RewriteRule<BitwiseSlicing>
-        >::apply(node);
+        >::apply(resultNode);
     
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -273,7 +273,7 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) {
     resultNode = LinearRewriteStrategy
       < RewriteRule<XorOne>, 
       RewriteRule <BitwiseSlicing>
-        >::apply(node);
+        >::apply(resultNode);
     
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -341,15 +341,24 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
 }
 
 RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) {
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>, 
+  Node resultNode = node;
+  if (prerewrite) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<FlattenAssocCommut>
+        >::apply(node);
+    return RewriteResponse(REWRITE_DONE, resultNode);
+  }
+  
+  resultNode =  LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>,
       RewriteRule<PlusCombineLikeTerms>
       >::apply(node);
-  if (prerewrite || node == resultNode) {
-    return RewriteResponse(REWRITE_DONE, resultNode);
+
+  if (node != resultNode) {
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
   }
   
-  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
 RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){
-- 
2.30.2