Add regression tests for array read traces

Author: NlightNFotis

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

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

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

@@ -0,0 +1,15 @@
+CORE
+array_read.c
+--trace
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: FAILURE
+^Trace for main\.assertion\.1
+example_array=\{ (\d+, )*42
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of reading a value at a non-deterministic index of an array.
+Similar to the test in ../arrays/array_read.c, but we want to assert
+the value of the array that comes back in the trace to make sure we're
+observing the correct values.