diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-21 18:07:45 -0800 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-21 18:07:45 -0800 |
commit | c0c424283c12cfce2874ea92188487d91acecdf3 (patch) | |
tree | 75af6c90758c754d3faa9463602faf2120a10529 /test/regress/regress0 | |
parent | c12cfca2bdd44b6cda5c61a764ae6aee150c384b (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 'test/regress/regress0')
0 files changed, 0 insertions, 0 deletions