Add test that Z3 solver support is present and working

This confirms that Z3 is present and working in CI, as well as that
cbmc's support for Z3 is not entirely broken.

Author: thomasspriggs

regression/cbmc/z3/invalid.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned int non_det;
+  assert(non_det * non_det != 9u);
+  return 0;
+}

regression/cbmc/z3/invalid.desc

@@ -0,0 +1,14 @@
+CORE
+invalid.c
+--trace --smt2 --z3
+^EXIT=10$
+^SIGNAL=0$
+line 6 assertion non_det \* non_det != 9u: FAILURE
+non_det=\d+u
+VERIFICATION FAILED
+--
+line 6 assertion non_det \* non_det != 9u: ERROR
+error running SMT2 solver
+--
+Run cbmc with the --z3 option to confirm that support for the Z3 solver is
+available and working for an invalid program where the assertion may fail.

regression/cbmc/z3/valid.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned int non_det;
+  assert(non_det * non_det != 12u);
+  return 0;
+}

regression/cbmc/z3/valid.desc

@@ -0,0 +1,13 @@
+CORE
+valid.c
+--trace --smt2 --z3
+^EXIT=0$
+^SIGNAL=0$
+line 6 assertion non_det \* non_det != 12u: SUCCESS
+VERIFICATION SUCCESSFUL
+--
+line 6 assertion non_det \* non_det != 12u: ERROR
+error running SMT2 solver
+--
+Run cbmc with the --z3 option to confirm that support for the Z3 solver is
+available and working for a valid program.