# HG changeset patch
# User blanchet
# Date 1289843791 -3600
# Node ID de581d7da0b63c54e5421eacf23721792c2d2447
# Parent  ff446d5e9a62ba907f33272dacd85db180cfb399
interpret SMT_Failure.Solver_Crashed correctly

diff -r ff446d5e9a62 -r de581d7da0b6 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 18:56:30 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 18:56:31 2010 +0100
@@ -409,9 +409,15 @@
      run_time_in_msecs = msecs}
   end
 
+(* "SMT_Failure.Solver_Crashed" is a misnomer; it should really be called
+   "Abnormal_Termination". Return codes 1 to 127 are application-specific,
+   whereas (at least on Unix) 128 to 255 are reserved for signals (e.g.,
+   SIGSEGV) and other system codes. *)
+
 fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
-  | failure_from_smt_failure (SMT_Failure.Solver_Crashed _) = Crashed
+  | failure_from_smt_failure (SMT_Failure.Solver_Crashed code) =
+    if code >= 128 then Crashed else IncompleteUnprovable
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
@@ -463,10 +469,11 @@
             NONE => false
           | SOME (SMT_Failure.Counterexample _) => false
           | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
-          | SOME (SMT_Failure.Solver_Crashed _) =>
+          | SOME (SMT_Failure.Solver_Crashed code) =>
             (if verbose then
-               "The SMT solver crashed with " ^ string_of_int num_facts ^
-               " fact" ^ plural_s num_facts ^ "."
+               "The SMT solver invoked with " ^ string_of_int num_facts ^
+               " fact" ^ plural_s num_facts ^ " terminated abnormally with \
+               \exit code " ^ string_of_int code
                |> (if debug then error else warning)
              else
                ();