byte_extract lowering over arrays: fix bits vs bytes error

The offset is computed in bits.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -246,7 +246,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
       {
         plus_exprt new_offset(
           unpacked.offset(),
-          from_integer(i * (*element_width), unpacked.offset().type()));
+          from_integer(i * (*element_width) / 8, unpacked.offset().type()));
 
         byte_extract_exprt tmp(unpacked);
         tmp.type()=subtype;

unit/solvers/lowering/byte_operators.cpp

@@ -116,9 +116,9 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       // union_typet({{"compA", u32}, {"compB", u64}}),
       c_enum_typet(u16),
       c_enum_typet(unsignedbv_typet(128)),
-      // array_typet(u8, size),
-      // array_typet(s32, size),
-      // array_typet(u64, size),
+      array_typet(u8, size),
+      array_typet(s32, size),
+      array_typet(u64, size),
       unsignedbv_typet(24),
       unsignedbv_typet(128),
       signedbv_typet(24),