Add regression tests for array output with z3

Add two regression tests to check for array output in traces.

Author: TGWDB

regression/cbmc/z3/trace-char.c

@@ -0,0 +1,5 @@
+void main(int argc, char **argv)
+{
+  char arr[] = {'0', '1', '2', '3', '4', '5', '6', '7'};
+  assert(arr[0] == '2');
+}

regression/cbmc/z3/trace-char.desc

@@ -0,0 +1,13 @@
+CORE smt-backend broken-cprover-smt-backend
+trace-char.c
+--trace --smt2 --z3
+^EXIT=10$
+^SIGNAL=0$
+arr=\{ arr
+arr=\{ '0', '1', '2', '3', '4', '5', '6', '7' \}
+--
+arr=(assignment removed)
+error running SMT2 solver
+--
+Run cbmc with the --z3 and --trace options with arrays to confirm that
+char arrays are displayed in traces.

regression/cbmc/z3/trace.c

@@ -0,0 +1,5 @@
+void main(int argc, char **argv)
+{
+  int arr[] = {0, 1, 2, 3, 4, 5, 6, 17};
+  assert(arr[0] == 2);
+}

regression/cbmc/z3/trace.desc

@@ -0,0 +1,13 @@
+CORE smt-backend broken-cprover-smt-backend
+trace.c
+--trace --smt2 --z3
+^EXIT=10$
+^SIGNAL=0$
+arr=\{ arr
+arr=\{ 0, 1, 2, 3, 4, 5, 6, 17 \}
+--
+arr=(assignment removed)
+error running SMT2 solver
+--
+Run cbmc with the --z3 and --trace options with arrays to confirm that
+int arrays are displayed in traces.