Merge pull request #7855 from tautschnig/bugfixes/byte-update-members

Fix byte update of struct/array elements

Author: kroening

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.