summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/bool_to_bv.cpp8
1 files changed, 7 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback