# HG changeset patch
# User blanchet
# Date 1282655207 -7200
# Node ID fe5929dacd439b1242b0da95f175bc96df50803c
# Parent  38a926e033ad584b325c24e7bc8633a397c2a313
use a soft time limit for E
with a hard limit, "eproof"/"eproof.pl" doesn't show the proof is there's less than 1 second left, yielding "the ATP output is malformed"

diff -r 38a926e033ad -r fe5929dacd43 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 14:36:29 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 15:06:47 2010 +0200
@@ -136,7 +136,8 @@
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
-     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
+     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
+     \--soft-cpu-limit=" ^
      string_of_int (to_generous_secs timeout),
    has_incomplete_mode = false,
    proof_delims = [tstp_proof_delims],