src/HOL/Tools/Nunchaku/nunchaku_tool.ML

   type nun_solution =
     {tys: (ty * tm list) list,
      tms: (tm * tm) list}
 
   datatype nun_outcome =
-    Unsat
-  | Sat of string * nun_solution
-  | Unknown of (string * nun_solution) option
+    Unsat of string
+  | Sat of string * string * nun_solution
+  | Unknown of (string * string * nun_solution) option
   | Timeout
   | Nunchaku_Var_Not_Set
   | Nunchaku_Cannot_Execute
   | Nunchaku_Not_Found
   | CVC4_Cannot_Execute

 type nun_solution =
   {tys: (ty * tm list) list,
    tms: (tm * tm) list};
 
 datatype nun_outcome =
-  Unsat
-| Sat of string * nun_solution
-| Unknown of (string * nun_solution) option
+  Unsat of string
+| Sat of string * string * nun_solution
+| Unknown of (string * string * nun_solution) option
 | Timeout
 | Nunchaku_Var_Not_Set
 | Nunchaku_Cannot_Execute
 | Nunchaku_Not_Found
 | CVC4_Cannot_Execute

   let val {out, err, rc, ...} = Bash.process s in
     ((out, err), rc)
   end;
 
 val nunchaku_home_env_var = "NUNCHAKU_HOME";
+
+val unknown_solver = "unknown";
 
 val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
   (NONE : ((string list * nun_problem) * nun_outcome) option);
 
 fun uncached_solve_nun_problem ({solvers, overlord, specialize, timeout, ...} : tool_params)

         val comments =
           [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];
         val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
         val _ = File.write prob_path prob_str;
         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)));
       in
         if String.isPrefix "SAT" output then
-          (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
+          (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []})
         else if String.isPrefix "UNSAT" output then
-          if complete then Unsat else Unknown NONE
+          if complete then Unsat backend else Unknown NONE
         else if String.isSubstring "TIMEOUT" output
             (* FIXME: temporary *)
             orelse String.isSubstring "kodkod failed (errcode 152)" error then
           Timeout
         else if String.isPrefix "UNKNOWN" output then

 
         fun update_cache () =
           Synchronized.change cached_outcome (K (SOME (key, outcome)));
       in
         (case outcome of
-          Unsat => update_cache ()
+          Unsat _ => update_cache ()
         | Sat _ => update_cache ()
         | Unknown _ => update_cache ()
         | _ => ());
         outcome
       end)