# HG changeset patch
# User blanchet
# Date 1444340427 -7200
# Node ID 1190beb207629f2b251a1408ca251ed9bb45d199
# Parent  4a47a4c3e8d5dd8946df31d3c4a26ad0fa2bb34e
made TPTP SZS status more compliant

diff -r 4a47a4c3e8d5 -r 1190beb20762 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Oct 08 22:41:21 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Oct 08 23:40:27 2015 +0200
@@ -905,7 +905,7 @@
                                  scope = n
                      ? Integer.add 1) (!generated_scopes) 0
       in
-        (if mode = TPTP then "% SZS status Unknown\n" else "") ^
+        (if mode = TPTP then "% SZS status GaveUp\n" else "") ^
         "Nitpick " ^ did_so_and_so ^
         (if is_some (!checked_problems) andalso total > 0 then
            " " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope"
@@ -934,7 +934,7 @@
           (print_nt (fn () => excipit "checked"); unknownN)
         else if max_genuine = original_max_genuine then
           if max_potential = original_max_potential then
-            (print_t (K "% SZS status Unknown");
+            (print_t (K "% SZS status GaveUp");
              print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ ".");
              if skipped > 0 then unknownN else noneN)
           else
@@ -991,13 +991,13 @@
               (pick_them_nits_in_term deadline state params mode i n step subst
                                       def_assm_ts nondef_assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
-                 (print_t "% SZS status Unknown";
+                 (print_t "% SZS status GaveUp";
                   print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
                | TOO_SMALL (_, details) =>
-                 (print_t "% SZS status Unknown";
+                 (print_t "% SZS status GaveUp";
                   print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
                | Kodkod.SYNTAX (_, details) =>
-                 (print_t "% SZS status Unknown";
+                 (print_t "% SZS status GaveUp";
                   print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
                   unknown_outcome)
                | TimeLimit.TimeOut =>