Add regression test for SMT unknown result

This adds a regression test for the SMT solver (here z3) returning
a satisfiability result of "unknown" and reporting this to the user

Author: TGWDB

regression/cbmc/z3/Issue5977.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void main()
+{
+  int i;
+  __CPROVER_assume(i % 2 == 0);
+  assert(__CPROVER_exists {
+    int j;
+    i == j + j
+  });
+}

regression/cbmc/z3/Issue5977.desc

@@ -0,0 +1,9 @@
+CORE smt-backend broken-cprover-smt-backend
+Issue5977.c
+--z3
+^EXIT=(6|10)$
+^SIGNAL=0$
+^SMT2 solver returned "unknown"$
+--
+--
+This tests that an "unknown" result from the SMT solver is reported.