projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cf29fe2) | patch
Fix non-idempotent rewrite in Array rewriter
authorAndres Noetzli <noetzli@stanford.edu>
Wed, 4 Jan 2017 17:20:34 +0000 (09:20 -0800)
committerAndres Nötzli <andres.noetzli@gmail.com>
Wed, 18 Jan 2017 21:07:43 +0000 (13:07 -0800)
commita8a7949ec3e1a7f2a2d241d0fc58e08cbf4b7aec
treeb66b6806c1d2e20aeb986b0ca5dd7f01ce1cd640tree
parentcf29fe25fa902c23e440c02abe945f8441c60ec8commit | 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.
src/theory/arrays/theory_arrays_rewriter.h diff | blob | history
test/regress/regress0/arrays/Makefile.am diff | blob | history
test/regress/regress0/arrays/bug637.delta.smt2 [new file with mode: 0644] blob