Test trace-values: create reads to enforce instantiation

The test specification expects that the indices 0, 1, and one other are
instantiated. The array theory is only required to do so when also
reading from these elements.

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);
 }