diff options
| -rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 12 |
1 files 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) |