Fixes some assertion failures

1 files changed, 8 insertions, 5 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 896133e46..13c049c85 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -615,8 +615,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<BitwiseEq>::applies(TNode node) {
-  if (node.getKind() != kind::EQUAL ||
-      utils::getSize(node[0]) != 1) {
+  if (node.getKind() != kind::EQUAL) {
     return false;
   }
   TNode term;
@@ -636,11 +635,15 @@ bool RewriteRule<BitwiseEq>::applies(TNode node) {
     case kind::BITVECTOR_AND:
     case kind::BITVECTOR_OR:
       //operator BITVECTOR_XOR 2: "bitwise xor"
-    case kind::BITVECTOR_NOT:
     case kind::BITVECTOR_NAND:
     case kind::BITVECTOR_NOR:
       //operator BITVECTOR_XNOR 2 "bitwise xnor"
     case kind::BITVECTOR_COMP:
+      if (utils::getSize(node[0]) != 1) {
+        return false;
+      }
+      break;
+    case kind::BITVECTOR_NOT:
     case kind::BITVECTOR_NEG:
       return true;
       break;
@@ -678,7 +681,7 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) {
     term = node[0];
   }
 
-  bool eqOne = (c == BitVector(1,(unsigned)1));
+  bool eqOne = (c == BitVector(utils::getSize(node[0]),(unsigned)1));
 
   switch (term.getKind()) {
     case kind::BITVECTOR_AND:
@@ -724,7 +727,7 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) {
         return term[0].eqNode(term[1]).notNode();
       }
     case kind::BITVECTOR_NEG:
-      return term[0].eqNode(utils::mkConst(c));
+      return term[0].eqNode(utils::mkConst(-c));
     default:
       break;
   }