diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-01 15:14:45 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-01 15:14:45 -0700 |
commit | e6325ad7e1f69193c3f9c489f75b4308b733009e (patch) | |
tree | a9582ec83099959158039c19f6b0aeac00f25541 /src/preprocessing | |
parent | 149134dfdb5a435ae4d1bea1a93ae3bde28fd646 (diff) |
Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 8 |
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; |