# HG changeset patch
# User blanchet
# Date 1314177453 -7200
# Node ID 5e19eecb0e1c10d0f2f2318f5ac582dcda4a27ba
# Parent  5d0754cf994a7c688f72247020b103a9717dd449
specify timeout for "sledgehammer_tac"

diff -r 5d0754cf994a -r 5e19eecb0e1c src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 24 11:17:33 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Aug 24 11:17:33 2011 +0200
@@ -550,19 +550,21 @@
   end
 
 
-val e_override_params =
+fun e_override_params timeout =
   [("provers", "e"),
    ("max_relevant", "0"),
    ("type_enc", "poly_guards?"),
    ("sound", "true"),
-   ("slicing", "false")]
+   ("slicing", "false"),
+   ("timeout", timeout |> Time.toSeconds |> string_of_int)]
 
-val vampire_override_params =
+fun vampire_override_params timeout =
   [("provers", "vampire"),
    ("max_relevant", "0"),
    ("type_enc", "poly_tags"),
    ("sound", "true"),
-   ("slicing", "false")]
+   ("slicing", "false"),
+   ("timeout", timeout |> Time.toSeconds |> string_of_int)]
 
 fun run_reconstructor trivial full m name reconstructor named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
@@ -572,10 +574,10 @@
          (fn ctxt => fn thms =>
             Method.insert_tac thms THEN'
             (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-                 e_override_params
+                 (e_override_params timeout)
              ORELSE'
              Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-                 vampire_override_params))
+                 (vampire_override_params timeout)))
        else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
        else if full orelse !reconstructor = "metis (full_types)" then