Add regression test

Test to see if z3 has get-value problem

Author: TGWDB

regression/contracts/z3_array_comprehension/main.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+void foo(char *dst, const char *src, size_t n)
+  __CPROVER_requires(__CPROVER_is_fresh(src, n))
+  __CPROVER_requires(__CPROVER_is_fresh(dst, n))
+  __CPROVER_assigns(__CPROVER_object_from(dst))
+  __CPROVER_ensures(__CPROVER_forall{size_t j; j < n ==> dst[j] == src[j]})
+{
+  for(size_t i = 0; i < n; i++)
+    __CPROVER_assigns(i, __CPROVER_object_from(dst))
+      // commenting out the loop invariant to make the analysis fail and reveal the error
+      // __CPROVER_loop_invariant(i <= n)
+      // __CPROVER_loop_invariant(__CPROVER_forall{size_t j; j < i ==> dst[j] == src[j]})
+    {
+      dst[i] = src[i];
+    }
+}
+
+int main()
+{
+  char *dst;
+  char *src;
+  size_t n;
+  foo(dst, src, n);
+  return 0;
+}

regression/contracts/z3_array_comprehension/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo --apply-loop-contracts --malloc-may-fail --malloc-fail-null _ --z3
+^\** 1 of 54 failed (2 iterations)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+SMT2 solver returned error message:
+invalid get-value term, term must be ground and must not contain quantifiers
+--
+Checks that there are not get-value errors related to lambdas in array
+comprehension leading to quantifiers in z3 values.