src/HOL/Tools/Sledgehammer/sledgehammer.ML

   in
     {outcome = outcome, message = message, used_facts = used_facts,
      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
 
 val smt_max_iter = 8

         val too_many_facts_perhaps =
           case outcome of
             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 \
                \exit code " ^ string_of_int code ^ "."
                |> (if debug then error else warning)

         try_command_line (proof_banner auto)
                          (apply_on_subgoal subgoal subgoal_count ^
                           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."
       | SOME failure =>
         SMT_Failure.string_of_failure ctxt failure