Skip to content

Commit 9baef8f

Browse files
committed
Remove vectors: Boolean expressions do not require signed bitvectors
Any bitvector type will do as all we need to produce is a constant with all bits set (see https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html: "Vectors are compared element-wise producing 0 when comparison is false and -1 (constant of the appropriate type where all bits are set) otherwise.").
1 parent b0744ea commit 9baef8f

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/goto-programs/remove_vector.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -188,7 +188,6 @@ static void remove_vector(exprt &expr)
188188
const auto dimension = numeric_cast_v<std::size_t>(vector_type.size());
189189

190190
const typet &subtype = vector_type.element_type();
191-
PRECONDITION(subtype.id() == ID_signedbv);
192191
exprt minus_one = from_integer(-1, subtype);
193192
exprt zero = from_integer(0, subtype);
194193

0 commit comments

Comments
 (0)