diff options
| author | lianah <lianahady@gmail.com> | 2014-06-14 14:18:45 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-14 14:18:45 -0400 |
| commit | 61e3aa5a2483aeb02ec76380725f842471451927 (patch) | |
| tree | 7cdf6df87d9a108aa619aa3a4e801bb926df9653 | |
| parent | d039293e5864502d454c6078790ea403cf3db869 (diff) | |
fix to inequality rewrite
| -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; |