Fix byte update of struct/array elements

A key part of this is factoring out code that was almost-the-same from
lower_byte_update_array_vector and lower_byte_update_struct, but
actually had subtle bugs as documented in regression test included in
this commit.

For consistency, do all offset calculations in bits rather than flipping
back and forth between bits and bytes.

Author: tautschnig

regression/cbmc/byte_update18/main.c

@@ -0,0 +1,22 @@
+struct S
+{
+  unsigned char A[1];
+  char len; // keep this to reproduce
+};
+
+struct O
+{
+  struct S A[2];
+  char len; // this is key to reproduce
+};
+
+int main()
+{
+  struct O t = {{{{0}, 2}, {{42}, 2}}, 2};
+  unsigned n;
+  __CPROVER_assume(n < 2);
+  __CPROVER_assume(n > 0);
+  char src_n[n];
+  __CPROVER_array_replace((char *)t.A[0].A, src_n);
+  __CPROVER_assert(t.A[1].A[0] == 42, "");
+}

regression/cbmc/byte_update18/test.desc

@@ -0,0 +1,11 @@
+CORE broken-cprover-smt-backend
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Some bug in our in-tree SMT2 solver makes it report SAT, when Z3 states that the
+same SMT2 formula is (as expected) UNSAT.