# HG changeset patch
# User boehmes
# Date 1288107352 -7200
# Node ID 8d470bbaafd791a6e90103c7b7e686d2e2e0396f
# Parent  d99f74ed95bee5450102e7586525f7bd298feff1
trace assumptions before giving them to the SMT solver

diff -r d99f74ed95be -r 8d470bbaafd7 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 17:35:51 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 17:35:52 2010 +0200
@@ -228,6 +228,9 @@
 
 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]
@@ -247,6 +250,7 @@
       "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