# HG changeset patch
# User blanchet
# Date 1289851728 -3600
# Node ID e75614d0a85996ad255c6f8a69f13ed11d338e11
# Parent  d66403b60b3bca9b2153d55cb6ee43c300db4744
better error message

diff -r d66403b60b3b -r e75614d0a859 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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