distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job

--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu May 19 10:24:13 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu May 19 10:24:13 2011 +0200
@@ -324,10 +324,10 @@
 \item[$\bullet$] \textbf{\textit{provers}} specifies the ATP and SMT solvers to
 use (e.g., ``\textit{provers} = \textit{e spass remote\_vampire}'').
 
-\item[$\bullet$] \textbf{\textit{timeout}} controls the time limit. It is set to
-30 seconds, but since Sledgehammer runs asynchronously you should not hesitate
-to crank up this limit to 60 or 120 seconds if you are the kind of user who can
-think clearly while ATPs are active.
+\item[$\bullet$] \textbf{\textit{timeout}} controls the provers' time limit. It
+is set to 30 seconds, but since Sledgehammer runs asynchronously you should not
+hesitate to raise this limit to 60 or 120 seconds if you are the kind of user
+who can think clearly while ATPs are active.
 
 \item[$\bullet$] \textbf{\textit{full\_types}} specifies whether type-sound
 encodings should be used. By default, Sledgehammer employs a mixture of
@@ -428,6 +428,10 @@
 %      to re-find by Metis
 %    * but the opposite is sometimes the case
 
+% Why is Sledgehammer automatically minimizing sometimes?
+%       * some provers (e.g. CVC3 and Yices)
+%       * also, sometimes E finds a proof but doesn't give a proof object
+
 \point{I got a strange error from Sledgehammer---what should I do?}
 
 Sledgehammer tries to give informative error messages. Please report any strange
@@ -678,9 +682,10 @@
 
 \opdefault{timeout}{float\_or\_none}{\upshape 30}
 Specifies the maximum number of seconds that the automatic provers should spend
-searching for a proof. For historical reasons, the default value of this option
-can be overridden using the option ``Sledgehammer: Time Limit'' from the
-``Isabelle'' menu in Proof General.
+searching for a proof. This excludes problem preparation and is a soft limit.
+For historical reasons, the default value of this option can be overridden using
+the option ``Sledgehammer: Time Limit'' from the ``Isabelle'' menu in Proof
+General.
 
 \opfalse{blocking}{non\_blocking}
 Specifies whether the \textbf{sledgehammer} command should operate

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu May 19 10:24:13 2011 +0200
@@ -92,8 +92,9 @@
         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
   let
     val ctxt = Proof.context_of state
+    val hard_timeout = Time.+ (timeout, timeout)
     val birth_time = Time.now ()
-    val death_time = Time.+ (birth_time, timeout)
+    val death_time = Time.+ (birth_time, hard_timeout)
     val max_relevant =
       max_relevant
       |> the_default (default_max_relevant_for_prover ctxt slicing name)
@@ -143,7 +144,7 @@
                             Pretty.mark Markup.hilite (Pretty.str message)]))
       end
     else if blocking then
-      let val (success, message) = TimeLimit.timeLimit timeout go () in
+      let val (success, message) = TimeLimit.timeLimit hard_timeout go () in
         List.app Output.urgent_message
                  (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
         (success, state)