src/HOL/Tools/SMT/smt_solver.ML
changeset 41062 304cfdbc6475
parent 41059 d2b1fc1b8e19
child 41065 13424972ade4
equal deleted inserted replaced
41061:492f8fd35fc0 41062:304cfdbc6475
   178 
   178 
   179 fun invoke translate_config name cmd options irules ctxt =
   179 fun invoke translate_config name cmd options irules ctxt =
   180   let
   180   let
   181     val args = C.solver_options_of ctxt @ options ctxt
   181     val args = C.solver_options_of ctxt @ options ctxt
   182     val comments = ("solver: " ^ name) ::
   182     val comments = ("solver: " ^ name) ::
   183       ("timeout: " ^ Time.toString (seconds (Config.get ctxt C.timeout))) ::
   183       ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
   184       "arguments:" :: args
   184       "arguments:" :: args
   185   in
   185   in
   186     irules
   186     irules
   187     |> tap (trace_assms ctxt)
   187     |> tap (trace_assms ctxt)
   188     |> SMT_Translate.translate translate_config ctxt comments
   188     |> SMT_Translate.translate translate_config ctxt comments