diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 15:16:43 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:39:21 -0500 |
| commit | 195dffbb7468e814d3dc3226666688869c13ba3d (patch) | |
| tree | 4c4915245a90615ea36cbcfbb4a8a6dcc910c384 /src/theory/bv | |
| parent | 73760b3c213733fc98d67f9ceeb74d06b01a3777 (diff) | |
Fix errors and reduce warnings on clang (merge from mdeters/clang)
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 23cd8381d..8bcc64414 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -430,10 +430,6 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) { template<> inline bool RewriteRule<XorNot>::applies(TNode node) { Unreachable(); - if (node.getKind() == kind::BITVECTOR_XOR && - node.getNumChildren() == 2 && - node[0].getKind() == kind::BITVECTOR_NOT && - node[1].getKind() == kind::BITVECTOR_NOT); } template<> inline |