output SZS status as early as possible
authorblanchet
Wed Apr 25 14:33:21 2012 +0200 (2012-04-25 ago)
changeset 477520814fc93ab89
parent 47751 f98bbb445c06
child 47753 792634c6679e
output SZS status as early as possible
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 25 14:28:13 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 25 14:33:21 2012 +0200
     1.3 @@ -667,6 +667,14 @@
     1.4              ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
     1.5               : problem_extension) =
     1.6        let
     1.7 +        val _ =
     1.8 +          print_t (fn () =>
     1.9 +               "% SZS status " ^
    1.10 +               (if genuine then
    1.11 +                  if falsify then "CounterSatisfiable" else "Satisfiable"
    1.12 +                else
    1.13 +                  "Unknown") ^ "\n" ^
    1.14 +               "% SZS output start FiniteModel")
    1.15          val (reconstructed_model, codatatypes_ok) =
    1.16            reconstruct_hol_model
    1.17                {show_datatypes = show_datatypes, show_skolems = show_skolems,
    1.18 @@ -680,14 +688,7 @@
    1.19          fun assms_prop () =
    1.20            Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts)
    1.21        in
    1.22 -        (print_t (fn () =>
    1.23 -             "% SZS status " ^
    1.24 -             (if genuine then
    1.25 -                if falsify then "CounterSatisfiable" else "Satisfiable"
    1.26 -              else
    1.27 -                "Unknown") ^ "\n" ^
    1.28 -             "% SZS output start FiniteModel");
    1.29 -         pprint_a (Pretty.chunks
    1.30 +        (pprint_a (Pretty.chunks
    1.31               [Pretty.blk (0,
    1.32                    (pstrs ((if mode = Auto_Try then "Auto " else "") ^
    1.33                            "Nitpick found a" ^