diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2017-01-04 09:20:34 -0800 |
|---|---|---|
| committer | Andres Nötzli <andres.noetzli@gmail.com> | 2017-01-18 13:07:43 -0800 |
| commit | a8a7949ec3e1a7f2a2d241d0fc58e08cbf4b7aec (patch) | |
| tree | b66b6806c1d2e20aeb986b0ca5dd7f01ce1cd640 /src/theory/arrays | |
| parent | cf29fe25fa902c23e440c02abe945f8441c60ec8 (diff) | |
Fix non-idempotent rewrite in Array rewriter
This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index de10a861b..2726f386b 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -370,8 +370,9 @@ public: indices.pop_back(); elements.pop_back(); } + Assert(n != node); Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; - return RewriteResponse(REWRITE_DONE, n); + return RewriteResponse(REWRITE_AGAIN, n); } } break; |