# HG changeset patch
# User blanchet
# Date 1504826380 -7200
# Node ID 4bc61fea27009b6725edc27f55aea6543ba280d8
# Parent  809d40cfa4deaa15fc6255f68060ec96e6da7da4
more robust backend identification

diff -r 809d40cfa4de -r 4bc61fea2700 src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 01:14:33 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 01:19:40 2017 +0200
@@ -111,13 +111,9 @@
         val ((output, error), code) = bash_output_error bash_cmd;
 
         val backend =
-          (case filter_out (curry (op =) "") (split_lines output) of
-            [] => unknown_solver
-          | lines =>
-            (case try (unprefix "{backend:") (List.last lines) of
-              NONE => unknown_solver
-            | SOME "" => unknown_solver
-            | SOME s => hd (space_explode "," s)));
+          (case map_filter (try (unprefix "{backend:")) (split_lines output) of
+            [s] => hd (space_explode "," s)
+          | _ => unknown_solver);
       in
         if String.isPrefix "SAT" output then
           (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []})