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 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 (filter_only, setup_filter_only) =
   Attrib.config_bool "smt_filter_only" (K false)
 
 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)
 
 fun with_timeout ctxt f x =
   TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x

       info
     val {extra_norm, translate} = interface
     val (with_datatypes, translate') =
       set_has_datatypes (Config.get ctxt datatypes) translate
     val cmd = (rm, env_var, is_remote, name)
+    val keep = Config.get ctxt keep_assms
   in
     (irules, ctxt)
-    |-> SMT_Normalize.normalize extra_norm with_datatypes
+    |-> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes
     |-> invoke translate' name cmd more_options options
     |-> reconstruct
     |-> (fn (idxs, thm) => fn ctxt' => thm
     |> singleton (ProofContext.export ctxt' ctxt)
     |> discharge_definitions

     val ctxt =
       Proof.context_of st
       |> Config.put timeout (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
       |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt
       |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
     val irs = map (pair ~1) (Thm.assume cprop :: facts)

       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration" #>
   setup_oracle #>
   setup_filter_only #>
   setup_datatypes #>
+  setup_keep_assms #>
   setup_timeout #>
   setup_trace #>
   setup_trace_used_facts #>
   setup_fixed_certificates #>
   Attrib.setup @{binding smt_certificates}