# HG changeset patch
# User blanchet
# Date 1292576164 -3600
# Node ID def0a3013554343843c577a46a3db550da435dbf
# Parent  f9783376d9b1362ce03f04265b2ff395f6d78e92
trap one more Z3 error

diff -r f9783376d9b1 -r def0a3013554 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 00:27:40 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 09:56:04 2010 +0100
@@ -442,7 +442,8 @@
    (12, InternalError),
    (13, InternalError)]
 val z3_failures =
-  [(103, MalformedInput),
+  [(101, OutOfResources),
+   (103, MalformedInput),
    (110, MalformedInput)]
 val unix_failures =
   [(139, Crashed)]