Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorboehmes
Mon, 15 Nov 2010 22:24:08 +0100
changeset 40562 bbcb7aa90afc
parent 40561 0125cbb5d3c7 (current diff)
parent 40559 9597b93a8c00 (diff)
child 40563 1e218365a20e
merged
src/HOL/Tools/Sledgehammer/sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 22:23:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 22:24:08 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 *)
isabelle