projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e9c115e) | patch
Fix quantifiers selector over store rewrite (#2510)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 25 Sep 2018 05:24:20 +0000 (00:24 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 25 Sep 2018 05:24:20 +0000 (22:24 -0700)
commitd383a8ff4868d80f33247b84e94c6ea9c0c1b3c5
tree10f6ef8c23277b0ba15a54b667453649360a8c64tree
parente9c115e82ea1341f1bbc37fb99c005aacec3d7eccommit | diff
Fix quantifiers selector over store rewrite (#2510)

Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.

After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
test/regress/regress0/quantifiers/qarray-sel-over-store.smt2 [new file with mode: 0644] blob