Fix corner case - might need to REWRITE_AGAIN (#3706)

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 851d2ca5d7df3779f6901f409560b7ad1660388e..e8c3d78d06ad64b577b3e7a84ef8be4930eb6428 100644 (file)
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -317,17 +317,9 @@ class TheoryArraysRewriter : public TheoryRewriter
           NodeManager* nm = NodeManager::currentNM();
           if (val) {
             // store(store(a,i,v),i,w) = store(a,i,w)
-            Node result;
-            if (value.getKind() == kind::SELECT &&
-                value[0] == store[0] &&
-                value[1] == index) {
-              result = store[0];
-            }
-            else {
-              result = nm->mkNode(kind::STORE, store[0], index, value);
-            }
+            Node result = nm->mkNode(kind::STORE, store[0], index, value);
             Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl;
-            return RewriteResponse(REWRITE_DONE, result);
+            return RewriteResponse(REWRITE_AGAIN, result);
           }
           else if (index < store[1]) {
             // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)