# HG changeset patch
# User blanchet
# Date 1298280540 -3600
# Node ID adfd365c7ea4b63514cb618913b72f289bcfcb8c
# Parent  5acde4abb07b46afd35433c1067d3a92eff6135d
added a timeout around SMT preprocessing (notably monomorphization)

diff -r 5acde4abb07b -r adfd365c7ea4 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Feb 21 10:03:48 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Feb 21 10:29:00 2011 +0100
@@ -165,7 +165,8 @@
 val auto_max_relevant_divisor = 2
 
 fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
-                                 relevance_thresholds, max_relevant, ...})
+                                 relevance_thresholds, max_relevant, timeout,
+                                 ...})
                      auto i (relevance_override as {only, ...}) minimize_command
                      state =
   if null provers then
@@ -255,7 +256,8 @@
             val facts = get_facts "SMT solver" true smt_relevance_fudge smts
             val weight = SMT_Weighted_Fact oo weight_smt_fact thy
             fun smt_filter facts =
-              (if debug then curry (op o) SOME else try)
+              (if debug then curry (op o) SOME
+               else TimeLimit.timeLimit timeout o try)
                   (SMT_Solver.smt_filter_preprocess state (facts ()))
           in
             smts |> map (`(class_of_smt_solver ctxt))