src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

 val unix_failures =
   [(139, Crashed)]
 val smt_failures =
   remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
 
-val internal_error_prefix = "Internal error: "
-
 fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
     (case AList.lookup (op =) smt_failures code of
        SOME failure => failure
      | NONE => UnknownError ("Abnormal termination with exit code " ^
                              string_of_int code ^ "."))
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
-    if String.isPrefix internal_error_prefix msg then InternalError
-    else UnknownError msg
+    UnknownError msg
 
 (* FUDGE *)
 val smt_max_iters = Unsynchronized.ref 8
 val smt_iter_fact_frac = Unsynchronized.ref 0.5
 val smt_iter_time_frac = Unsynchronized.ref 0.5

           |> SMT_Solver.smt_filter_apply iter_timeout
           |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn => if Exn.is_interrupt exn then
                           reraise exn
                         else
-                          (internal_error_prefix ^ ML_Compiler.exn_message exn
+                          (ML_Compiler.exn_message exn
                            |> SMT_Failure.Other_Failure |> SOME, [])
         val death = Timer.checkRealTimer timer
         val _ =
           if verbose andalso is_some outcome then
             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)