--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 18:58:30 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 21:08:48 2010 +0100
@@ -512,6 +512,9 @@
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) =>
+ "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