From 61e3aa5a2483aeb02ec76380725f842471451927 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Sat, 14 Jun 2014 14:18:45 -0400
Subject: [PATCH] fix to inequality rewrite

---
 src/theory/bv/theory_bv_rewrite_rules_simplification.h | 4 ++++
 1 file changed, 4 insertions(+)

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