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,8 @@
+#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=10$
+^SIGNAL=0$
+^SMT2 solver returned "unknown"$
+--
+--
+This tests that an "unknown" result from the SMT solver is reported.