From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 1 Feb 2022 17:26:16 +0000 (-0800)
Subject: [Arrays] Fix response for `store` chains (#8015)
X-Git-Tag: cvc5-1.0.0~487
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e23ff52320d1024307c32ecc2db849c7ce14f46;p=cvc5.git

[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 5bc0ea176..2047bcb0f 100644
--- 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;