src/HOL/Tools/SMT/smt_solver.ML
changeset 41121 5c5d05963f93
parent 41065 13424972ade4
child 41124 1de17a2de5ad
equal deleted inserted replaced
41119:573f557ed716 41121:5c5d05963f93
   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: " ^ string_of_real (Config.get ctxt C.timeout)) ::
   183       ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
       
   184       ("random seed: " ^ string_of_int (Config.get ctxt C.random_seed)) ::
   184       "arguments:" :: args
   185       "arguments:" :: args
   185   in
   186   in
   186     irules
   187     irules
   187     |> tap (trace_assms ctxt)
   188     |> tap (trace_assms ctxt)
   188     |> SMT_Translate.translate translate_config ctxt comments
   189     |> SMT_Translate.translate translate_config ctxt comments