diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2020-02-03 15:18:22 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-03 17:18:22 -0600 |
| commit | 6118996ec32a66fb8a62f42c79b093fdf82b9ef6 (patch) | |
| tree | cd45b58222d202737dc895ee0f4f52e00540579e | |
| parent | 35cf275a068f28c518acaab456ece16e19b6959c (diff) | |
Fix corner case - might need to REWRITE_AGAIN (#3706)
| -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) |