# HG changeset patch
# User blanchet
# Date 1344941666 -7200
# Node ID e653853365316bfc906a318b40bc5e86eca05765
# Parent  0f94b8b69e790e1b4d54a9aff114a7c6ee338c17
recognize bus errors as crash

diff -r 0f94b8b69e79 -r e65385336531 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 12:49:42 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 12:54:26 2012 +0200
@@ -906,7 +906,8 @@
    (103, MalformedInput),
    (110, MalformedInput)]
 val unix_failures =
-  [(139, Crashed)]
+  [(138, Crashed),
+   (139, Crashed)]
 val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
 
 fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =