Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index b7078225a603e95e917bedd9ca509ade4754acbe..4c08d7e47f7f474b2f68e0ba878d825e25a3e48e 100644 (file)
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -95,7 +95,13 @@ Node BoolToBV::lowerNode(TNode current, bool topLevel)
       Kind new_kind = kind;
       switch (kind)
       {
-        case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
+        case kind::EQUAL:
+          if (current[0].getType().isBitVector()
+              || current[0].getType().isBoolean())
+          {
+            new_kind = kind::BITVECTOR_COMP;
+          }
+          break;
         case kind::AND: new_kind = kind::BITVECTOR_AND; break;
         case kind::OR: new_kind = kind::BITVECTOR_OR; break;
         case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;