Merge pull request #6826 from tautschnig/bugfixes/trace-values

Test trace-values: create reads to enforce instantiation

Author: tautschnig

regression/cbmc/trace-values/unbounded_array.c

@@ -9,5 +9,8 @@ int main(int argc, char *argv[])
   array[size - 1] = 42;
   int fixed_array[] = {1, 2};
   __CPROVER_array_replace(array, fixed_array);
+  assert(array[0] == 1);
+  assert(array[1] == 2);
+  assert(array[size - 1] == 42);
   assert(array[0] == 0);
 }