# HG changeset patch
# User blanchet
# Date 1236440856 -3600
# Node ID 110826d1e5ffc6b7eadafa0056defb7756b0dd08
# Parent  5598523c482ac83e6ac2ce28866445b2b1a5398b
Added a second timeout mechanism to Refute.
For some reason, TimeLimit.timeLimit often does not work, and it
leaves Refute running forever, making any evaluation using
Mutabelle or Mirabelle impossible. The redundant timeout seems to
do the trick.

diff -r 5598523c482a -r 110826d1e5ff src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Mar 07 12:27:26 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Mar 07 16:47:36 2009 +0100
@@ -1165,6 +1165,7 @@
     (* unit -> unit *)
     fun wrapper () =
     let
+      val timer  = Timer.startRealTimer ()
       val u      = unfold_defs thy t
       val _      = Output.tracing ("Unfolded term: " ^
                                    Syntax.string_of_term_global thy u)
@@ -1201,6 +1202,9 @@
       (* (Term.typ * int) list -> string *)
       fun find_model_loop universe =
       let
+        val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
+        val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
+                orelse raise TimeLimit.TimeOut
         val init_model = (universe, [])
         val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
           bounds = [], wellformed = True}