diff --git a/regression/cbmc/Failing_Assert1/external-z3.desc b/regression/cbmc/Failing_Assert1/external-z3.desc
new file mode 100644
index 00000000000..0ca9b64dc45
--- /dev/null
+++ b/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.
diff --git a/regression/cbmc/Failing_Assert1/z3-wrapper.sh b/regression/cbmc/Failing_Assert1/z3-wrapper.sh
new file mode 100755
index 00000000000..cf069c0a893
--- /dev/null
+++ b/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
diff --git a/src/solvers/sat/external_sat.cpp b/src/solvers/sat/external_sat.cpp
index 752686ddc8c..d2d37d30bb5 100644
--- a/src/solvers/sat/external_sat.cpp
+++ b/src/solvers/sat/external_sat.cpp
@@ -109,7 +109,7 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
 
     if(line[0] == 'v')
     {
-      auto assignments = split_string(line, ' ');
+      auto assignments = split_string(line, ' ', false, true);
 
       // remove the first element which should be 'v' identifying
       // the line as the satisfying assignments