# HG changeset patch
# User blanchet
# Date 1504821732 -7200
# Node ID 41ca77ba0f83f5edfd3c2c846ec9277ae72a4b93
# Parent  ee56847876b27d316d6d60c402fc818787797977
tuned Nunchaku's output

diff -r ee56847876b2 -r 41ca77ba0f83 src/HOL/Tools/Nunchaku/nunchaku.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:05 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:12 2017 +0200
@@ -136,6 +136,10 @@
 
 val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort);
 
+val unprefix_error =
+  perhaps (try (unprefix "Error: "))
+  #> perhaps (try (unprefix "failure: "));
+
 (* Give the soft timeout a chance. *)
 val timeout_slack = seconds 1.0;
 
@@ -213,10 +217,7 @@
               null whacks andalso null cards andalso null monos;
 
             fun unknown () =
-              (print_n ("No " ^ das_wort_model ^ " can be found\n\
-                 \The problem lies outside Nunchaku's fragment, or the Nunchaku backends are not \
-                 \installed properly");
-               (unknownN, NONE));
+              (print_n ("No " ^ das_wort_model ^ " found"); (unknownN, NONE));
 
             fun unsat_or_unknown complete =
               if complete then
@@ -268,7 +269,7 @@
               (print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE))
             | CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE))
             | Unknown_Error (code, msg) =>
-              (print_n ("Unknown error: " ^ msg ^
+              (print_n ("Unknown error: " ^ unprefix_error msg ^
                  (if code = 0 then "" else " (code " ^ string_of_int code ^ ")"));
                (unknownN, NONE)))
           end