Byte-update lowering: fixup invariant for array-comprehension

In case of an array comprehension the number of operands must not be
used to sanity check the update offset (any update offset would be
valid). This was observed on several device driver benchmarks in
SV-COMP. One example (with --unwind 2):
ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i

Author: tautschnig

regression/cbmc/byte_update12/main.c

@@ -0,0 +1,18 @@
+#include <string.h>
+
+struct S
+{
+  int i;
+  int j;
+};
+
+int main()
+{
+  unsigned x;
+  char A[x];
+  __CPROVER_assume(x == sizeof(int));
+  A[0] = 42;
+  struct S s;
+  memcpy(&s, A, x);
+  __CPROVER_assert((s.i & 0xFF) == 42, "lowest byte is 42");
+}

regression/cbmc/byte_update12/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/lowering/byte_operators.cpp

@@ -1822,7 +1822,8 @@ static exprt lower_byte_update_struct(
     {
       offset = from_integer(0, src.offset().type());
       INVARIANT(
-        value_as_byte_array.operands().size() > -*offset_bytes,
+        value_as_byte_array.id() != ID_array ||
+          value_as_byte_array.operands().size() > -*offset_bytes,
         "members past the update should be handled above");
       first = numeric_cast_v<std::size_t>(-*offset_bytes);
     }