From 436c124105897977cec7a7f11c716f678dd3b7a5 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 18 Jun 2012 22:18:27 +0000
Subject: [PATCH] Fixed bug in rewriter

---
 src/theory/arrays/theory_arrays_rewriter.h | 111 +++++++++++----------
 1 file changed, 57 insertions(+), 54 deletions(-)

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index d59ef736d..5de9d225f 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -53,36 +53,39 @@ public:
               break;
             }
             val = eqRewritten.getConst<bool>();
-            if (val) {
-              // select(store(a,i,v),i) = v
-              return RewriteResponse(REWRITE_DONE, store[2]);
-            }
-            else {
-              // select(store(a,i,v),j) = select(a,j) if i /= j
-              store = store[0];
-              Node n;
-              while (store.getKind() == kind::STORE) {
-                if (index == store[1]) {
-                  val = true;
-                }
-                else if (index.isConst() && store[1].isConst()) {
-                  val = false;
-                }
-                else {
-                  n = Rewriter::rewrite(store[1].eqNode(index));
-                  if (n.getKind() != kind::CONST_BOOLEAN) {
-                    break;
-                  }
-                  val = n.getConst<bool>();
-                }
-                if (val) {
-                  return RewriteResponse(REWRITE_DONE, store[2]);
+          }
+          if (val) {
+            // select(store(a,i,v),i) = v
+            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl;
+            return RewriteResponse(REWRITE_DONE, store[2]);
+          }
+          else {
+            // select(store(a,i,v),j) = select(a,j) if i /= j
+            store = store[0];
+            Node n;
+            while (store.getKind() == kind::STORE) {
+              if (index == store[1]) {
+                val = true;
+              }
+              else if (index.isConst() && store[1].isConst()) {
+                val = false;
+              }
+              else {
+                n = Rewriter::rewrite(store[1].eqNode(index));
+                if (n.getKind() != kind::CONST_BOOLEAN) {
+                  break;
                 }
-                store = store[0];
+                val = n.getConst<bool>();
               }
-              n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
-              return RewriteResponse(REWRITE_DONE, n);
+              if (val) {
+                Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl;
+                return RewriteResponse(REWRITE_DONE, store[2]);
+              }
+              store = store[0];
             }
+            n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
+            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
+            return RewriteResponse(REWRITE_DONE, n);
           }
         }
         break;
@@ -202,36 +205,36 @@ public:
               break;
             }
             val = eqRewritten.getConst<bool>();
-            if (val) {
-              // select(store(a,i,v),i) = v
-              return RewriteResponse(REWRITE_DONE, store[2]);
-            }
-            else {
-              // select(store(a,i,v),j) = select(a,j) if i /= j
-              store = store[0];
-              Node n;
-              while (store.getKind() == kind::STORE) {
-                if (index == store[1]) {
-                  val = true;
-                }
-                else if (index.isConst() && store[1].isConst()) {
-                  val = false;
-                }
-                else {
-                  n = Rewriter::rewrite(store[1].eqNode(index));
-                  if (n.getKind() != kind::CONST_BOOLEAN) {
-                    break;
-                  }
-                  val = n.getConst<bool>();
-                }
-                if (val) {
-                  return RewriteResponse(REWRITE_DONE, store[2]);
+          }
+          if (val) {
+            // select(store(a,i,v),i) = v
+            return RewriteResponse(REWRITE_DONE, store[2]);
+          }
+          else {
+            // select(store(a,i,v),j) = select(a,j) if i /= j
+            store = store[0];
+            Node n;
+            while (store.getKind() == kind::STORE) {
+              if (index == store[1]) {
+                val = true;
+              }
+              else if (index.isConst() && store[1].isConst()) {
+                val = false;
+              }
+              else {
+                n = Rewriter::rewrite(store[1].eqNode(index));
+                if (n.getKind() != kind::CONST_BOOLEAN) {
+                  break;
                 }
-                store = store[0];
+                val = n.getConst<bool>();
               }
-              n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
-              return RewriteResponse(REWRITE_DONE, n);
+              if (val) {
+                return RewriteResponse(REWRITE_DONE, store[2]);
+              }
+              store = store[0];
             }
+            n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
+            return RewriteResponse(REWRITE_DONE, n);
           }
         }
         break;
-- 
2.30.2