# HG changeset patch
# User blanchet
# Date 1288821690 -3600
# Node ID df25b51af0134b259a27255793d7ba534cb116e4
# Parent  4521d56aef63553721602f87a50fe2c430bb50b6
give E one more second, to prevent cases where it finds a proof but has no time to print it

diff -r 4521d56aef63 -r df25b51af013 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Nov 03 22:51:32 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Nov 03 23:01:30 2010 +0100
@@ -80,15 +80,16 @@
 
 (* E *)
 
-(* Give older versions of E an extra second, because the "eproof" script wrongly
-   subtracted an entire second to account for the overhead of the script
-   itself, which is in fact much lower. *)
+(* Give E an extra second to reconstruct the proof. Older versions even get two
+   seconds, because the "eproof" script wrongly subtracted an entire second to
+   account for the overhead of the script itself, which is in fact much
+   lower. *)
 fun e_bonus () =
   case getenv "E_VERSION" of
-    "" => 1000
+    "" => 2000
   | version =>
-    if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000
-    else 0
+    if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 2000
+    else 1000
 
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")