src/HOL/Tools/SMT/smt_solver.ML

   (*options*)
   val oracle: bool Config.T
   val filter_only: bool Config.T
   val datatypes: bool Config.T
   val keep_assms: bool Config.T
-  val timeout: int Config.T
+  val timeout: real Config.T
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
   val traceN: string
   val trace: bool Config.T
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val trace_used_facts: bool Config.T

 val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
 
 val (keep_assms, setup_keep_assms) =
   Attrib.config_bool "smt_keep_assms" (K true)
 
-val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
+val (timeout, setup_timeout) = Attrib.config_real "smt_timeout" (K 30.0)
 
 fun with_timeout ctxt f x =
-  TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
+  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
   handle TimeLimit.TimeOut => raise SMT Time_Out
 
 val traceN = "smt_trace"
 val (trace, setup_trace) = Attrib.config_bool traceN (K false)
 

 
 fun invoke translate_config name cmd more_opts options irules ctxt =
   let
     val args = more_opts @ options ctxt
     val comments = ("solver: " ^ name) ::
-      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
+      ("timeout: " ^ Time.toString (seconds (Config.get ctxt timeout))) ::
       "arguments:" :: args
   in
     irules
     |> tap (trace_assms ctxt)
     |> SMT_Translate.translate translate_config ctxt comments

 fun smt_filter run_remote time_limit st xrules i =
   let
     val {facts, goal, ...} = Proof.goal st
     val ctxt =
       Proof.context_of st
-      |> Config.put timeout (Time.toSeconds time_limit)
+      |> Config.put timeout (Real.fromInt (Time.toSeconds time_limit))
       |> Config.put oracle false
       |> Config.put filter_only true
       |> Config.put keep_assms false
     val cprop =
       Thm.cprem_of goal i

     "Applies an SMT solver to the current goal."
 
 
 fun print_setup context =
   let
-    val t = string_of_int (Config.get_generic context timeout)
+    val t = Time.toString (seconds (Config.get_generic context timeout))
     val names = sort_strings (all_solver_names_of context)
     val ns = if null names then [no_solver] else names
     val n = solver_name_of context
     val opts =
       (case Symtab.lookup (Solvers.get context) n of