# HG changeset patch
# User blanchet
# Date 1289148967 -3600
# Node ID 66c8c1f7e121f13e36bf0dcd099c14d3ed5a4219
# Parent  f2fbea1e5f9e1d4ea2f13d17441f195bda16d16b
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns

diff -r f2fbea1e5f9e -r 66c8c1f7e121 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 17:51:25 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 17:56:07 2010 +0100
@@ -420,8 +420,11 @@
 fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
   let
     val timer = Timer.startRealTimer ()
+    (* The "timeout" argument passed to "smt_filter" is a soft timeout. We make
+       it hard using "timeLimit". *)
     val {outcome, used_facts, run_time_in_msecs} =
-      SMT_Solver.smt_filter remote timeout state facts i
+      TimeLimit.timeLimit timeout
+                          (SMT_Solver.smt_filter remote timeout state facts) i
     val outcome0 = if is_none outcome0 then SOME outcome else outcome0
     val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
     val too_many_facts_perhaps =