diff options
Diffstat (limited to 'src')
-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; } /** |