# HG changeset patch
# User blanchet
# Date 1291627889 -3600
# Node ID e3ee5bbeb06e8ccbcbe611411f01e073e2a0db11
# Parent  79d2ea0e1fdbd695970e297cf3bd5ed49f27f294
trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases

diff -r 79d2ea0e1fdb -r e3ee5bbeb06e src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 10:23:31 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 06 10:31:29 2010 +0100
@@ -480,11 +480,7 @@
           else
             ()
         val {outcome, used_facts, run_time_in_msecs} =
-          TimeLimit.timeLimit iter_timeout
-              (SMT_Solver.smt_filter remote iter_timeout state facts) i
-          handle TimeLimit.TimeOut =>
-                 {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
-                  run_time_in_msecs = NONE}
+          SMT_Solver.smt_filter remote iter_timeout state facts i
         val _ =
           if verbose andalso is_some outcome then
             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)