diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-11 18:18:44 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-12-11 18:18:44 -0800 |
| commit | 89be804959b82c68b69906c84d843a8ecc33056a (patch) | |
| tree | 694375e00ccf6b4433f5d5d6fe9351d44cc695f0 /src/theory | |
| parent | 89b08f2e68933e1da033f827ea1f10cd8ee224e9 (diff) | |
| parent | 762c8a3cf028fa7c12c2ee32d8643bd73ff2f07c (diff) | |
Merge pull request #116 from 4tXJ7f/fix_mult
Fix (inactive) `MultSlice` rewrite
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 6ef591760..871380467 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1108,13 +1108,10 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) { template<> inline bool RewriteRule<MultSlice>::applies(TNode node) { - if (node.getKind() != kind::BITVECTOR_MULT) { + if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) { return false; } - if (utils::getSize(node[0]) % 2 != 0) { - return false; - } - return true; + return utils::getSize(node[0]) % 2 == 0; } /** |