diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-03-28 02:47:50 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-03-28 02:47:50 +0000 |
| commit | 05d64d040fd7340ec713af7b34515c3daac50220 (patch) | |
| tree | 0af797a2b7413f9b604c691c3fd5cec44af28125 /src | |
| parent | 2eec05ba299532c663fffc4262467a9b6771c2c4 (diff) | |
fixed faulty bv rewrite rule
Diffstat (limited to 'src')
| -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<> |