added bvcomp case to bv to bool lifting

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 72131d6e716c66e32f1952fe283d99e8909cf4c6..aef1437a0e684cbf6786323df64ed7bde34a08a4 100644 (file)
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -86,7 +86,8 @@ bool BvToBoolPreprocessor::isConvertibleBvTerm(TNode node) {
       kind == kind::BITVECTOR_AND ||
       kind == kind::BITVECTOR_OR ||
       kind == kind::BITVECTOR_NOT ||
-      kind == kind::BITVECTOR_XOR) {
+      kind == kind::BITVECTOR_XOR ||
+      kind == kind::BITVECTOR_COMP) {
     return true; 
   }
 
@@ -156,7 +157,13 @@ Node BvToBoolPreprocessor::convertBvTerm(TNode node) {
     Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; 
     return result; 
   }
-  
+
+  if (kind == kind::BITVECTOR_COMP) {
+    Node result = utils::mkNode(kind::EQUAL, node[0], node[1]);
+    addToBoolCache(node, result);
+    Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; 
+    return result; 
+  }
 
   switch(kind) {
   case kind::BITVECTOR_OR: