Remove vectors: Boolean expressions do not required 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.").

Author: tautschnig

src/goto-programs/remove_vector.cpp

@@ -14,6 +14,7 @@ Date:   September 2014
 #include "remove_vector.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/std_expr.h>
 
 #include <ansi-c/c_expr.h>
@@ -188,8 +189,11 @@ static void remove_vector(exprt &expr)
       const auto dimension = numeric_cast_v<std::size_t>(vector_type.size());
 
       const typet &subtype = vector_type.element_type();
-      PRECONDITION(subtype.id() == ID_signedbv);
-      exprt minus_one = from_integer(-1, subtype);
+      exprt minus_one = constant_exprt{
+        make_bvrep(
+          to_bitvector_type(subtype).get_width(),
+          [](std::size_t) { return true; }),
+        subtype};
       exprt zero = from_integer(0, subtype);
 
       exprt::operandst operands;