From 05d64d040fd7340ec713af7b34515c3daac50220 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 28 Mar 2012 02:47:50 +0000
Subject: [PATCH] fixed faulty bv rewrite rule

---
 src/theory/bv/theory_bv_rewrite_rules_simplification.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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<>
-- 
2.30.2