# HG changeset patch
# User blanchet
# Date 1289855281 -3600
# Node ID 9597b93a8c00ae77dd1936434b755d1b0e5eb420
# Parent  e75614d0a85996ad255c6f8a69f13ed11d338e11
better error message

diff -r e75614d0a859 -r 9597b93a8c00 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 21:08:48 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 22:08:01 2010 +0100
@@ -516,6 +516,7 @@
         "The SMT solver terminated abnormally with exit code " ^
         string_of_int code ^ "."
       | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
+      | SOME SMT_Failure.Out_Of_Memory => "The SMT solver ran out of memory."
       | SOME failure =>
         SMT_Failure.string_of_failure ctxt failure
     val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)