From e6325ad7e1f69193c3f9c489f75b4308b733009e Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 1 Aug 2018 15:14:45 -0700 Subject: [PATCH] Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251) --- src/preprocessing/passes/bool_to_bv.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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; -- 2.30.2