src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 41268 56b7e277fd7d
parent 41266 b6b77c963f11
child 41274 6a9306c427b9
equal deleted inserted replaced
41267:958fee9ec275 41268:56b7e277fd7d
   417     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
   417     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
   418     val (prover_name, prover) = get_prover (Proof.context_of st) args
   418     val (prover_name, prover) = get_prover (Proof.context_of st) args
   419     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
   419     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
   420     val dir = AList.lookup (op =) args keepK
   420     val dir = AList.lookup (op =) args keepK
   421     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
   421     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
   422     val hard_timeout = SOME timeout (* always use a hard timeout *)
   422     (* always use a hard timeout, but give some slack so that the automatic
       
   423        minimizer has a chance to do its magic *)
       
   424     val hard_timeout = SOME (2 * timeout)
   423     val (msg, result) =
   425     val (msg, result) =
   424       run_sh prover_name prover type_sys hard_timeout timeout dir st
   426       run_sh prover_name prover type_sys hard_timeout timeout dir st
   425   in
   427   in
   426     case result of
   428     case result of
   427       SH_OK (time_isa, time_prover, names) =>
   429       SH_OK (time_isa, time_prover, names) =>