src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
                        else
                          I)
                   |>> (if measure_run_time then split_time else rpair NONE)
                 val (tstplike_proof, outcome) =
-                  extract_tstplike_proof_and_outcome complete res_code
+                  extract_tstplike_proof_and_outcome verbose complete res_code
                       proof_delims known_failures output
               in (output, msecs, tstplike_proof, outcome) end
             val readable_names = debug andalso overlord
             val (atp_problem, pool, conjecture_offset, fact_names) =
               prepare_atp_problem ctxt readable_names explicit_forall type_sys

 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)
+     | 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
+    else 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