From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 1 Aug 2018 22:14:45 +0000 (-0700)
Subject: Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)
X-Git-Tag: cvc5-1.0.0~4835
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6325ad7e1f69193c3f9c489f75b4308b733009e;p=cvc5.git

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 b7078225a..4c08d7e47 100644
--- 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;