diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 1569fb008..a8a7d1127 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1168,6 +1168,10 @@ bool RewriteRule<UltPlusOne>::applies(TNode node) { if (y1[0].getKind() != kind::CONST_BITVECTOR && y1[1].getKind() != kind::CONST_BITVECTOR) return false; + + if (y1.getNumChildren() != 2) + return false; + TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1]; if (one != utils::mkConst(utils::getSize(one), 1)) return false; return true; |