Add regression tests for array write traces

Author: thomasspriggs

regression/cbmc-incr-smt2/arrays_traces/array_write.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int example_array[1025];
+  unsigned int index;
+  __CPROVER_assume(index < 1025);
+  example_array[index] = 42;
+  __CPROVER_assert(example_array[index] == 42, "Array condition");
+  __CPROVER_assert(example_array[index] != 42, "Array condition");
+}

regression/cbmc-incr-smt2/arrays_traces/array_write.desc

@@ -0,0 +1,12 @@
+CORE
+array_write.c
+--trace
+Passing problem to incremental SMT2 solving
+^Trace for main\.assertion\.2
+example_array\[\d{1,4}ll?\]=42
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of writing a value at a non-deterministic index of an array, then asserting
+the value we expect.