src/HOL/Tools/SMT/smt_solver.ML

     val _ = trace_msg ctxt (pretty "SMT result:") ls
   in ls end
 
 end
 
+fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o
+  Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd))
+
 fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
   let
     fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
     fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
     fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)

     val comments = ("solver: " ^ name) ::
       ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
       "arguments:" :: args
   in
     irules
+    |> tap (trace_assms ctxt)
     |> SMT_Translate.translate translate_config ctxt comments
     ||> tap (trace_recon_data ctxt)
     |>> run_solver ctxt cmd args
     |> rpair ctxt
   end