change

2 files changed, 61 insertions, 54 deletions

diff --git a/src/theory/arrays/arrays_post.h b/src/theory/arrays/arrays_post.h
index 5dbf6a506..3e29d77f4 100644
--- a/src/theory/arrays/arrays_post.h
+++ b/src/theory/arrays/arrays_post.h
@@ -103,24 +103,24 @@ inline RewriteResponse arrays_post_rewrite6(TNode node, RewriteProof *proof) {
       Node rewritten_node = node[0];
       return arrays_post_rewrite5<Proof>(rewritten_node, proof);
     };
-    if ((node[0]).getKind() == kind::STORE) {
-      if ((true) && (node[0][1] == node[1])) {
-        if (Proof) {
-          proof->registerRewrite(arrays_post_STORE_STORE_I_I);
-        };
-        Node rewritten_node =
-            nm->mkNode(kind::STORE, node[0][0], node[0][1], node[2]);
-        return arrays_post_rewrite5<Proof>(rewritten_node, proof);
+    if (((node[0]).getKind() == kind::STORE) && (true) &&
+        (node[0][1] == node[1])) {
+      if (Proof) {
+        proof->registerRewrite(arrays_post_STORE_STORE_I_I);
       };
-      if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
-          nm->mkConst(true)) {
-        if (Proof) {
-          proof->registerRewrite(arrays_post_STORE_STORE_I_J);
-        };
-        Node rewritten_node =
-            nm->mkNode(kind::STORE, node[0][0], node[1], node[2]);
-        return arrays_post_rewrite5<Proof>(rewritten_node, proof);
-      }
+      Node rewritten_node =
+          nm->mkNode(kind::STORE, node[0][0], node[0][1], node[2]);
+      return arrays_post_rewrite5<Proof>(rewritten_node, proof);
+    };
+    if (((node[0]).getKind() == kind::STORE) &&
+        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
+         nm->mkConst(true))) {
+      if (Proof) {
+        proof->registerRewrite(arrays_post_STORE_STORE_I_J);
+      };
+      Node rewritten_node =
+          nm->mkNode(kind::STORE, node[0][0], node[1], node[2]);
+      return arrays_post_rewrite5<Proof>(rewritten_node, proof);
     }
   };
   return arrays_post_rewrite4<Proof>(node, proof);
@@ -135,18 +135,19 @@ inline RewriteResponse arrays_post_rewrite7(TNode node, RewriteProof *proof) {
 template <bool Proof>
 inline RewriteResponse arrays_post_rewrite8(TNode node, RewriteProof *proof) {
   NodeManager *nm = NodeManager::currentNM();
-  if (((node).getKind() == kind::SELECT) &&
-      ((node[0]).getKind() == kind::STORE)) {
-    if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
-        nm->mkConst(false)) {
+  if ((node).getKind() == kind::SELECT) {
+    if (((node[0]).getKind() == kind::STORE) &&
+        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
+         nm->mkConst(false))) {
       if (Proof) {
         proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_I_J);
       };
       Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]);
       return arrays_post_rewrite7<Proof>(rewritten_node, proof);
     };
-    if ((((node[0][1]).isConst()) && ((node[1]).isConst())) &&
-        ((node[0][1] != node[1]))) {
+    if (((node[0]).getKind() == kind::STORE) &&
+        ((((node[0][1]).isConst()) && ((node[1]).isConst())) &&
+         ((node[0][1] != node[1])))) {
       if (Proof) {
         proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_CONSTS);
       };
@@ -167,28 +168,29 @@ template <bool Proof>
 inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) {
   NodeManager *nm = NodeManager::currentNM();
   if ((node).getKind() == kind::SELECT) {
-    if ((node[0]).getKind() == kind::STORE) {
-      if ((true) && (node[0][1] == node[1])) {
-        if (Proof) {
-          proof->registerRewrite(arrays_post_SELECT_STORE_I_I);
-        };
-        Node rewritten_node = node[0][2];
-        return arrays_post_rewrite9<Proof>(rewritten_node, proof);
+    if (((node[0]).getKind() == kind::STORE) && (true) &&
+        (node[0][1] == node[1])) {
+      if (Proof) {
+        proof->registerRewrite(arrays_post_SELECT_STORE_I_I);
+      };
+      Node rewritten_node = node[0][2];
+      return arrays_post_rewrite9<Proof>(rewritten_node, proof);
+    };
+    if (((node[0]).getKind() == kind::STORE) &&
+        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
+         nm->mkConst(true))) {
+      if (Proof) {
+        proof->registerRewrite(arrays_post_SELECT_STORE_I_J);
       };
-      if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
-          nm->mkConst(true)) {
-        if (Proof) {
-          proof->registerRewrite(arrays_post_SELECT_STORE_I_J);
-        };
-        Node rewritten_node = node[0][2];
-        return arrays_post_rewrite9<Proof>(rewritten_node, proof);
-      }
+      Node rewritten_node = node[0][2];
+      return arrays_post_rewrite9<Proof>(rewritten_node, proof);
     };
     if (((node[0]).getKind() == kind::STORE_ALL) && (true)) {
       if (Proof) {
         proof->registerRewrite(arrays_post_SELECT_STORE_ALL);
       };
-      Node rewritten_node = node[0][0];
+      Node rewritten_node =
+          Node::fromExpr(node[0].getConst<ArrayStoreAll>().getExpr());
       return arrays_post_rewrite9<Proof>(rewritten_node, proof);
     }
   };
diff --git a/src/theory/arrays/arrays_pre.h b/src/theory/arrays/arrays_pre.h
index 7fabc17e6..a43b8fe7b 100644
--- a/src/theory/arrays/arrays_pre.h
+++ b/src/theory/arrays/arrays_pre.h
@@ -33,9 +33,9 @@ inline RewriteResponse arrays_pre_rewrite1(TNode node, RewriteProof *proof) {
 template <bool Proof>
 inline RewriteResponse arrays_pre_rewrite2(TNode node, RewriteProof *proof) {
   NodeManager *nm = NodeManager::currentNM();
-  if (((node).getKind() == kind::STORE) &&
-      ((node[0]).getKind() == kind::STORE)) {
-    if ((true) && (node[0][1] == node[1])) {
+  if ((node).getKind() == kind::STORE) {
+    if (((node[0]).getKind() == kind::STORE) && (true) &&
+        (node[0][1] == node[1])) {
       if (Proof) {
         proof->registerRewrite(arrays_pre_STORE_STORE_I_I);
       };
@@ -43,8 +43,9 @@ inline RewriteResponse arrays_pre_rewrite2(TNode node, RewriteProof *proof) {
           nm->mkNode(kind::STORE, node[0][0], node[0][1], node[2]);
       return arrays_pre_rewrite1<Proof>(rewritten_node, proof);
     };
-    if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
-        nm->mkConst(true)) {
+    if (((node[0]).getKind() == kind::STORE) &&
+        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
+         nm->mkConst(true))) {
       if (Proof) {
         proof->registerRewrite(arrays_pre_STORE_STORE_I_J);
       };
@@ -98,7 +99,8 @@ inline RewriteResponse arrays_pre_rewrite6(TNode node, RewriteProof *proof) {
     if (Proof) {
       proof->registerRewrite(arrays_pre_SELECT_STORE_ALL);
     };
-    Node rewritten_node = node[0][0];
+    Node rewritten_node =
+        Node::fromExpr(node[0].getConst<ArrayStoreAll>().getExpr());
     return arrays_pre_rewrite5<Proof>(rewritten_node, proof);
   };
   return arrays_pre_rewrite4<Proof>(node, proof);
@@ -113,33 +115,36 @@ inline RewriteResponse arrays_pre_rewrite7(TNode node, RewriteProof *proof) {
 template <bool Proof>
 inline RewriteResponse arrays_pre_rewrite8(TNode node, RewriteProof *proof) {
   NodeManager *nm = NodeManager::currentNM();
-  if (((node).getKind() == kind::SELECT) &&
-      ((node[0]).getKind() == kind::STORE)) {
-    if ((true) && (node[0][1] == node[1])) {
+  if ((node).getKind() == kind::SELECT) {
+    if (((node[0]).getKind() == kind::STORE) && (true) &&
+        (node[0][1] == node[1])) {
       if (Proof) {
         proof->registerRewrite(arrays_pre_SELECT_STORE_I_I);
       };
       Node rewritten_node = node[0][2];
       return arrays_pre_rewrite7<Proof>(rewritten_node, proof);
     };
-    if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
-        nm->mkConst(false)) {
+    if (((node[0]).getKind() == kind::STORE) &&
+        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
+         nm->mkConst(false))) {
       if (Proof) {
         proof->registerRewrite(arrays_pre_SELECT_STORE_DIFF_I_J);
       };
       Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]);
       return arrays_pre_rewrite7<Proof>(rewritten_node, proof);
     };
-    if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
-        nm->mkConst(true)) {
+    if (((node[0]).getKind() == kind::STORE) &&
+        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
+         nm->mkConst(true))) {
       if (Proof) {
         proof->registerRewrite(arrays_pre_SELECT_STORE_I_J);
       };
       Node rewritten_node = node[0][2];
       return arrays_pre_rewrite7<Proof>(rewritten_node, proof);
     };
-    if ((((node[0][1]).isConst()) && ((node[1]).isConst())) &&
-        ((node[0][1] != node[1]))) {
+    if (((node[0]).getKind() == kind::STORE) &&
+        ((((node[0][1]).isConst()) && ((node[1]).isConst())) &&
+         ((node[0][1] != node[1])))) {
       if (Proof) {
         proof->registerRewrite(arrays_pre_SELECT_STORE_DIFF_CONSTS);
       };