diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2016-11-28 13:54:02 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-11-28 13:54:02 -0800 |
| commit | bc2378517a2f4100ba614cd44b3aa047089c82c8 (patch) | |
| tree | f04b70bf848eea734570ea6e25256b62e3e5e1db /src | |
| parent | 92d78a10ac24962efad4daf240acf5c5fb265a59 (diff) | |
| parent | c0c424283c12cfce2874ea92188487d91acecdf3 (diff) | |
Merge pull request #112 from 4tXJ7f/fix_mult_distrib
Fix `MultDistrib` rewrite rule
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4abd02e73..89bb3d7ac 100644 --- 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 || |