Add regression test

Author: thomasspriggs

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

@@ -0,0 +1,13 @@
+int main()
+{
+  int example_array[] = {5, 4, 3, 2, 1};
+  unsigned int index;
+  __CPROVER_assume(index < 5);
+  __CPROVER_assert(example_array[index] != 42, "Non-existent element");
+  __CPROVER_assert(example_array[index] != 5, "Index 0");
+  __CPROVER_assert(example_array[index] != 4, "Index 1");
+  __CPROVER_assert(example_array[index] != 3, "Index 2");
+  __CPROVER_assert(example_array[index] != 2, "Index 3");
+  __CPROVER_assert(example_array[index] != 1, "Index 4");
+  __CPROVER_assert(example_array[index] == 5 - index, "Index value relation");
+}

regression/cbmc-incr-smt2/arrays/array_literal.desc

@@ -0,0 +1,16 @@
+CORE
+array_literal.c
+
+Passing problem to incremental SMT2 solving
+line \d+ Non-existent element: SUCCESS
+line \d+ Index 0: FAILURE
+line \d+ Index 1: FAILURE
+line \d+ Index 2: FAILURE
+line \d+ Index 3: FAILURE
+line \d+ Index 4: FAILURE
+line \d+ Index value relation: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of reading an array which is initialised using an array literal.