Add array update regression test

Author: Enrico Steffinlongo

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

@@ -0,0 +1,9 @@
+int main()
+{
+  int example_array[10000];
+  unsigned int index;
+  __CPROVER_assume(index < 10000);
+  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/array_write.desc

@@ -0,0 +1,11 @@
+CORE
+array_write.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: SUCCESS
+\[main\.assertion\.2\] line \d+ Array condition: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of updating the value at an index of an array.