summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
authorAndres Notzli <andres.noetzli@gmail.com>2016-11-21 18:07:45 -0800
committerAndres Notzli <andres.noetzli@gmail.com>2016-11-21 18:07:45 -0800
commitc0c424283c12cfce2874ea92188487d91acecdf3 (patch)
tree75af6c90758c754d3faa9463602faf2120a10529 /examples
parentc12cfca2bdd44b6cda5c61a764ae6aee150c384b (diff)
Fix `MultDistrib` rewrite rule
The assertion in the `MultDistrib` rule would fail when doing: ``` Node expr = d_nm->mkNode(BITVECTOR_MULT, mkNode(BITVECTOR_SUB, x, y), z); if (RewriteRule<MultDistrib>::applies(expr)) RewriteRule<MultDistrib>::apply(expr); ``` When checking which side to distribute over, the code only checked for `BITVECTOR_PLUS` instead of `BITVECTOR_PLUS` or `BITVECTOR_SUB` in contrast to the other conditions in `RewriteRule<MultDistrib>::applies()` and the assert. NOTE: I was only able to reproduce this issue when testing the rewrite rule in isolation. The rule `SubEliminate` generally seems to turn the `BITVECTOR_SUB` node into a `BITVECTOR_PLUS` node before the rewriter tries `MultDistrib`.
Diffstat (limited to 'examples')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback