--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Mon Feb 22 12:30:05 2021 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Mon Feb 22 13:29:55 2021 +0100
@@ -103,30 +103,30 @@
[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 {out = output, err = error, rc = code, ...} = Isabelle_System.bash_process bash_cmd;
+ val {out, err, rc, ...} = Isabelle_System.bash_process bash_cmd;
val backend =
- (case map_filter (try (unprefix "{backend:")) (split_lines output) of
+ (case map_filter (try (unprefix "{backend:")) (split_lines out) 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 = []})
- else if String.isPrefix "UNSAT" output then
+ if String.isPrefix "SAT" out then
+ (if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []})
+ else if String.isPrefix "UNSAT" out then
if complete then Unsat backend else Unknown NONE
- else if String.isSubstring "TIMEOUT" output
+ else if String.isSubstring "TIMEOUT" out
(* FIXME: temporary *)
- orelse String.isSubstring "kodkod failed (errcode 152)" error then
+ orelse String.isSubstring "kodkod failed (errcode 152)" err then
Timeout
- else if String.isPrefix "UNKNOWN" output then
+ else if String.isPrefix "UNKNOWN" out then
Unknown NONE
- else if code = 126 then
+ else if rc = 126 then
Nunchaku_Cannot_Execute
- else if code = 127 then
+ else if rc = 127 then
Nunchaku_Not_Found
else
- Unknown_Error (code,
- simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
+ Unknown_Error (rc,
+ simplify_spaces (elide_string 1000 (if err <> "" then err else out)))
end);
fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =