# 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 *)