src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

         )
     | NONE => log (minimize_tag id ^ "failed: " ^ msg)
   end
 
 
-val e_override_params =
+fun e_override_params timeout =
   [("provers", "e"),
    ("max_relevant", "0"),
    ("type_enc", "poly_guards?"),
    ("sound", "true"),
-   ("slicing", "false")]
-
-val vampire_override_params =
+   ("slicing", "false"),
+   ("timeout", timeout |> Time.toSeconds |> string_of_int)]
+
+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) =
   let
     fun do_reconstructor thms ctxt =
       (if !reconstructor = "sledgehammer_tac" then
          (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
          Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
        else if !reconstructor = "metis (no_types)" then