projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 000feae) | patch
Fix extended rewriter for binary associative operators. (#2751)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Dec 2018 02:17:50 +0000 (20:17 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Fri, 14 Dec 2018 02:17:50 +0000 (02:17 +0000)
commit075e3d97974c89dcbd4cf6c7a1c3b37cbb27403d
treecb1466de550072e4a11d0a67816e6e23ef5770cbtree
parent000feaeb02292d7a2873198664022801b12e5151commit | diff
 Fix extended rewriter for binary associative operators. (#2751)

This was causing assertion failures when using Sets + Sygus.
src/theory/quantifiers/extended_rewrite.cpp diff | blob | history
src/theory/quantifiers/term_util.cpp diff | blob | history
src/theory/quantifiers/term_util.h diff | blob | history
src/theory/sets/theory_sets_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sets/sets-extr.smt2 [new file with mode: 0644] blob