From 7e23ff52320d1024307c32ecc2db849c7ce14f46 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 1 Feb 2022 09:26:16 -0800 Subject: [PATCH] [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. --- src/theory/arrays/theory_arrays_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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; -- 2.30.2