Fixed bug in rewriter

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index d59ef736dff640d567cd032d569bfb6e9f068428..5de9d225fb2af844878e5721cbd1b85e9f228885 100644 (file)
--- 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;