src/HOL/Tools/Nitpick/kodkod.ML

                  "int_bounds: " ^
                  commas (map int_string_for_bound int_bounds) ^ "\n"));
          map (fn b => (out_assign b; out ";")) expr_assigns;
          out "solve "; out_outmost_f formula; out ";\n")
   in
-    out ("// This file was generated by Isabelle (probably Nitpick)\n" ^
+    out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
          "// " ^ Date.fmt "%Y-%m-%d %H:%M:%S"
                           (Date.fromTimeLocal (Time.now ())) ^ "\n");
     map out_problem problems
   end
 

               val (io_error, (ps, nontriv_js)) =
                 read_output_file out_path
                 ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
               val js = triv_js @ nontriv_js
               val first_error =
-                File.fold_lines (fn line => fn "" => line | s => s) err_path ""
-                handle IO.Io _ => "" | OS.SysErr _ => ""
+                (File.fold_lines (fn line => fn "" => line | s => s) err_path ""
+                 handle IO.Io _ => "" | OS.SysErr _ => "")
+                |> perhaps (try (unsuffix "\r"))
+                |> perhaps (try (unsuffix "."))
+                |> perhaps (try (unprefix "Error: "))
             in
               if null ps then
                 if code = 2 then
                   TimedOut js
                 else if code = 0 then

                 else if first_error |> Substring.full
                         |> Substring.position "NoClassDefFoundError" |> snd
                         |> Substring.isEmpty |> not then
                   NotInstalled
                 else if first_error <> "" then
-                  Error (first_error |> perhaps (try (unsuffix "."))
-                                     |> perhaps (try (unprefix "Error: ")), js)
+                  Error (first_error, js)
                 else if io_error then
                   Error ("I/O error", js)
                 else
                   Error ("Unknown error", js)
               else