From 9baef8f447ca3db79f0603bf57dfcd9c56013446 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Oct 2022 19:02:16 +0000 Subject: [PATCH] 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."). --- src/goto-programs/remove_vector.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 65950af5e8e..86e5a5b3321 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -188,7 +188,6 @@ static void remove_vector(exprt &expr) const auto dimension = numeric_cast_v(vector_type.size()); const typet &subtype = vector_type.element_type(); - PRECONDITION(subtype.id() == ID_signedbv); exprt minus_one = from_integer(-1, subtype); exprt zero = from_integer(0, subtype);