From: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon, 3 Feb 2020 23:18:22 +0000 (-0800)
Subject: Fix corner case - might need to REWRITE_AGAIN (#3706)
X-Git-Tag: cvc5-1.0.0~3688
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6118996ec32a66fb8a62f42c79b093fdf82b9ef6;p=cvc5.git

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 851d2ca5d..e8c3d78d0 100644
--- 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)