Merge pull request diffblue#7222 from tautschnig/bugfixes/7164-space

External SAT back-end: handle whitespace at end of line gracefully

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

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