Fix `MultDistrib` rewrite rule
authorAndres Notzli <andres.noetzli@gmail.com>
Tue, 22 Nov 2016 02:07:45 +0000 (18:07 -0800)
committerAndres Notzli <andres.noetzli@gmail.com>
Tue, 22 Nov 2016 02:07:45 +0000 (18:07 -0800)
commitc0c424283c12cfce2874ea92188487d91acecdf3
tree75af6c90758c754d3faa9463602faf2120a10529
parentc12cfca2bdd44b6cda5c61a764ae6aee150c384b
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`.
src/theory/bv/theory_bv_rewrite_rules_normalization.h