Add regression test for new error handling

Add a new regression test for error handling for z3
output that came from a Issue #5970

Author: TGWDB

regression/cbmc/z3/Issue5970.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void main()
+{
+  unsigned A, x[64];
+  // clang-format off
+  __CPROVER_assume(0 <= A && A < 64);
+  __CPROVER_assume(__CPROVER_forall { int i ; (0 <= i && i < A) ==> x[i] >= 1 });
+  // clang-format on
+  assert(x[0] > 0);
+}

regression/cbmc/z3/Issue5970.desc

@@ -0,0 +1,12 @@
+CORE smt-backend broken-cprover-smt-backend
+Issue5970.c
+--z3
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line 8 assertion x\[0\] > 0: FAILURE$
+--
+invalid get-value term, term must be ground and must not contain quantifiers
+^\[main\.assertion\.1\] line 8 assertion x\[0\] > 0: ERROR$
+--
+This tests that attempts to "(get-value |XXX|)" from z3 sat results
+are handled and do not cause an error message or ERROR result.