From 6118996ec32a66fb8a62f42c79b093fdf82b9ef6 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 3 Feb 2020 15:18:22 -0800 Subject: [PATCH] Fix corner case - might need to REWRITE_AGAIN (#3706) --- src/theory/arrays/theory_arrays_rewriter.h | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) 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) -- 2.30.2