diff options
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 3b813d1fa..507f98c91 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -558,7 +558,7 @@ Node RewriteRule<UleSelf>::apply(Node node) { template<> bool RewriteRule<ZeroUle>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULE && - node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); + node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); } template<> |