Test external SAT back-end

The test uses Z3 as this is a tool we expect to be installed in other
regression tests anyway.

Author: tautschnig

regression/cbmc/Failing_Assert1/external-z3.desc

@@ -0,0 +1,10 @@
+CORE gcc-only
+main.c
+--external-sat-solver ./z3-wrapper.sh --trace
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test is marked "gcc-only" as resolving ./ won't work with Windows.

regression/cbmc/Failing_Assert1/z3-wrapper.sh

@@ -0,0 +1,10 @@
+#!/bin/sh
+
+# handle output by older Z3 versions where the output was not compatible with
+# current SAT solvers
+
+z3 $1 2>&1 | \
+  perl -n -e '
+    print "s ".uc($1)."ISFIABLE\n" if(/^((un)?sat)\s*$/);
+    print "v $_\n" if(/^-?\d+/);
+    print "$_\n" if(/^[sv]\s+/);' 2>&1