[Arrays] Fix response for `store` chains (#8015)

When rewriting applying the rule store(store(a,i,v),i,w) ---> store(a,i,w), the arrays rewriter would return REWRITE_DONE. However,
this is incorrect if there are three or more nested stores of that kind
or the rewrite store(a,i,select(a,i)) ---> a applies to the result.
This commit fixes the response to always be REWRITE_AGAIN.

diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index 5bc0ea176263ab364942a395ca75b421d88c8b28..2047bcb0f722b276951992edd44741e6225df697 100644 (file)
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -639,7 +639,10 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
           Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
           Trace("arrays-prerewrite")
               << "Arrays::preRewrite returning " << newNode << std::endl;
-          return RewriteResponse(REWRITE_DONE, newNode);
+          // We may have more than two nested stores to the same index or the
+          // rule above (store(a,i,select(a,i)) ---> a) may apply after this
+          // rewrite, so we return REWRITE_AGAIN here.
+          return RewriteResponse(REWRITE_AGAIN, newNode);
         }
       }
       break;