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`.

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 4abd02e734048e489b7857cbce20747752d75754..89bb3d7ac24176123fc233e78021d2e37660aa63 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -492,8 +492,10 @@ template<> inline
 Node RewriteRule<MultDistrib>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")" << std::endl;
 
-  TNode factor = node[0].getKind() != kind::BITVECTOR_PLUS ? node[0] : node[1];
-  TNode sum = node[0].getKind() == kind::BITVECTOR_PLUS? node[0] : node[1];
+  bool is_rhs_factor = node[0].getKind() == kind::BITVECTOR_PLUS ||
+                       node[0].getKind() == kind::BITVECTOR_SUB;
+  TNode factor = !is_rhs_factor ? node[0] : node[1];
+  TNode sum = is_rhs_factor ? node[0] : node[1];
   Assert (factor.getKind() != kind::BITVECTOR_PLUS &&
           factor.getKind() != kind::BITVECTOR_SUB &&
           (sum.getKind() == kind::BITVECTOR_PLUS ||