# HG changeset patch
# User boehmes
# Date 1289856208 -3600
# Node ID 0125cbb5d3c7828a9e23e1a1499ca8407cc5a0f4
# Parent  b57f7fee72ee926ddf09ef6a508371a98aa2aa4e
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed

diff -r b57f7fee72ee -r 0125cbb5d3c7 src/HOL/Tools/SMT/smt_failure.ML
--- a/src/HOL/Tools/SMT/smt_failure.ML	Mon Nov 15 22:23:26 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_failure.ML	Mon Nov 15 22:23:28 2010 +0100
@@ -10,7 +10,7 @@
     Counterexample of bool * term list |
     Time_Out |
     Out_Of_Memory |
-    Solver_Crashed of int |
+    Abnormal_Termination of int |
     Other_Failure of string
   val string_of_failure: Proof.context -> failure -> string
   exception SMT of failure
@@ -23,7 +23,7 @@
   Counterexample of bool * term list |
   Time_Out |
   Out_Of_Memory |
-  Solver_Crashed of int |
+  Abnormal_Termination of int |
   Other_Failure of string
 
 fun string_of_failure ctxt (Counterexample (real, ex)) =
@@ -38,8 +38,8 @@
       end
   | string_of_failure _ Time_Out = "Timed out"
   | string_of_failure _ Out_Of_Memory = "Ran out of memory"
-  | string_of_failure _ (Solver_Crashed err) =
-      "Solver crashed with error code " ^ string_of_int err
+  | string_of_failure _ (Abnormal_Termination err) =
+      "Solver terminated abnormally with error code " ^ string_of_int err
   | string_of_failure _ (Other_Failure msg) = msg
 
 exception SMT of failure
diff -r b57f7fee72ee -r 0125cbb5d3c7 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 22:23:26 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 22:23:28 2010 +0100
@@ -138,7 +138,7 @@
     val _ = C.trace_msg ctxt (pretty "Result:") ls
 
     val _ = null ls andalso return_code <> 0 andalso
-      raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
+      raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
   in ls end
 
 end
diff -r b57f7fee72ee -r 0125cbb5d3c7 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 22:23:26 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 22:23:28 2010 +0100
@@ -409,14 +409,14 @@
      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. *)
+(* "SMT_Failure.Abnormal_Termination" carries the solver's return code.
+   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 code) =
+  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
     if code >= 128 then Crashed else IncompleteUnprovable
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
@@ -469,7 +469,7 @@
             NONE => false
           | SOME (SMT_Failure.Counterexample _) => false
           | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
-          | SOME (SMT_Failure.Solver_Crashed code) =>
+          | SOME (SMT_Failure.Abnormal_Termination code) =>
             (if verbose then
                "The SMT solver invoked with " ^ string_of_int num_facts ^
                " fact" ^ plural_s num_facts ^ " terminated abnormally with \
@@ -512,7 +512,7 @@
                           command_call smtN (map fst used_facts)) ^
         minimize_line minimize_command (map fst used_facts)
       | SOME SMT_Failure.Time_Out => "Timed out."
-      | SOME (SMT_Failure.Solver_Crashed code) =>
+      | SOME (SMT_Failure.Abnormal_Termination code) =>
         "The SMT solver terminated abnormally with exit code " ^
         string_of_int code ^ "."
       | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."