more robust backend identification
authorblanchet
Fri, 08 Sep 2017 01:19:40 +0200
changeset 66638 4bc61fea2700
parent 66637 809d40cfa4de
child 66639 6a3cefd026fb
more robust backend identification
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 = []})