diff --git a/src/HOL/Library/Tools/smt_word.ML b/src/HOL/Library/Tools/smt_word.ML
--- a/src/HOL/Library/Tools/smt_word.ML
+++ b/src/HOL/Library/Tools/smt_word.ML
@@ -1,167 +1,170 @@
 (*  Title:      HOL/Word/Tools/smt_word.ML
     Author:     Sascha Boehme, TU Muenchen
 
 SMT setup for words.
 *)
 
 signature SMT_WORD =
 sig
   val add_word_shift': term * string -> Context.generic -> Context.generic
 end
 
 structure SMT_Word : SMT_WORD =
 struct
 
 open Word_Lib
 
 
 (* SMT-LIB logic *)
 
 (* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers.
    Better set the logic to "" and make at least Z3 happy. *)
-fun smtlib_logic ts =
-  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
+fun smtlib_logic "z3" ts =
+    if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
+  | smtlib_logic "verit" _ = NONE
+  | smtlib_logic _ ts =
+    if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "AUFBVLIRA" else NONE
 
 
 (* SMT-LIB builtins *)
 
 local
-  val smtlibC = SMTLIB_Interface.smtlibC
+  val smtlibC = SMTLIB_Interface.smtlibC @ SMTLIB_Interface.bvsmlibC
 
   val wordT = \<^typ>\<open>'a::len word\<close>
 
   fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
   fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
 
   fun word_typ (Type (\<^type_name>\<open>word\<close>, [T])) =
       Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
     | word_typ _ = NONE
 
   (*CVC4 does not support "_bvk T" when k does not fit in the BV of size T, so remove the bits that
    will be ignored according to the SMT-LIB*)
   fun word_num (Type (\<^type_name>\<open>word\<close>, [T])) k =
         let
           val size = try dest_binT T
           fun max_int size = Integer.pow size 2
         in
           (case size of
             NONE => NONE
           | SOME size => SOME (index1 ("bv" ^ string_of_int (Int.rem(k, max_int size))) size))
         end
     | word_num _ _ = NONE
 
   fun if_fixed pred m n T ts =
     let val (Us, U) = Term.strip_type T
     in
       if pred (U, Us) then SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) else NONE
     end
 
   fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
   fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
 
   fun add_word_fun f (t, n) =
     let val (m, _) = Term.dest_Const t
     in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
 
   val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
 
   fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t
     | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
 
   fun shift m n T ts =
     let val U = Term.domain_type (Term.range_type T)
     in
       (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
         (true, SOME i) =>
           SOME (n, 2, [hd (tl ts), HOLogic.mk_number U i], mk_shift (m, T))
       | _ => NONE)   (* FIXME: also support non-numerical shifts *)
     end
 
   fun mk_shift' c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
     | mk_shift' c ts = raise TERM ("bad arguments", Const c :: ts)
 
   fun shift' m n T ts =
     let val U = Term.domain_type T
     in
       (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
         (true, SOME i) =>
           SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift' (m, T))
       | _ => NONE)   (* FIXME: also support non-numerical shifts *)
     end
 
   fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
 
   fun extract m n T ts =
     let val U = Term.range_type (Term.range_type T)
     in
       (case (try (snd o HOLogic.dest_number o hd) ts, try dest_wordT U) of
         (SOME lb, SOME i) =>
           SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
       | _ => NONE)
     end
 
   fun mk_extend c ts = Term.list_comb (Const c, ts)
 
   fun extend m n T ts =
     let val (U1, U2) = Term.dest_funT T
     in
       (case (try dest_wordT U1, try dest_wordT U2) of
         (SOME i, SOME j) =>
           if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
           else NONE
       | _ => NONE)
     end
 
   fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
 
   fun rotate m n T ts =
     let val U = Term.domain_type (Term.range_type T)
     in
       (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
         (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
       | _ => NONE)
     end
 in
 
 val setup_builtins =
   SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
   fold (add_word_fun if_fixed_all) [
     (\<^term>\<open>uminus :: 'a::len word \<Rightarrow> _\<close>, "bvneg"),
     (\<^term>\<open>plus :: 'a::len word \<Rightarrow> _\<close>, "bvadd"),
     (\<^term>\<open>minus :: 'a::len word \<Rightarrow> _\<close>, "bvsub"),
     (\<^term>\<open>times :: 'a::len word \<Rightarrow> _\<close>, "bvmul"),
     (\<^term>\<open>not :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
     (\<^term>\<open>and :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
     (\<^term>\<open>or :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
     (\<^term>\<open>xor :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
     (\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
   fold (add_word_fun shift) [
     (\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
     (\<^term>\<open>drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
     (\<^term>\<open>signed_drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
   add_word_fun extract
     (\<^term>\<open>slice :: _ \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "extract") #>
   fold (add_word_fun extend) [
     (\<^term>\<open>ucast :: 'a::len word \<Rightarrow> _\<close>, "zero_extend"),
     (\<^term>\<open>scast :: 'a::len word \<Rightarrow> _\<close>, "sign_extend") ] #>
   fold (add_word_fun rotate) [
     (\<^term>\<open>word_rotl\<close>, "rotate_left"),
     (\<^term>\<open>word_rotr\<close>, "rotate_right") ] #>
   fold (add_word_fun if_fixed_args) [
     (\<^term>\<open>less :: 'a::len word \<Rightarrow> _\<close>, "bvult"),
     (\<^term>\<open>less_eq :: 'a::len word \<Rightarrow> _\<close>, "bvule"),
     (\<^term>\<open>word_sless\<close>, "bvslt"),
     (\<^term>\<open>word_sle\<close>, "bvsle") ]
 
 val add_word_shift' = add_word_fun shift'
 
 end
 
 
 (* setup *)
 
 val _ = Theory.setup (Context.theory_map (
   SMTLIB_Interface.add_logic (20, smtlib_logic) #>
   setup_builtins))
 
 end;
diff --git a/src/HOL/Tools/SMT/cvc4_interface.ML b/src/HOL/Tools/SMT/cvc4_interface.ML
--- a/src/HOL/Tools/SMT/cvc4_interface.ML
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML
@@ -1,37 +1,37 @@
 (*  Title:      HOL/Tools/SMT/cvc4_interface.ML
     Author:     Jasmin Blanchette, TU Muenchen
 
 Interface to CVC4 based on an extended version of SMT-LIB.
 *)
 
 signature CVC4_INTERFACE =
 sig
   val smtlib_cvc4C: SMT_Util.class
   val hosmtlib_cvc4C: SMT_Util.class
 end;
 
 structure CVC4_Interface: CVC4_INTERFACE =
 struct
 
 val cvc4C = ["cvc4"]
 val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
 val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
 
 
 (* interface *)
 
 local
   fun translate_config order ctxt =
     {order = order,
-     logic = K "(set-logic ALL_SUPPORTED)\n",
+     logic = K (K "(set-logic ALL_SUPPORTED)\n"),
      fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
      serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
 in
 
 val _ = Theory.setup (Context.theory_map
   (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
    SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
 
 end
 
 end;
diff --git a/src/HOL/Tools/SMT/smt_config.ML b/src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML
+++ b/src/HOL/Tools/SMT/smt_config.ML
@@ -1,291 +1,293 @@
 (*  Title:      HOL/Tools/SMT/smt_config.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Configuration options and diagnostic tools for SMT.
 *)
 
 signature SMT_CONFIG =
 sig
   (*solver*)
   type solver_info = {
     name: string,
     class: Proof.context -> SMT_Util.class,
     avail: unit -> bool,
     options: Proof.context -> string list }
   val add_solver: solver_info -> Context.generic -> Context.generic
   val set_solver_options: string * string -> Context.generic -> Context.generic
   val is_available: Proof.context -> string -> bool
   val available_solvers_of: Proof.context -> string list
   val select_solver: string -> Context.generic -> Context.generic
   val solver_of: Proof.context -> string
   val solver_class_of: Proof.context -> SMT_Util.class
   val solver_options_of: Proof.context -> string list
 
   (*options*)
   val oracle: bool Config.T
   val timeout: real Config.T
   val reconstruction_step_timeout: real Config.T
   val random_seed: int Config.T
   val read_only_certificates: bool Config.T
   val verbose: bool Config.T
   val trace: bool Config.T
   val statistics: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
   val explicit_application: int Config.T
   val higher_order: bool Config.T
+  val native_bv: bool Config.T
   val nat_as_int: bool Config.T
   val infer_triggers: bool Config.T
   val debug_files: string Config.T
   val sat_solver: string Config.T
   val compress_verit_proofs: Proof.context -> bool
 
   (*tools*)
   val get_timeout: Proof.context -> Time.time option
   val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
 
   (*diagnostics*)
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val verit_msg: Proof.context -> (unit -> 'a) -> unit
   val verit_arith_msg: Proof.context -> (unit -> 'a) -> unit
   val spy_verit: Proof.context -> bool
   val spy_Z3: Proof.context -> bool
 
   (*certificates*)
   val select_certificates: string -> Context.generic -> Context.generic
   val certificates_of: Proof.context -> Cache_IO.cache option
 
   (*setup*)
   val print_setup: Proof.context -> unit
 end;
 
 structure SMT_Config: SMT_CONFIG =
 struct
 
 (* solver *)
 
 type solver_info = {
   name: string,
   class: Proof.context -> SMT_Util.class,
   avail: unit -> bool,
   options: Proof.context -> string list}
 
 type data = {
   solvers: (solver_info * string list) Symtab.table,
   solver: string option,
   certs: Cache_IO.cache option}
 
 fun mk_data solvers solver certs: data = {solvers=solvers, solver=solver, certs=certs}
 
 val empty_data = mk_data Symtab.empty NONE NONE
 
 fun solvers_of ({solvers, ...}: data) = solvers
 fun solver_of ({solver, ...}: data) = solver
 fun certs_of ({certs, ...}: data) = certs
 
 fun map_solvers f ({solvers, solver, certs}: data) = mk_data (f solvers) solver certs
 fun map_solver f ({solvers, solver, certs}: data) = mk_data solvers (f solver) certs
 fun put_certs c ({solvers, solver, ...}: data) = mk_data solvers solver c
 
 fun merge_data ({solvers=ss1,solver=s1,certs=c1}: data, {solvers=ss2,solver=s2,certs=c2}: data) =
   mk_data (Symtab.merge (K true) (ss1, ss2)) (merge_options (s1, s2)) (merge_options (c1, c2))
 
 structure Data = Generic_Data
 (
   type T = data
   val empty = empty_data
   val merge = merge_data
 )
 
 fun set_solver_options (name, options) =
   let val opts = String.tokens (Symbol.is_ascii_blank o str) options
   in Data.map (map_solvers (Symtab.map_entry name (apsnd (K opts)))) end
 
 fun add_solver (info as {name, ...} : solver_info) context =
   if Symtab.defined (solvers_of (Data.get context)) name then
     error ("Solver already registered: " ^ quote name)
   else
     context
     |> Data.map (map_solvers (Symtab.update (name, (info, []))))
     |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
         (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
         ("additional command line options for SMT solver " ^ quote name))
 
 fun all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt)))
 
 fun solver_name_of ctxt = solver_of (Data.get (Context.Proof ctxt))
 
 fun is_available ctxt name =
   (case Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name of
     SOME ({avail, ...}, _) => avail ()
   | NONE => false)
 
 fun available_solvers_of ctxt =
   filter (is_available ctxt) (all_solvers_of ctxt)
 
 fun warn_solver (Context.Proof ctxt) name =
       if Context_Position.is_visible ctxt then
         warning ("The SMT solver " ^ quote name ^ " is not installed")
       else ()
   | warn_solver _ _ = ()
 
 fun select_solver name context =
   let
     val ctxt = Context.proof_of context
     val upd = Data.map (map_solver (K (SOME name)))
   in
     if not (member (op =) (all_solvers_of ctxt) name) then
       error ("Trying to select unknown solver: " ^ quote name)
     else if not (is_available ctxt name) then
       (warn_solver context name; upd context)
     else upd context
   end
 
 fun no_solver_err () = error "No SMT solver selected"
 
 fun solver_of ctxt =
   (case solver_name_of ctxt of
     SOME name => name
   | NONE => no_solver_err ())
 
 fun solver_info_of default select ctxt =
   (case solver_name_of ctxt of
     NONE => default ()
   | SOME name => select (Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name))
 
 fun solver_class_of ctxt =
   let fun class_of ({class, ...}: solver_info, _) = class ctxt
   in solver_info_of no_solver_err (class_of o the) ctxt end
 
 fun solver_options_of ctxt =
   let
     fun all_options NONE = []
       | all_options (SOME ({options, ...} : solver_info, opts)) =
           opts @ options ctxt
   in solver_info_of (K []) all_options ctxt end
 
 val setup_solver =
   Attrib.setup \<^binding>\<open>smt_solver\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration"
 
 
 (* options *)
 
 val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true)
 val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 0.0)
 val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0)
 val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1)
 val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
 val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
 val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
 val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
 val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false)
 val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false)
 val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false)
 val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true)
 val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
 val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
 val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
 val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
 val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
+val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true)
 val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
 val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
 val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
 val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite")
 
 
 (* diagnostics *)
 
 fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
 
 fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
 fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
 fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
 
 fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ()
 fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ()
 
 fun spy_verit ctxt  = Config.get ctxt spy_verit_attr
 fun spy_Z3 ctxt  = Config.get ctxt spy_z3
 fun compress_verit_proofs ctxt  = Config.get ctxt trace_verit_compression
 
 
 (* tools *)
 
 fun get_timeout ctxt =
   let val t = seconds (Config.get ctxt timeout);
   in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end;
 
 fun with_time_limit ctxt timeout_config f x =
   Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
     handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
 
 fun with_timeout ctxt = with_time_limit ctxt timeout
 
 
 (* certificates *)
 
 val certificates_of = certs_of o Data.get o Context.Proof
 
 val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of
 
 fun select_certificates name context = context |> Data.map (put_certs (
   if name = "" then NONE
   else
     (Resources.master_directory (Context.theory_of context) + Path.explode name)
     |> SOME o Cache_IO.unsynchronized_init))
 
 val setup_certificates =
   Attrib.setup \<^binding>\<open>smt_certificates\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
     "SMT certificates configuration"
 
 
 (* setup *)
 
 val _ = Theory.setup (
   setup_solver #>
   setup_certificates)
 
 fun print_setup ctxt =
   let
     fun string_of_bool b = if b then "true" else "false"
 
     val names = available_solvers_of ctxt
     val ns = if null names then ["(none)"] else sort_strings names
     val n = the_default "(none)" (solver_name_of ctxt)
     val opts = solver_options_of ctxt
 
     val t = string_of_real (Config.get ctxt timeout)
 
     val certs_filename =
       (case get_certificates_path ctxt of
         SOME path => Path.print path
       | NONE => "(disabled)")
   in
     Pretty.writeln (Pretty.big_list "SMT setup:" [
       Pretty.str ("Current SMT solver: " ^ n),
       Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
       Pretty.str_list "Available SMT solvers: "  "" ns,
       Pretty.str ("Current timeout: " ^ t ^ " seconds"),
       Pretty.str ("With proofs: " ^
         string_of_bool (not (Config.get ctxt oracle))),
       Pretty.str ("Certificates cache: " ^ certs_filename),
       Pretty.str ("Fixed certificates: " ^
         string_of_bool (Config.get ctxt read_only_certificates))])
   end
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close>
     "show the available SMT solvers, the currently selected SMT solver, \
     \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
 
 end;
diff --git a/src/HOL/Tools/SMT/smt_real.ML b/src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML
+++ b/src/HOL/Tools/SMT/smt_real.ML
@@ -1,115 +1,115 @@
 (*  Title:      HOL/Tools/SMT/smt_real.ML
     Author:     Sascha Boehme, TU Muenchen
 
 SMT setup for reals.
 *)
 
 structure SMT_Real: sig end =
 struct
 
 
 (* SMT-LIB logic *)
 
-fun smtlib_logic ts =
+fun smtlib_logic _ ts =
   if exists (Term.exists_type (Term.exists_subtype (equal \<^typ>\<open>real\<close>))) ts
   then SOME "AUFLIRA"
   else NONE
 
 
 (* SMT-LIB and Z3 built-ins *)
 
 local
   fun real_num _ i = SOME (string_of_int i ^ ".0")
 
   fun is_linear [t] = SMT_Util.is_number t
     | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
     | is_linear _ = false
 
   fun mk_times ts = Term.list_comb (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, ts)
 
   fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
 in
 
 val setup_builtins =
   SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
     (\<^typ>\<open>real\<close>, K (SOME ("Real", [])), real_num) #>
   fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
     (\<^Const>\<open>less \<^Type>\<open>real\<close>\<close>, "<"),
     (\<^Const>\<open>less_eq \<^Type>\<open>real\<close>\<close>, "<="),
     (\<^Const>\<open>uminus \<^Type>\<open>real\<close>\<close>, "-"),
     (\<^Const>\<open>plus \<^Type>\<open>real\<close>\<close>, "+"),
     (\<^Const>\<open>minus \<^Type>\<open>real\<close>\<close>, "-") ] #>
   SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
     (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, times) #>
   SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
     (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, "*") #>
   SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
     (\<^Const>\<open>divide \<^Type>\<open>real\<close>\<close>, "/")
 
 end
 
 
 (* Z3 constructors *)
 
 local
   fun z3_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME \<^typ>\<open>real\<close>
     | z3_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME \<^typ>\<open>real\<close>
         (*FIXME: delete*)
     | z3_mk_builtin_typ _ = NONE
 
   fun z3_mk_builtin_num _ i T =
     if T = \<^typ>\<open>real\<close> then SOME (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> i)
     else NONE
 
   fun mk_nary _ cu [] = cu
     | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
 
   val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
   val add = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
   val real0 = Numeral.mk_cnumber \<^ctyp>\<open>real\<close> 0
   val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
   val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
   val mk_div = Thm.mk_binop \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
   val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: real \<Rightarrow> _\<close>
   val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: real \<Rightarrow> _\<close>
 
   fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
     | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)
     | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
     | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
     | z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
     | z3_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
     | z3_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
     | z3_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
     | z3_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
     | z3_mk_builtin_fun _ _ = NONE
 in
 
 val z3_mk_builtins = {
   mk_builtin_typ = z3_mk_builtin_typ,
   mk_builtin_num = z3_mk_builtin_num,
   mk_builtin_fun = (fn _ => fn sym => fn cts =>
     (case try (Thm.typ_of_cterm o hd) cts of
       SOME \<^typ>\<open>real\<close> => z3_mk_builtin_fun sym cts
     | _ => NONE)) }
 
 end
 
 
 (* Z3 proof replay *)
 
 val real_linarith_proc =
   Simplifier.make_simproc \<^context> "fast_real_arith"
    {lhss = [\<^term>\<open>(m::real) < n\<close>, \<^term>\<open>(m::real) \<le> n\<close>, \<^term>\<open>(m::real) = n\<close>],
     proc = K Lin_Arith.simproc}
 
 
 (* setup *)
 
 val _ = Theory.setup (Context.theory_map (
   SMTLIB_Interface.add_logic (10, smtlib_logic) #>
   setup_builtins #>
   Z3_Interface.add_mk_builtins z3_mk_builtins #>
   SMT_Replay.add_simproc real_linarith_proc))
 
 end;
diff --git a/src/HOL/Tools/SMT/smt_solver.ML b/src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML
+++ b/src/HOL/Tools/SMT/smt_solver.ML
@@ -1,318 +1,318 @@
 (*  Title:      HOL/Tools/SMT/smt_solver.ML
     Author:     Sascha Boehme, TU Muenchen
 
 SMT solvers registry and SMT tactic.
 *)
 
 signature SMT_SOLVER =
 sig
   (*configuration*)
   datatype outcome = Unsat | Sat | Unknown | Time_Out
 
   type parsed_proof =
     {outcome: SMT_Failure.failure option,
      fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option,
      atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
 
   type solver_config =
     {name: string,
      class: Proof.context -> SMT_Util.class,
      avail: unit -> bool,
      command: unit -> string list,
      options: Proof.context -> string list,
      smt_options: (string * string) list,
      default_max_relevant: int,
      outcome: string -> string list -> outcome * string list,
      parse_proof: (Proof.context -> SMT_Translate.replay_data ->
        ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
        parsed_proof) option,
      replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option}
 
   (*registry*)
   val add_solver: solver_config -> theory -> theory
   val default_max_relevant: Proof.context -> string -> int
 
   (*filter*)
   val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list ->
     int -> Time.time -> parsed_proof
 
   (*tactic*)
   val smt_tac: Proof.context -> thm list -> int -> tactic
   val smt_tac': Proof.context -> thm list -> int -> tactic
 end;
 
 structure SMT_Solver: SMT_SOLVER =
 struct
 
 (* interface to external solvers *)
 
 local
 
 fun make_command command options problem_path proof_path =
   Bash.strings (command () @ options) ^ " " ^
     File.bash_platform_path problem_path ^
     " > " ^ File.bash_path proof_path ^ " 2>&1"
 
 fun with_trace ctxt msg f x =
   let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
   in f x end
 
 fun run ctxt name mk_cmd input =
   (case SMT_Config.certificates_of ctxt of
     NONE =>
       if not (SMT_Config.is_available ctxt name) then
         error ("The SMT solver " ^ quote name ^ " is not installed")
       else if Config.get ctxt SMT_Config.debug_files = "" then
         with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run mk_cmd) input
       else
         let
           val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files)
           val in_path = Path.ext "smt_in" base_path
           val out_path = Path.ext "smt_out" base_path
         in Cache_IO.raw_run mk_cmd input in_path out_path end
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>
           if Config.get ctxt SMT_Config.read_only_certificates then
             error ("Bad certificate cache: missing certificate")
           else
             Cache_IO.run_and_cache certs key mk_cmd input
       | (SOME output, _) =>
           with_trace ctxt ("Using cached certificate from " ^
             Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
 
 (* Z3 and cvc returns 1 if "get-proof" or "get-model" fails.
 veriT returns 255 in that case and 14 for timeouts. *)
 fun normal_return_codes "z3" = [0, 1]
   | normal_return_codes "verit" = [0, 14, 255]
   | normal_return_codes _ = [0, 1]
 
 fun run_solver ctxt name mk_cmd input =
   let
     fun pretty tag lines = Pretty.string_of (Pretty.big_list tag (map Pretty.str lines))
 
     val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
 
     val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) =
       Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input
     val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
 
     val output = drop_suffix (equal "") res
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
     val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
     val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
 
     val _ = member (op =) (normal_return_codes name) return_code orelse
       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
   in output end
 
 fun trace_assms ctxt =
   SMT_Config.trace_msg ctxt (Pretty.string_of o
     Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
 
 fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) =
   let
     fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
     fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
     fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
   in
     SMT_Config.trace_msg ctxt (fn () =>
       Pretty.string_of (Pretty.big_list "Names:" [
         Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
         Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
   end
 
 in
 
 fun invoke name command smt_options ithms ctxt =
   let
     val options = SMT_Config.solver_options_of ctxt
     val comments = [space_implode " " options]
 
     val (str, replay_data as {context = ctxt', ...}) =
       ithms
       |> tap (trace_assms ctxt)
-      |> SMT_Translate.translate ctxt smt_options comments
+      |> SMT_Translate.translate ctxt name smt_options comments
       ||> tap trace_replay_data
   in (run_solver ctxt' name (make_command command options) str, replay_data) end
 
 end
 
 
 (* configuration *)
 
 datatype outcome = Unsat | Sat | Unknown | Time_Out
 
 type parsed_proof =
   {outcome: SMT_Failure.failure option,
    fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option,
    atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
 
 type solver_config =
   {name: string,
    class: Proof.context -> SMT_Util.class,
    avail: unit -> bool,
    command: unit -> string list,
    options: Proof.context -> string list,
    smt_options: (string * string) list,
    default_max_relevant: int,
    outcome: string -> string list -> outcome * string list,
    parse_proof: (Proof.context -> SMT_Translate.replay_data ->
      ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
      parsed_proof) option,
    replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option}
 
 
 (* check well-sortedness *)
 
 val has_topsort = Term.exists_type (Term.exists_subtype (fn
     TFree (_, []) => true
   | TVar (_, []) => true
   | _ => false))
 
 (* top sorts cause problems with atomization *)
 fun check_topsort ctxt thm =
   if has_topsort (Thm.prop_of thm) then (SMT_Normalize.drop_fact_warning ctxt thm; TrueI) else thm
 
 
 (* registry *)
 
 type solver_info = {
   command: unit -> string list,
   smt_options: (string * string) list,
   default_max_relevant: int,
   parse_proof: Proof.context -> SMT_Translate.replay_data ->
     ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
     parsed_proof,
   replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm}
 
 structure Solvers = Generic_Data
 (
   type T = solver_info Symtab.table
   val empty = Symtab.empty
   fun merge data = Symtab.merge (K true) data
 )
 
 local
   fun parse_proof outcome parse_proof0 outer_ctxt replay_data xfacts prems concl output =
     (case outcome output of
       (Unsat, lines) =>
         (case parse_proof0 of
           SOME pp => pp outer_ctxt replay_data xfacts prems concl lines
         | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []})
     | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   fun replay outcome replay0 oracle outer_ctxt
       (replay_data as {context = ctxt, ...} : SMT_Translate.replay_data) output =
     (case outcome output of
       (Unsat, lines) =>
         if Config.get ctxt SMT_Config.oracle then
           oracle ()
         else
           (case replay0 of
             SOME replay => replay outer_ctxt replay_data lines
           | NONE => error "No proof reconstruction for solver -- \
             \declare [[smt_oracle]] to allow oracle")
     | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out)
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   val cfalse = Thm.cterm_of \<^context> \<^prop>\<open>False\<close>
 in
 
 fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome,
     parse_proof = parse_proof0, replay = replay0} : solver_config) =
   let
     fun solver oracle = {
       command = command,
       smt_options = smt_options,
       default_max_relevant = default_max_relevant,
       parse_proof = parse_proof (outcome name) parse_proof0,
       replay = replay (outcome name) replay0 oracle}
 
     val info = {name = name, class = class, avail = avail, options = options}
   in
     Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, oracle) =>
     Context.theory_map (Solvers.map (Symtab.update_new (name, solver oracle)))) #>
     Context.theory_map (SMT_Config.add_solver info)
   end
 
 end
 
 fun get_info ctxt name = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
 
 fun name_and_info_of ctxt =
   let val name = SMT_Config.solver_of ctxt
   in (name, get_info ctxt name) end
 
 val default_max_relevant = #default_max_relevant oo get_info
 
 fun apply_solver_and_replay ctxt thms0 =
   let
     val thms = map (check_topsort ctxt) thms0
     val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt
     val (output, replay_data) =
       invoke name command smt_options (SMT_Normalize.normalize ctxt thms) ctxt
   in replay ctxt replay_data output end
 
 
 (* filter (for Sledgehammer) *)
 
 fun smt_filter ctxt0 goal xfacts i time_limit =
   let
     val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit)
 
     val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal
     fun negate ct = Thm.dest_comb ct ||> Thm.apply \<^cterm>\<open>Not\<close> |-> Thm.apply
     val cprop =
       (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of
         SOME ct => ct
       | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal"))
 
     val conjecture = Thm.assume cprop
     val facts = map snd xfacts
     val thms = conjecture :: prems @ facts
     val thms' = map (check_topsort ctxt) thms
 
     val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt
     val (output, replay_data) =
       invoke name command smt_options (SMT_Normalize.normalize ctxt thms') ctxt
   in
     parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
   end
   handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = NONE, atp_proof = K []}
 
 
 (* SMT tactic *)
 
 local
   fun str_of ctxt fail =
     "Solver " ^ SMT_Config.solver_of ctxt ^ ": " ^ SMT_Failure.string_of_failure fail
 
   fun safe_solve ctxt facts = SOME (apply_solver_and_replay ctxt facts)
     handle
       SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
         (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
     | SMT_Failure.SMT (fail as SMT_Failure.Time_Out) =>
         (SMT_Config.verbose_msg ctxt (K ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^
           SMT_Failure.string_of_failure fail ^ " (setting the " ^
           "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")) ();
          NONE)
     | SMT_Failure.SMT fail => error (str_of ctxt fail)
 
   fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1
     | resolve _ NONE = no_tac
 
   fun tac prove ctxt rules =
     CONVERSION (SMT_Normalize.atomize_conv ctxt)
     THEN' resolve_tac ctxt @{thms ccontr}
     THEN' SUBPROOF (fn {context = ctxt', prems, ...} =>
       resolve ctxt' (prove ctxt' (rules @ prems))) ctxt
 in
 
 val smt_tac = tac safe_solve
 val smt_tac' = tac (SOME oo apply_solver_and_replay)
 
 end
 
 end;
diff --git a/src/HOL/Tools/SMT/smt_systems.ML b/src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML
+++ b/src/HOL/Tools/SMT/smt_systems.ML
@@ -1,204 +1,208 @@
 (*  Title:      HOL/Tools/SMT/smt_systems.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Setup SMT solvers.
 *)
 
 signature SMT_SYSTEMS =
 sig
   val cvc4_extensions: bool Config.T
   val z3_extensions: bool Config.T
 end;
 
 structure SMT_Systems: SMT_SYSTEMS =
 struct
 
 (* helper functions *)
 
 fun check_tool var () =
   (case getenv var of
     "" => NONE
   | s =>
       if File.is_file (Path.variable var |> Path.expand |> Path.platform_exe)
       then SOME [s] else NONE);
 
 fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
 
 fun make_command name () = [getenv (name ^ "_SOLVER")]
 
 fun outcome_of unsat sat unknown timeout solver_name line =
   if String.isPrefix unsat line then SMT_Solver.Unsat
   else if String.isPrefix sat line then SMT_Solver.Sat
   else if String.isPrefix unknown line then SMT_Solver.Unknown
   else if String.isPrefix timeout line then SMT_Solver.Time_Out
   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
     " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
     " option for details"))
 
 (* When used with bitvectors, CVC4 can produce error messages like:
 
 $ISABELLE_TMP_PREFIX/... No set-logic command was given before this point.
 
 These message should be ignored.
 *)
 fun is_blank_or_error_line "" = true
   | is_blank_or_error_line s =
   String.isPrefix "(error " s orelse String.isPrefix (getenv "ISABELLE_TMP_PREFIX") s
 
 fun on_first_line test_outcome solver_name lines =
   let
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
     val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines)
   in (test_outcome solver_name l, ls) end
 
 fun on_first_non_unsupported_line test_outcome solver_name lines =
   on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
 
 
 (* CVC4 *)
 
 val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false)
 
 local
   fun cvc4_options ctxt =
     ["--no-stats",
      "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
      "--lang=smt2"] @
     (case SMT_Config.get_timeout ctxt of
       NONE => []
     | SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)])
 
   fun select_class ctxt =
     if Config.get ctxt cvc4_extensions then
       if Config.get ctxt SMT_Config.higher_order then
         CVC4_Interface.hosmtlib_cvc4C
       else
         CVC4_Interface.smtlib_cvc4C
     else
       if Config.get ctxt SMT_Config.higher_order then
         SMTLIB_Interface.hosmtlibC
+      else if Config.get ctxt SMT_Config.native_bv then
+        SMTLIB_Interface.bvsmlibC
       else
         SMTLIB_Interface.smtlibC
 in
 
 val cvc4: SMT_Solver.solver_config = {
   name = "cvc4",
   class = select_class,
   avail = make_avail "CVC4",
   command = make_command "CVC4",
   options = cvc4_options,
   smt_options = [(":produce-unsat-cores", "true")],
   default_max_relevant = 400 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
   replay = NONE }
 
 end
 
 
 (* veriT *)
 
 local
   fun select_class ctxt =
     if Config.get ctxt SMT_Config.higher_order then
       SMTLIB_Interface.hosmtlibC
     else
       SMTLIB_Interface.smtlibC
 
   fun veriT_options ctxt =
    ["--proof-with-sharing",
     "--proof-define-skolems",
     "--proof-prune",
     "--proof-merge",
     "--disable-print-success",
     "--disable-banner"] @
     Verit_Proof.veriT_current_strategy (Context.Proof ctxt) @
     (case SMT_Config.get_timeout ctxt of
       NONE => []
     | SOME t => ["--max-time=" ^ string_of_int (Time.toMilliseconds t)])
 in
 
 val veriT: SMT_Solver.solver_config = {
   name = "verit",
   class = select_class,
   avail = is_some o check_tool "ISABELLE_VERIT",
   command = the o check_tool "ISABELLE_VERIT",
   options = veriT_options,
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 200 (* FUDGE *),
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"),
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   replay = SOME Verit_Replay.replay }
 
 end
 
 
 (* Z3 *)
 
 val z3_extensions = Attrib.setup_config_bool \<^binding>\<open>z3_extensions\<close> (K false)
 
 local
   fun z3_options ctxt =
     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
      "smt.refine_inj_axioms=false"] @
     (case SMT_Config.get_timeout ctxt of
       NONE => []
     | SOME t => ["-T:" ^ string_of_int (Real.ceil (Time.toReal t))]) @
     ["-smt2"]
 
   fun select_class ctxt =
-    if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC
+    if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C
+    else if Config.get ctxt SMT_Config.native_bv then SMTLIB_Interface.bvsmlibC
+    else SMTLIB_Interface.smtlibC
 in
 
 val z3: SMT_Solver.solver_config = {
   name = "z3",
   class = select_class,
   avail = make_avail "Z3",
   command = make_command "Z3",
   options = z3_options,
   smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 350 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME Z3_Replay.parse_proof,
   replay = SOME Z3_Replay.replay }
 
 end
 
 (* smt tactic *)
 val parse_smt_options =
   Scan.optional
     (Args.parens (Args.name -- Scan.option (\<^keyword>\<open>,\<close> |-- Args.name)) >> apfst SOME)
     (NONE, NONE)
 
 fun smt_method ((solver, stgy), thms) ctxt facts =
   let
     val default_solver = SMT_Config.solver_of ctxt
     val solver = the_default default_solver solver
     val _ = 
       if solver = "z3" andalso stgy <> NONE
       then warning ("No strategy is available for z3. Ignoring " ^ quote (the stgy)) 
       else ()
     val ctxt =
       ctxt
       |> (if stgy <> NONE then Context.proof_map (Verit_Proof.select_veriT_stgy (the stgy)) else I)
       |> Context.Proof
       |> SMT_Config.select_solver solver
       |> Context.proof_of
   in
     HEADGOAL (SOLVED' (SMT_Solver.smt_tac ctxt (thms @ facts)))
   end
 
 val _ =
   Theory.setup
     (Method.setup \<^binding>\<open>smt\<close>
       (Scan.lift parse_smt_options -- Attrib.thms >> (METHOD oo smt_method))
       "Call to the SMT solvers veriT or z3")
 
 (* overall setup *)
 
 val _ = Theory.setup (
   SMT_Solver.add_solver cvc4 #>
   SMT_Solver.add_solver veriT #>
   SMT_Solver.add_solver z3)
 
 end;
diff --git a/src/HOL/Tools/SMT/smt_translate.ML b/src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML
+++ b/src/HOL/Tools/SMT/smt_translate.ML
@@ -1,537 +1,537 @@
 (*  Title:      HOL/Tools/SMT/smt_translate.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Translate theorems into an SMT intermediate format and serialize them.
 *)
 
 signature SMT_TRANSLATE =
 sig
   (*intermediate term structure*)
   datatype squant = SForall | SExists
   datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
   datatype sterm =
     SVar of int * sterm list |
     SConst of string * sterm list |
     SQua of squant * string list * sterm spattern list * sterm
 
   (*translation configuration*)
   type sign = {
     logic: string,
     sorts: string list,
     dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
     funcs: (string * (string list * string)) list }
   type config = {
     order: SMT_Util.order,
-    logic: term list -> string,
+    logic: string -> term list -> string,
     fp_kinds: BNF_Util.fp_kind list,
     serialize: (string * string) list -> string list -> sign -> sterm list -> string }
   type replay_data = {
     context: Proof.context,
     typs: typ Symtab.table,
     terms: term Symtab.table,
     ll_defs: term list,
     rewrite_rules: thm list,
     assms: (int * thm) list }
 
   (*translation*)
   val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
-  val translate: Proof.context -> (string * string) list -> string list -> (int * thm) list ->
+  val translate: Proof.context -> string -> (string * string) list -> string list -> (int * thm) list ->
     string * replay_data
 end;
 
 structure SMT_Translate: SMT_TRANSLATE =
 struct
 
 
 (* intermediate term structure *)
 
 datatype squant = SForall | SExists
 
 datatype 'a spattern =
   SPat of 'a list | SNoPat of 'a list
 
 datatype sterm =
   SVar of int * sterm list |
   SConst of string * sterm list |
   SQua of squant * string list * sterm spattern list * sterm
 
 
 (* translation configuration *)
 
 type sign = {
   logic: string,
   sorts: string list,
   dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
   funcs: (string * (string list * string)) list }
 
 type config = {
   order: SMT_Util.order,
-  logic: term list -> string,
+  logic: string -> term list -> string,
   fp_kinds: BNF_Util.fp_kind list,
   serialize: (string * string) list -> string list -> sign -> sterm list -> string }
 
 type replay_data = {
   context: Proof.context,
   typs: typ Symtab.table,
   terms: term Symtab.table,
   ll_defs: term list,
   rewrite_rules: thm list,
   assms: (int * thm) list }
 
 
 (* translation context *)
 
 fun add_components_of_typ (Type (s, Ts)) =
     cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts
   | add_components_of_typ (TFree (s, _)) = cons (perhaps (try (unprefix "'")) s)
   | add_components_of_typ _ = I;
 
 fun suggested_name_of_typ T = space_implode "_" (add_components_of_typ T []);
 
 fun suggested_name_of_term (Const (s, _)) = Long_Name.base_name s
   | suggested_name_of_term (Free (s, _)) = s
   | suggested_name_of_term _ = Name.uu
 
 val empty_tr_context = (Name.context, Typtab.empty, Termtab.empty)
 val safe_suffix = "$"
 
 fun add_typ T proper (cx as (names, typs, terms)) =
   (case Typtab.lookup typs T of
     SOME (name, _) => (name, cx)
   | NONE =>
       let
         val sugg = Name.desymbolize (SOME true) (suggested_name_of_typ T) ^ safe_suffix
         val (name, names') = Name.variant sugg names
         val typs' = Typtab.update (T, (name, proper)) typs
       in (name, (names', typs', terms)) end)
 
 fun add_fun t sort (cx as (names, typs, terms)) =
   (case Termtab.lookup terms t of
     SOME (name, _) => (name, cx)
   | NONE =>
       let
         val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix
         val (name, names') = Name.variant sugg names
         val terms' = Termtab.update (t, (name, sort)) terms
       in (name, (names', typs, terms')) end)
 
 fun sign_of logic dtyps (_, typs, terms) = {
   logic = logic,
   sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
   dtyps = dtyps,
   funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
 
 fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) =
   let
     fun add_typ (T, (n, _)) = Symtab.update (n, T)
     val typs' = Typtab.fold add_typ typs Symtab.empty
 
     fun add_fun (t, (n, _)) = Symtab.update (n, t)
     val terms' = Termtab.fold add_fun terms Symtab.empty
   in
     {context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules,
      assms = assms}
   end
 
 
 (* preprocessing *)
 
 (** (co)datatype declarations **)
 
 fun collect_co_datatypes fp_kinds (tr_context, ctxt) ts =
   let
     val (fp_decls, ctxt') =
       ([], ctxt)
       |> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds)) ts
       |>> flat
 
     fun is_decl_typ T = exists (equal T o fst o snd) fp_decls
 
     fun add_typ' T proper =
       (case SMT_Builtin.dest_builtin_typ ctxt' T of
         SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *)
       | NONE => add_typ T proper)
 
     fun tr_select sel =
       let val T = Term.range_type (Term.fastype_of sel)
       in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end
     fun tr_constr (constr, selects) =
       add_fun constr NONE ##>> fold_map tr_select selects
     fun tr_typ (fp, (T, cases)) =
       add_typ' T false ##>> fold_map tr_constr cases #>> pair fp
 
     val (fp_decls', tr_context') = fold_map tr_typ fp_decls tr_context
 
     fun add (constr, selects) =
       Termtab.update (constr, length selects) #>
       fold (Termtab.update o rpair 1) selects
 
     val funcs = fold (fold add o snd o snd) fp_decls Termtab.empty
 
   in ((funcs, fp_decls', tr_context', ctxt'), ts) end
     (* FIXME: also return necessary (co)datatype theorems *)
 
 
 (** eta-expand quantifiers, let expressions and built-ins *)
 
 local
   fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0))
 
   fun exp f T = eta f (Term.domain_type (Term.domain_type T))
 
   fun exp2 T q =
     let val U = Term.domain_type T
     in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end
 
   fun expf k i T t =
     let val Ts = drop i (fst (SMT_Util.dest_funT k T))
     in
       Term.incr_boundvars (length Ts) t
       |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
       |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
     end
 in
 
 fun eta_expand ctxt funcs =
   let
     fun exp_func t T ts =
       (case Termtab.lookup funcs t of
         SOME k => Term.list_comb (t, ts) |> k <> length ts ? expf k (length ts) T
       | NONE => Term.list_comb (t, ts))
 
     fun expand ((q as Const (\<^const_name>\<open>All\<close>, _)) $ Abs a) = q $ abs_expand a
       | expand ((q as Const (\<^const_name>\<open>All\<close>, T)) $ t) = q $ exp expand T t
       | expand (q as Const (\<^const_name>\<open>All\<close>, T)) = exp2 T q
       | expand ((q as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs a) = q $ abs_expand a
       | expand ((q as Const (\<^const_name>\<open>Ex\<close>, T)) $ t) = q $ exp expand T t
       | expand (q as Const (\<^const_name>\<open>Ex\<close>, T)) = exp2 T q
       | expand (Const (\<^const_name>\<open>Let\<close>, T) $ t) =
           let val U = Term.domain_type (Term.range_type T)
           in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
       | expand (Const (\<^const_name>\<open>Let\<close>, T)) =
           let val U = Term.domain_type (Term.range_type T)
           in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end
       | expand t =
           (case Term.strip_comb t of
             (Const (\<^const_name>\<open>Let\<close>, _), t1 :: t2 :: ts) =>
             Term.betapplys (Term.betapply (expand t2, expand t1), map expand ts)
           | (u as Const (c as (_, T)), ts) =>
               (case SMT_Builtin.dest_builtin ctxt c ts of
                 SOME (_, k, us, mk) =>
                   if k = length us then mk (map expand us)
                   else if k < length us then chop k (map expand us) |>> mk |> Term.list_comb
                   else expf k (length ts) T (mk (map expand us))
               | NONE => exp_func u T (map expand ts))
           | (u as Free (_, T), ts) => exp_func u T (map expand ts)
           | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts)
           | (u, ts) => Term.list_comb (u, map expand ts))
 
     and abs_expand (n, T, t) = Abs (n, T, expand t)
 
   in map expand end
 
 end
 
 
 (** introduce explicit applications **)
 
 local
   (*
     Make application explicit for functions with varying number of arguments.
   *)
 
   fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i))
   fun add_type T = apsnd (Typtab.update (T, ()))
 
   fun min_arities t =
     (case Term.strip_comb t of
       (u as Const _, ts) => add u (length ts) #> fold min_arities ts
     | (u as Free _, ts) => add u (length ts) #> fold min_arities ts
     | (Abs (_, T, u), ts) => (can dest_funT T ? add_type T) #> min_arities u #> fold min_arities ts
     | (_, ts) => fold min_arities ts)
 
   fun take_vars_into_account types t i =
     let
       fun find_min j (T as Type (\<^type_name>\<open>fun\<close>, [_, T'])) =
           if j = i orelse Typtab.defined types T then j else find_min (j + 1) T'
         | find_min j _ = j
     in find_min 0 (Term.type_of t) end
 
   fun app u (t, T) = (Const (\<^const_name>\<open>fun_app\<close>, T --> T) $ t $ u, Term.range_type T)
 
   fun apply i t T ts =
     let
       val (ts1, ts2) = chop i ts
       val (_, U) = SMT_Util.dest_funT i T
     in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
 in
 
 fun intro_explicit_application ctxt funcs ts =
   let
     val explicit_application = Config.get ctxt SMT_Config.explicit_application
     val get_arities =
       (case explicit_application of
         0 => min_arities
       | 1 => min_arities
       | 2 => K I
       | n => error ("Illegal value for " ^ quote (Config.name_of SMT_Config.explicit_application) ^
           ": " ^ string_of_int n))
 
     val (arities, types) = fold get_arities ts (Termtab.empty, Typtab.empty)
     val arities' = arities |> explicit_application = 1 ? Termtab.map (take_vars_into_account types)
 
     fun app_func t T ts =
       if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
       else apply (the_default 0 (Termtab.lookup arities' t)) t T ts
 
     fun in_list T f t = SMT_Util.mk_symb_list T (map f (SMT_Util.dest_symb_list t))
 
     fun traverse Ts t =
       (case Term.strip_comb t of
         (q as Const (\<^const_name>\<open>All\<close>, _), [Abs (x, T, u)]) =>
           q $ Abs (x, T, in_trigger (T :: Ts) u)
       | (q as Const (\<^const_name>\<open>Ex\<close>, _), [Abs (x, T, u)]) =>
           q $ Abs (x, T, in_trigger (T :: Ts) u)
       | (q as Const (\<^const_name>\<open>Let\<close>, _), [u1, u2 as Abs _]) =>
           q $ traverse Ts u1 $ traverse Ts u2
       | (u as Const (c as (_, T)), ts) =>
           (case SMT_Builtin.dest_builtin ctxt c ts of
             SOME (_, k, us, mk) =>
               let
                 val (ts1, ts2) = chop k (map (traverse Ts) us)
                 val U = Term.strip_type T |>> snd o chop k |> (op --->)
               in apply 0 (mk ts1) U ts2 end
           | NONE => app_func u T (map (traverse Ts) ts))
       | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
       | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
       | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
       | (u, ts) => traverses Ts u ts)
     and in_trigger Ts ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
       | in_trigger Ts t = traverse Ts t
     and in_pats Ts ps =
       in_list \<^typ>\<open>pattern symb_list\<close> (in_list \<^typ>\<open>pattern\<close> (in_pat Ts)) ps
     and in_pat Ts ((p as \<^Const_>\<open>pat _\<close>) $ t) = p $ traverse Ts t
       | in_pat Ts ((p as \<^Const_>\<open>nopat _\<close>) $ t) = p $ traverse Ts t
       | in_pat _ t = raise TERM ("bad pattern", [t])
     and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
   in map (traverse []) ts end
 
 val fun_app_eq = mk_meta_eq @{thm fun_app_def}
 
 end
 
 
 (** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **)
 
 local
   val is_quant = member (op =) [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>]
 
   val fol_rules = [
     Let_def,
     @{lemma "P = True == P" by (rule eq_reflection) simp}]
 
   exception BAD_PATTERN of unit
 
   fun is_builtin_conn_or_pred ctxt c ts =
     is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
     is_some (SMT_Builtin.dest_builtin_pred ctxt c ts)
 in
 
 fun folify ctxt =
   let
     fun in_list T f t = SMT_Util.mk_symb_list T (map_filter f (SMT_Util.dest_symb_list t))
 
     fun in_term pat t =
       (case Term.strip_comb t of
         (\<^Const_>\<open>True\<close>, []) => t
       | (\<^Const_>\<open>False\<close>, []) => t
       | (u as \<^Const_>\<open>If _\<close>, [t1, t2, t3]) =>
           if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
       | (Const (c as (n, _)), ts) =>
           if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then
             if pat then raise BAD_PATTERN () else in_form t
           else
             Term.list_comb (Const c, map (in_term pat) ts)
       | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
       | _ => t)
 
     and in_pat ((p as Const (\<^const_name>\<open>pat\<close>, _)) $ t) =
           p $ in_term true t
       | in_pat ((p as Const (\<^const_name>\<open>nopat\<close>, _)) $ t) =
           p $ in_term true t
       | in_pat t = raise TERM ("bad pattern", [t])
 
     and in_pats ps =
       in_list \<^typ>\<open>pattern symb_list\<close> (SOME o in_list \<^typ>\<open>pattern\<close> (try in_pat)) ps
 
     and in_trigger ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t
       | in_trigger t = in_form t
 
     and in_form t =
       (case Term.strip_comb t of
         (q as Const (qn, _), [Abs (n, T, u)]) =>
           if is_quant qn then q $ Abs (n, T, in_trigger u)
           else in_term false t
       | (Const c, ts) =>
           (case SMT_Builtin.dest_builtin_conn ctxt c ts of
             SOME (_, _, us, mk) => mk (map in_form us)
           | NONE =>
               (case SMT_Builtin.dest_builtin_pred ctxt c ts of
                 SOME (_, _, us, mk) => mk (map (in_term false) us)
               | NONE => in_term false t))
       | _ => in_term false t)
   in
     map in_form #>
     pair (fol_rules, I)
   end
 
 end
 
 
 (* translation into intermediate format *)
 
 (** utility functions **)
 
 val quantifier = (fn
     \<^const_name>\<open>All\<close> => SOME SForall
   | \<^const_name>\<open>Ex\<close> => SOME SExists
   | _ => NONE)
 
 fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) =
       if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
   | group_quant _ Ts t = (Ts, t)
 
 fun dest_pat (Const (\<^const_name>\<open>pat\<close>, _) $ t) = (t, true)
   | dest_pat (Const (\<^const_name>\<open>nopat\<close>, _) $ t) = (t, false)
   | dest_pat t = raise TERM ("bad pattern", [t])
 
 fun dest_pats [] = I
   | dest_pats ts =
       (case map dest_pat ts |> split_list ||> distinct (op =) of
         (ps, [true]) => cons (SPat ps)
       | (ps, [false]) => cons (SNoPat ps)
       | _ => raise TERM ("bad multi-pattern", ts))
 
 fun dest_trigger \<^Const_>\<open>trigger for tl t\<close> =
       (rev (fold (dest_pats o SMT_Util.dest_symb_list) (SMT_Util.dest_symb_list tl) []), t)
   | dest_trigger t = ([], t)
 
 fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
   let
     val (Ts, u) = group_quant qn [T] t
     val (ps, p) = dest_trigger u
   in (q, rev Ts, ps, p) end)
 
 fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
   | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
 
 
 (** translation from Isabelle terms into SMT intermediate terms **)
 
 fun intermediate logic dtyps builtin ctxt ts trx =
   let
     fun transT (T as TFree _) = add_typ T true
       | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
       | transT (T as Type _) =
           (case SMT_Builtin.dest_builtin_typ ctxt T of
             SOME (n, []) => pair n
           | SOME (n, Ts) =>
             fold_map transT Ts
             #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
           | NONE => add_typ T true)
 
     fun trans t =
       (case Term.strip_comb t of
         (Const (qn, _), [Abs (_, T, t1)]) =>
           (case dest_quant qn T t1 of
             SOME (q, Ts, ps, b) =>
               fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
               trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
           | NONE => raise TERM ("unsupported quantifier", [t]))
       | (u as Const (c as (_, T)), ts) =>
           (case builtin ctxt c ts of
             SOME (n, _, us, _) => fold_map trans us #>> curry SConst n
           | NONE => trans_applied_fun u T ts)
       | (u as Free (_, T), ts) => trans_applied_fun u T ts
       | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar
       | _ => raise TERM ("bad SMT term", [t]))
 
     and trans_applied_fun t T ts =
       let val (Us, U) = SMT_Util.dest_funT (length ts) T
       in
         fold_map transT Us ##>> transT U #-> (fn Up =>
           add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
       end
 
     val (us, trx') = fold_map trans ts trx
   in ((sign_of (logic ts) dtyps trx', us), trx') end
 
 
 (* translation *)
 
 structure Configs = Generic_Data
 (
   type T = (Proof.context -> config) SMT_Util.dict
   val empty = []
   fun merge data = SMT_Util.dict_merge fst data
 )
 
 fun add_config (cs, cfg) = Configs.map (SMT_Util.dict_update (cs, cfg))
 
 fun get_config ctxt =
   let val cs = SMT_Config.solver_class_of ctxt
   in
     (case SMT_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of
       SOME cfg => cfg ctxt
     | NONE => error ("SMT: no translation configuration found " ^
         "for solver class " ^ quote (SMT_Util.string_of_class cs)))
   end
 
-fun translate ctxt smt_options comments ithms =
+fun translate ctxt prover smt_options comments ithms =
   let
     val {order, logic, fp_kinds, serialize} = get_config ctxt
 
     fun no_dtyps (tr_context, ctxt) ts =
       ((Termtab.empty, [], tr_context, ctxt), ts)
 
     val ts1 = map (Envir.beta_eta_contract o SMT_Util.prop_of o snd) ithms
 
     val ((funcs, dtyps, tr_context, ctxt1), ts2) =
       ((empty_tr_context, ctxt), ts1)
       |-> (if null fp_kinds then no_dtyps else collect_co_datatypes fp_kinds)
 
     fun is_binder (Const (\<^const_name>\<open>Let\<close>, _) $ _) = true
       | is_binder t = Lambda_Lifting.is_quantifier t
 
     fun mk_trigger ((q as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (n, T, t)) =
           q $ Abs (n, T, mk_trigger t)
       | mk_trigger (eq as (Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lhs $ _)) =
           Term.domain_type T --> \<^typ>\<open>pattern\<close>
           |> (fn T => Const (\<^const_name>\<open>pat\<close>, T) $ lhs)
           |> SMT_Util.mk_symb_list \<^typ>\<open>pattern\<close> o single
           |> SMT_Util.mk_symb_list \<^typ>\<open>pattern symb_list\<close> o single
           |> (fn t => \<^Const>\<open>trigger for t eq\<close>)
       | mk_trigger t = t
 
     val (ctxt2, (ts3, ll_defs)) =
       ts2
       |> eta_expand ctxt1 funcs
       |> rpair ctxt1
       |-> Lambda_Lifting.lift_lambdas NONE is_binder
       |-> (fn (ts', ll_defs) => fn ctxt' =>
         let
           val ts'' = map mk_trigger ll_defs @ ts'
             |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
         in
           (ctxt', (ts'', ll_defs))
         end)
     val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
       |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
   in
     (ts4, tr_context)
-    |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
+    |-> intermediate (logic prover) dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
     |>> uncurry (serialize smt_options comments)
     ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms
   end
 
 end;
diff --git a/src/HOL/Tools/SMT/smtlib_interface.ML b/src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML
@@ -1,178 +1,181 @@
 (*  Title:      HOL/Tools/SMT/smtlib_interface.ML
     Author:     Sascha Boehme, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
 Interface to SMT solvers based on the SMT-LIB 2 format.
 *)
 
 signature SMTLIB_INTERFACE =
 sig
   val smtlibC: SMT_Util.class
   val hosmtlibC: SMT_Util.class
-  val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
+  val bvsmlibC: SMT_Util.class
+  val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
+  val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
   val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
   val assert_name_of_index: int -> string
   val assert_index_of_name: string -> int
   val assert_prefix : string
 end;
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
 struct
 
 val hoC = ["ho"]
 
 val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
 val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
-
+val bvsmlibC = smtlibC @ ["BV"] (* if BV are supported *)
 
 (* builtins *)
 
 local
   fun int_num _ i = SOME (string_of_int i)
 
   fun is_linear [t] = SMT_Util.is_number t
     | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
     | is_linear _ = false
 
   fun times _ _ ts =
     let val mk = Term.list_comb o pair \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>
     in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
 in
 
 val setup_builtins =
   SMT_Builtin.add_builtin_typ hosmtlibC
     (\<^typ>\<open>'a => 'b\<close>, fn Type (\<^type_name>\<open>fun\<close>, Ts) => SOME ("->", Ts), K (K NONE)) #>
   fold (SMT_Builtin.add_builtin_typ smtlibC) [
     (\<^typ>\<open>bool\<close>, K (SOME ("Bool", [])), K (K NONE)),
     (\<^typ>\<open>int\<close>, K (SOME ("Int", [])), int_num)] #>
   fold (SMT_Builtin.add_builtin_fun' smtlibC) [
     (\<^Const>\<open>True\<close>, "true"),
     (\<^Const>\<open>False\<close>, "false"),
     (\<^Const>\<open>Not\<close>, "not"),
     (\<^Const>\<open>conj\<close>, "and"),
     (\<^Const>\<open>disj\<close>, "or"),
     (\<^Const>\<open>implies\<close>, "=>"),
     (\<^Const>\<open>HOL.eq \<^typ>\<open>'a\<close>\<close>, "="),
     (\<^Const>\<open>If \<^typ>\<open>'a\<close>\<close>, "ite"),
     (\<^Const>\<open>less \<^Type>\<open>int\<close>\<close>, "<"),
     (\<^Const>\<open>less_eq \<^Type>\<open>int\<close>\<close>, "<="),
     (\<^Const>\<open>uminus \<^Type>\<open>int\<close>\<close>, "-"),
     (\<^Const>\<open>plus \<^Type>\<open>int\<close>\<close>, "+"),
     (\<^Const>\<open>minus \<^Type>\<open>int\<close>\<close>, "-")] #>
   SMT_Builtin.add_builtin_fun smtlibC
     (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, times)
 
 end
 
 
 (* serialization *)
 
 (** logic **)
 
 fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
 
 structure Logics = Generic_Data
 (
-  type T = (int * (term list -> string option)) list
+  type T = (int * (string -> term list -> string option)) list
   val empty = []
   fun merge data = Ord_List.merge fst_int_ord data
 )
 
 fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
+fun del_logic pf = Logics.map (Ord_List.remove fst_int_ord pf)
 
-fun choose_logic ctxt ts =
+fun choose_logic ctxt prover ts =
   let
     fun choose [] = "AUFLIA"
-      | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
+      | choose ((_, f) :: fs) = (case f prover ts of SOME s => s | NONE => choose fs)
   in
     (case choose (Logics.get (Context.Proof ctxt)) of
       "" => "" (* for default Z3 logic, a subset of everything *)
     | logic => "(set-logic " ^ logic ^ ")\n")
   end
 
 
 (** serialization **)
 
 fun var i = "?v" ^ string_of_int i
 
 fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
   | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
       SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
   | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
   | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
       SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
   | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
       let
         val l' = l + length ss
 
         fun quant_name SMT_Translate.SForall = "forall"
           | quant_name SMT_Translate.SExists = "exists"
 
         fun gen_trees_of_pat keyword ps =
           [SMTLIB.Key keyword, SMTLIB.S (map (tree_of_sterm l') ps)]
         fun trees_of_pat (SMT_Translate.SPat ps) = gen_trees_of_pat "pattern" ps
           | trees_of_pat (SMT_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps
         fun tree_of_pats [] t = t
           | tree_of_pats pats t = SMTLIB.S (SMTLIB.Sym "!" :: t :: maps trees_of_pat pats)
 
         val vs = map_index (fn (i, ty) =>
           SMTLIB.S [SMTLIB.Sym (var (l + i)), SMTLIB.Sym ty]) ss
 
         val body = t
           |> tree_of_sterm l'
           |> tree_of_pats pats
       in
         SMTLIB.S [SMTLIB.Sym (quant_name q), SMTLIB.S vs, body]
       end
 
 
 fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")"
 fun sctr (name, args) = enclose "(" ")" (space_implode " " (name :: map sctrarg args))
 fun sdatatype (name, ctrs) = enclose "(" ")" (space_implode " " (name :: map sctr ctrs))
 
 fun string_of_fun (f, (ss, s)) = f ^ " (" ^ space_implode " " ss ^ ") " ^ s
 
 fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s]
 
 val assert_prefix = "a"
 
 fun assert_name_of_index i = assert_prefix ^ string_of_int i
 fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
 
 fun sdtyp (fp, dtyps) =
   Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
     (space_implode "\n  " (map sdatatype dtyps)))
 
 fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
   let
     val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true")
   in
     Buffer.empty
     |> fold (Buffer.add o enclose "; " "\n") comments
     |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
     |> Buffer.add logic
     |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
     |> fold sdtyp (AList.coalesce (op =) dtyps)
     |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
         (sort (fast_string_ord o apply2 fst) funcs)
     |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"
         (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts)
     |> Buffer.add "(check-sat)\n"
     |> Buffer.add (if unsat_core then "(get-unsat-core)\n" else "(get-proof)\n")
     |> Buffer.content
   end
 
 (* interface *)
 
 fun translate_config order ctxt = {
   order = order,
   logic = choose_logic ctxt,
   fp_kinds = [],
   serialize = serialize}
 
 val _ = Theory.setup (Context.theory_map
   (setup_builtins #>
    SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
    SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))
 
 end;
diff --git a/src/HOL/Tools/SMT/verit_proof.ML b/src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML
+++ b/src/HOL/Tools/SMT/verit_proof.ML
@@ -1,892 +1,893 @@
 (*  Title:      HOL/Tools/SMT/Verit_Proof.ML
     Author:     Mathias Fleury, ENS Rennes
     Author:     Sascha Boehme, TU Muenchen
 
 VeriT proofs: parsing and abstract syntax tree.
 *)
 
 signature VERIT_PROOF =
 sig
   (*proofs*)
   datatype veriT_step = VeriT_Step of {
     id: string,
     rule: string,
     prems: string list,
     proof_ctxt: term list,
     concl: term,
     fixes: string list}
 
   datatype veriT_replay_node = VeriT_Replay_Node of {
     id: string,
     rule: string,
     args: term list,
     prems: string list,
     proof_ctxt: term list,
     concl: term,
     bounds: (string * typ) list,
     declarations: (string * term) list,
     insts: term Symtab.table,
     subproof: (string * typ) list * term list * term list * veriT_replay_node list}
 
   (*proof parser*)
   val parse: typ Symtab.table -> term Symtab.table -> string list ->
     Proof.context -> veriT_step list * Proof.context
   val parse_replay: typ Symtab.table -> term Symtab.table -> string list ->
     Proof.context -> veriT_replay_node list * Proof.context
 
   val step_prefix : string
   val input_rule: string
   val keep_app_symbols: string -> bool
   val keep_raw_lifting: string -> bool
   val normalized_input_rule: string
   val la_generic_rule : string
   val rewrite_rule : string
   val simp_arith_rule : string
   val veriT_deep_skolemize_rule : string
   val veriT_def : string
   val subproof_rule : string
   val local_input_rule : string
   val not_not_rule : string
   val contract_rule : string
   val ite_intro_rule : string
   val eq_congruent_rule : string
   val eq_congruent_pred_rule : string
   val skolemization_steps : string list
   val theory_resolution2_rule: string
   val equiv_pos2_rule: string
   val th_resolution_rule: string
 
   val is_skolemization: string -> bool
   val is_skolemization_step: veriT_replay_node -> bool
 
   val number_of_steps: veriT_replay_node list -> int
 
   (*Strategy related*)
   val veriT_strategy : string Config.T
   val veriT_current_strategy : Context.generic -> string list
   val all_veriT_stgies: Context.generic -> string list;
 
   val select_veriT_stgy: string -> Context.generic -> Context.generic;
   val valid_veriT_stgy: string -> Context.generic -> bool;
   val verit_add_stgy: string * string list -> Context.generic -> Context.generic
   val verit_rm_stgy: string -> Context.generic -> Context.generic
 
   (*Global tactic*)
   val verit_tac: Proof.context -> thm list -> int -> tactic
   val verit_tac_stgy: string -> Proof.context -> thm list -> int -> tactic
 end;
 
 structure Verit_Proof: VERIT_PROOF =
 struct
 
 open SMTLIB_Proof
 
 val veriT_strategy_default_name = "default"; (*FUDGE*)
 val veriT_strategy_del_insts_name = "del_insts"; (*FUDGE*)
 val veriT_strategy_rm_insts_name = "ccfv_SIG"; (*FUDGE*)
 val veriT_strategy_ccfv_insts_name = "ccfv_threshold"; (*FUDGE*)
 val veriT_strategy_best_name = "best"; (*FUDGE*)
 
 val veriT_strategy_best = ["--index-sorts", "--index-fresh-sorts", "--triggers-new",
   "--triggers-sel-rm-specific"];
 val veriT_strategy_del_insts = ["--index-sorts", "--index-fresh-sorts", "--ccfv-breadth",
   "--inst-deletion", "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars",
   "--inst-deletion", "--index-SAT-triggers"];
 val veriT_strategy_rm_insts = ["--index-SIG", "--triggers-new", "--triggers-sel-rm-specific"];
 val veriT_strategy_ccfv_insts = ["--index-sorts", "--index-fresh-sorts", "--triggers-new",
   "--triggers-sel-rm-specific", "--triggers-restrict-combine", "--inst-deletion",
   "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars", "--inst-deletion",
   "--index-SAT-triggers", "--inst-sorts-threshold=100000", "--ematch-exp=10000000",
   "--ccfv-index=100000", "--ccfv-index-full=1000"]
 
 val veriT_strategy_default = [];
 
 type verit_strategy = {default_strategy: string, strategies: (string * string list) list}
 fun mk_verit_strategy default_strategy strategies : verit_strategy = {default_strategy=default_strategy,strategies=strategies}
 
 val empty_data = mk_verit_strategy veriT_strategy_best_name
   [(veriT_strategy_default_name, veriT_strategy_default),
    (veriT_strategy_del_insts_name, veriT_strategy_del_insts),
    (veriT_strategy_rm_insts_name, veriT_strategy_rm_insts),
    (veriT_strategy_ccfv_insts_name, veriT_strategy_ccfv_insts),
    (veriT_strategy_best_name, veriT_strategy_best)]
 
 fun merge_data ({strategies=strategies1,...}:verit_strategy,
     {default_strategy,strategies=strategies2}:verit_strategy) : verit_strategy =
   mk_verit_strategy default_strategy (AList.merge (op =) (op =) (strategies1, strategies2))
 
 structure Data = Generic_Data
 (
   type T = verit_strategy
   val empty = empty_data
   val merge = merge_data
 )
 
 fun veriT_current_strategy ctxt =
   let
     val {default_strategy,strategies} = (Data.get ctxt)
   in
     AList.lookup (op=) strategies default_strategy
    |> the
   end
 
 val veriT_strategy = Attrib.setup_config_string \<^binding>\<open>smt_verit_strategy\<close> (K veriT_strategy_best_name);
 
 fun valid_veriT_stgy stgy context =
   let
     val {strategies,...} = Data.get context
   in
     AList.defined (op =) strategies stgy
   end
 
 fun select_veriT_stgy stgy context =
   let
     val {strategies,...} = Data.get context
     val upd = Data.map (K (mk_verit_strategy stgy strategies))
   in
     if not (AList.defined (op =) strategies stgy) then
       error ("Trying to select unknown veriT strategy: " ^ quote stgy)
     else upd context
   end
 
 fun verit_add_stgy stgy context =
   let
     val {default_strategy,strategies} = Data.get context
   in
     Data.map
       (K (mk_verit_strategy default_strategy (AList.update (op =) stgy strategies)))
       context
   end
 
 fun verit_rm_stgy stgy context =
   let
     val {default_strategy,strategies} = Data.get context
   in
     Data.map
       (K (mk_verit_strategy default_strategy (AList.delete (op =) stgy strategies)))
       context
   end
 
 fun all_veriT_stgies context =
   let
     val {strategies,...} = Data.get context
    in
     map fst strategies
   end
 
-fun verit_tac ctxt = SMT_Solver.smt_tac (Context.proof_map (SMT_Config.select_solver "verit") ctxt)
+val select_verit = SMT_Config.select_solver "verit"
+fun verit_tac ctxt = SMT_Solver.smt_tac (Config.put SMT_Config.native_bv false ((Context.proof_map select_verit ctxt)))
 fun verit_tac_stgy stgy ctxt = verit_tac (Context.proof_of (select_veriT_stgy stgy (Context.Proof ctxt)))
 
 datatype raw_veriT_node = Raw_VeriT_Node of {
   id: string,
   rule: string,
   args: SMTLIB.tree,
   prems: string list,
   concl: SMTLIB.tree,
   declarations: (string * SMTLIB.tree) list,
   subproof: raw_veriT_node list}
 
 fun mk_raw_node id rule args prems declarations concl subproof =
   Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations,
     concl = concl, subproof = subproof}
 
 datatype veriT_node = VeriT_Node of {
   id: string,
   rule: string,
   prems: string list,
   proof_ctxt: term list,
   concl: term}
 
 fun mk_node id rule prems proof_ctxt concl =
   VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl}
 
 datatype veriT_replay_node = VeriT_Replay_Node of {
   id: string,
   rule: string,
   args: term list,
   prems: string list,
   proof_ctxt: term list,
   concl: term,
   bounds: (string * typ) list,
   insts: term Symtab.table,
   declarations: (string * term) list,
   subproof: (string * typ) list * term list * term list * veriT_replay_node list}
 
 fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof =
   VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
     concl = concl, bounds = bounds, insts = insts, declarations = declarations,
     subproof = subproof}
 
 datatype veriT_step = VeriT_Step of {
   id: string,
   rule: string,
   prems: string list,
   proof_ctxt: term list,
   concl: term,
   fixes: string list}
 
 fun mk_step id rule prems proof_ctxt concl fixes =
   VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
     fixes = fixes}
 
 val step_prefix = ".c"
 val input_rule = "input"
 val la_generic_rule = "la_generic"
 val normalized_input_rule = "__normalized_input" (*arbitrary*)
 val rewrite_rule = "__rewrite" (*arbitrary*)
 val subproof_rule = "subproof"
 val local_input_rule = "__local_input" (*arbitrary*)
 val simp_arith_rule = "simp_arith"
 val veriT_def = "__skolem_definition" (*arbitrary*)
 val not_not_rule = "not_not"
 val contract_rule = "contraction"
 val eq_congruent_pred_rule = "eq_congruent_pred"
 val eq_congruent_rule = "eq_congruent"
 val ite_intro_rule = "ite_intro"
 val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*)
 val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*)
 val equiv_pos2_rule = "equiv_pos2"
 val th_resolution_rule = "th_resolution"
 
 val skolemization_steps = ["sko_forall", "sko_ex"]
 val is_skolemization = member (op =) skolemization_steps
 val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
 val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
 val is_SH_trivial = member (op =) [not_not_rule, contract_rule]
 
 fun is_skolemization_step (VeriT_Replay_Node {id, ...}) = is_skolemization id
 
 (* Even the veriT developers do not know if the following rule can still appear in proofs: *)
 val veriT_deep_skolemize_rule = "deep_skolemize"
 
 fun number_of_steps [] = 0
   | number_of_steps ((VeriT_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) =
       1 + number_of_steps subproof + number_of_steps pf
 
 (* proof parser *)
 
 fun node_of p cx =
   ([], cx)
   ||>> `(with_fresh_names (term_of p))
   |>> snd
 
 fun find_type_in_formula (Abs (v, T, u)) var_name =
     if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
   | find_type_in_formula (u $ v) var_name =
     (case find_type_in_formula u var_name of
       NONE => find_type_in_formula v var_name
     | some_T => some_T)
   | find_type_in_formula (Free(v, T)) var_name =
     if String.isPrefix var_name v then SOME T else NONE
   | find_type_in_formula _ _ = NONE
 
 fun synctactic_var_subst old_name new_name (u $ v) =
     (synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v)
   | synctactic_var_subst old_name new_name (Abs (v, T, u)) =
     Abs (if String.isPrefix old_name v then new_name else v, T,
       synctactic_var_subst old_name new_name u)
   | synctactic_var_subst old_name new_name (Free (v, T)) =
      if String.isPrefix old_name v then Free (new_name, T) else Free (v, T)
   | synctactic_var_subst _ _ t = t
 
 fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) =
      Const(\<^const_name>\<open>HOL.eq\<close>, T) $ synctactic_var_subst old_name new_name t1 $ t2
   | synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>Trueprop\<close>, T) $ t1) =
      Const(\<^const_name>\<open>Trueprop\<close>, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1)
   | synctatic_rew_in_lhs_subst _ _ t = t
 
 fun add_bound_variables_to_ctxt cx =
   fold (update_binding o
     (fn (s, SOME typ) => (s, Term (Free (s, type_of cx typ)))))
 
 local
 
   fun extract_symbols bds =
     bds
     |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => [([x, y], typ)]
              | t => raise (Fail ("match error " ^ @{make_string} t)))
     |> flat
 
   (* onepoint can bind a variable to another variable or to a constant *)
   fun extract_qnt_symbols cx bds =
     bds
     |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) =>
                 (case node_of (SMTLIB.Sym y) cx of
                   ((_, []), _) => [([x], typ)]
                 | _ => [([x, y], typ)])
              | (SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _), typ) => [([x], typ)]
              | t => raise (Fail ("match error " ^ @{make_string} t)))
     |> flat
 
   fun extract_symbols_map bds =
     bds
     |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _], typ) => [([x], typ)])
     |> flat
 in
 
 fun declared_csts _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [(x, typ)]
   | declared_csts _ "__skolem_definition" t = raise (Fail ("unrecognized skolem_definition " ^ @{make_string} t))
   | declared_csts _ _ _ = []
 
 fun skolems_introduced_by_rule (SMTLIB.S bds) =
    fold (fn (SMTLIB.S [SMTLIB.Sym "=", _, SMTLIB.Sym y]) => curry (op ::) y) bds []
 
 (*FIXME there is probably a way to use the information given by onepoint*)
 fun bound_vars_by_rule _ "bind" (bds) = extract_symbols bds
   | bound_vars_by_rule cx "onepoint" bds = extract_qnt_symbols cx bds
   | bound_vars_by_rule _ "sko_forall" bds = extract_symbols_map bds
   | bound_vars_by_rule _ "sko_ex" bds = extract_symbols_map bds
   | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [([x], SOME typ)]
   | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [_, SMTLIB.Sym x, _], _)] = [([x], NONE)]
   | bound_vars_by_rule _ _ _ = []
 
 (* VeriT adds "?" before some variables. *)
 fun remove_all_qm (SMTLIB.Sym v :: l) =
     SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l
   | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l'
   | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l
   | remove_all_qm (v :: l) = v :: remove_all_qm l
   | remove_all_qm [] = []
 
 fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v)
   | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l)
   | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v
   | remove_all_qm2 v = v
 
 end
 
 datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM
 
 fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) :
      (raw_veriT_node list * SMTLIB.tree list * name_bindings) =
   let
     fun rotate_pair (a, (b, c)) = ((a, b), c)
     fun step_kind [] = (NO_STEP, SMTLIB.S [], [])
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l)
     fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id,  _, typ,
            SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx =
          (*replace the name binding by the constant instead of the full term in order to reduce
            the size of the generated terms and therefore the reconstruction time*)
          let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx
             |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id))
          in
            (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
               (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
          end
       | parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id,  _, typ, SMTLIB.S l]) cx =
          let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx
          in
            (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
               (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
          end
       | parse_skolem t _ = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx))
       | get_id_cx t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l)
       | get_id t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) =
         (SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx))
       | parse_source (l, cx) = (NONE, (l, cx))
     fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx))
       | parse_rule t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx))
       | parse_anchor_step t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_args (SMTLIB.Key "args" :: args :: l, cx) =
           let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx
           in (args, (l, cx)) end
       | parse_args (l, cx) = (SMTLIB.S [], (l, cx))
     fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) =
           (SMTLIB.Sym "false", (l, cx))
       | parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) =
           let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx
           in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end
       | parse_and_clausify_conclusion t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     val parse_normal_step =
         get_id_cx
         ##> parse_and_clausify_conclusion
         #> rotate_pair
         ##> parse_rule
         #> rotate_pair
         ##> parse_source
         #> rotate_pair
         ##> parse_args
         #> rotate_pair
 
     fun to_raw_node subproof ((((id, concl), rule), prems), args) =
         mk_raw_node id rule args (the_default [] prems) [] concl subproof
     fun at_discharge NONE _ = false
       | at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2)
   in
     case step_kind ls of
         (NO_STEP, _, _) => ([],[], cx)
       | (NORMAL_STEP, p, l) =>
           if at_discharge limit p then ([], ls, cx) else
             let
               val (s, (_, cx)) =  (p, cx)
                 |> parse_normal_step
                 ||> (fn i => i)
                 |>>  (to_raw_node [])
               val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
       | (ASSUME, p, l) =>
           let
             val (id, t :: []) = p
               |> get_id
             val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx
             val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t []
             val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
       | (ANCHOR, p, l) =>
           let
             val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args)
             val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx
             val (curss, (_, cx)) = parse_normal_step (discharge_step, cx)
             val s = to_raw_node subproof (fst curss, anchor_args)
             val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx
           in (s :: rp, rl, cx) end
       | (SKOLEM, p, l) =>
           let
             val (s, cx) = parse_skolem p cx
             val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
   end
 
 fun proof_ctxt_of_rule "bind" t = t
   | proof_ctxt_of_rule "sko_forall" t = t
   | proof_ctxt_of_rule "sko_ex" t = t
   | proof_ctxt_of_rule "let" t = t
   | proof_ctxt_of_rule "onepoint" t = t
   | proof_ctxt_of_rule _ _ = []
 
 fun args_of_rule "bind" t = t
   | args_of_rule "la_generic" t = t
   | args_of_rule "lia_generic" t = t
   | args_of_rule _ _ = []
 
 fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t
   | insts_of_forall_inst _ _ = []
 
 fun id_of_last_step prems =
   if null prems then []
   else
     let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end
 
 fun extract_assumptions_from_subproof subproof =
   let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) assms =
     if rule = local_input_rule then concl :: assms else assms
   in
     fold extract_assumptions_from_subproof subproof []
   end
 
 fun normalized_rule_name id rule =
   (case (rule = input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of
     (true, true) => normalized_input_rule
   | (true, _) => local_input_rule
   | _ => rule)
 
 fun is_assm_repetition id rule =
   rule = input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id
 
 fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice)
   | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t)
 
 (* The preprocessing takes care of:
      1. unfolding the shared terms
      2. extract the declarations of skolems to make sure that there are not unfolded
 *)
 fun preprocess compress step =
   let
     fun expand_assms cs =
       map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a)
     fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args]
       | expand_lonely_arguments (x as SMTLIB.S [SMTLIB.Sym var, _]) = [SMTLIB.S [SMTLIB.Sym "=", x, SMTLIB.Sym var]]
 
     fun preprocess (Raw_VeriT_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms)  =
       let
         val (skolem_names, stripped_args) = args
           |> (fn SMTLIB.S args => args)
           |> map
               (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y]
                 | x => x)
           |> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments)
           |> `(if rule = veriT_def then single o extract_skolem else K [])
           ||> SMTLIB.S
         val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat
         val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms)
         (* declare variables in the context *)
         val declarations =
            if rule = veriT_def
            then skolem_names |> map (fn (name, _, choice) => (name, choice))
            else []
       in
         if compress andalso rule = "or"
         then ([], (cx, remap_assms))
         else ([Raw_VeriT_Node {id = id, rule = rule, args = stripped_args,
            prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}],
           (cx, remap_assms))
       end
   in preprocess step end
 
 fun filter_split _ [] = ([], [])
   | filter_split f (a :: xs) =
      (if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs)
 
 fun collect_skolem_defs (Raw_VeriT_Node {rule, subproof = subproof, args, ...}) =
   (if is_skolemization rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else []) @
   flat (map collect_skolem_defs subproof)
 
 fun extract_types_of_args (SMTLIB.S [var, typ, t as SMTLIB.S [SMTLIB.Sym "choice", _, _]]) =
     (SMTLIB.S [var, typ, t], SOME typ)
     |> single
  | extract_types_of_args (SMTLIB.S t) =
   let
     fun extract_types_of_arg (SMTLIB.S [eq, SMTLIB.S [var, typ], t]) = (SMTLIB.S [eq, var, t], SOME typ)
       | extract_types_of_arg t = (t, NONE)
   in
     t
     |> map extract_types_of_arg
   end
 
 (*The postprocessing does:
   1. translate the terms to Isabelle syntax, taking care of free variables
   2. remove the ambiguity in the proof terms:
        x \<leadsto> y |- x = x
     means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term
     by:
       xy \<leadsto> y |- xy = x.
     This is now does not have an ambiguity and we can safely move the "xy \<leadsto> y" to the proof
     assumptions.
 *)
 fun postprocess_proof compress ctxt step cx =
   let
     fun postprocess (Raw_VeriT_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) =
     let
       val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl))
 
       val (args) = extract_types_of_args args
       val globally_bound_vars = declared_csts cx rule args
       val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ)))))
            globally_bound_vars cx
 
       (*find rebound variables specific to the LHS of the equivalence symbol*)
       val bound_vars = bound_vars_by_rule cx rule args
       val bound_vars_no_typ = map fst bound_vars
       val rhs_vars =
         fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars_no_typ []
       fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso
           not (member (op =) rhs_vars t)
       val (shadowing_vars, rebound_lhs_vars) = bound_vars
         |> filter_split (fn ([t, _], typ) => not_already_bound cx t | _ => true)
         |>> map (apfst (hd))
         |>> (fn vars => vars @ flat (map (fn ([_, t], typ) => [(t, typ)] | _ => []) bound_vars))
       val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t'))
         (map fst rebound_lhs_vars) rew
       val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t')
          subproof_rew
 
       val ((concl, bounds), cx') = node_of concl cx
 
       val extra_lhs_vars = map (fn ([a,b], typ) => (a, a^b, typ)) rebound_lhs_vars
       val old_lhs_vars = map (fn (a, _, typ) => (a, typ)) extra_lhs_vars
       val new_lhs_vars = map (fn (_, newvar, typ) => (newvar, typ)) extra_lhs_vars
 
       (* postprocess conclusion *)
       val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl)
 
       val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl))
       val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx',
         "bound_vars =", bound_vars))
 
       val bound_tvars =
         map (fn (s, SOME typ) => (s, type_of cx typ))
          (shadowing_vars @ new_lhs_vars)
       val subproof_cx =
          add_bound_variables_to_ctxt cx (shadowing_vars @ new_lhs_vars) cx
 
       fun could_unify (Bound i, Bound j) = i = j
         | could_unify (Var v, Var v') = v = v'
         | could_unify (Free v, Free v') = v = v'
         | could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty'
         | could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy')
         | could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v')
         | could_unify _ = false
       fun is_alpha_renaming t =
           t
           |> HOLogic.dest_Trueprop
           |> HOLogic.dest_eq
           |> could_unify
         handle TERM _ => false
       val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl
 
       val can_remove_subproof =
         compress andalso (is_skolemization rule orelse alpha_conversion)
       val (fixed_subproof : veriT_replay_node list, _) =
          fold_map postprocess (if can_remove_subproof then [] else subproof)
            (subproof_cx, subproof_rew)
 
       val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter
 
       (* postprocess assms *)
       val stripped_args = map fst args
       val sanitized_args = proof_ctxt_of_rule rule stripped_args
 
       val arg_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ old_lhs_vars) subproof_cx
       val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst)
       val normalized_args = map unsk_and_rewrite termified_args
 
       val subproof_assms = proof_ctxt_of_rule rule normalized_args
 
       (* postprocess arguments *)
       val rule_args = args_of_rule rule stripped_args
       val (termified_args, _) = fold_map term_of rule_args subproof_cx
       val normalized_args = map unsk_and_rewrite termified_args
       val rule_args = map subproof_rewriter normalized_args
 
       val raw_insts = insts_of_forall_inst rule stripped_args
       fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end
       val (termified_args, _) = fold_map termify_term raw_insts subproof_cx
       val insts = Symtab.empty
         |> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args
         |> Symtab.map (K unsk_and_rewrite)
 
       (* declarations *)
       val (declarations, _) = fold_map termify_term declarations cx
         |> apfst (map (apsnd unsk_and_rewrite))
 
       (* fix step *)
       val _ = if bounds <> [] then raise (Fail "found dangling variable in concl") else ()
       val skolem_defs = (if is_skolemization rule
          then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule (SMTLIB.S (map fst args))) else [])
       val skolems_of_subproof = (if is_skolemization rule
          then flat (map collect_skolem_defs subproof) else [])
       val fixed_prems =
         prems @ (if is_assm_repetition id rule then [id] else []) @
         skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof)
 
       (* fix subproof *)
       val normalized_rule = normalized_rule_name id rule
         |> (if compress andalso alpha_conversion then K "refl" else I)
 
       val extra_assms2 =
         (if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else [])
 
       val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl
         [] insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof)
 
     in
        (step, (cx', rew))
     end
   in
     postprocess step (cx, [])
     |> (fn (step, (cx, _)) => (step, cx))
   end
 
 fun combine_proof_steps ((step1 : veriT_replay_node) :: step2 :: steps) =
       let
         val (VeriT_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1,
             proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1,
             declarations = declarations1,
             subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1
         val (VeriT_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2,
             proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2,
             declarations = declarations2,
             subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2
         val goals1 =
           (case concl1 of
             _ $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $
                   (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.Not\<close>, _) $a) $ b)) => [a,b]
           | _ => [])
         val goal2 = (case concl2 of _ $ a => a)
       in
         if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1
           andalso member (op =) goals1 goal2
         then
           mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2)
             proof_ctxt2 concl2 bounds2 insts2 declarations2
             (bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) ::
           combine_proof_steps steps
         else
           mk_replay_node id1 rule1 args1 prems1
             proof_ctxt1 concl1 bounds1 insts1 declarations1
             (bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) ::
           combine_proof_steps (step2 :: steps)
       end
   | combine_proof_steps steps = steps
 
 
 val linearize_proof =
   let
     fun map_node_concl f (VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
        mk_node id rule prems proof_ctxt (f concl)
     fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems,
         proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _,
         subproof = (bounds', assms, inputs, subproof)}) =
       let
         val bounds = distinct (op =) bounds
         val bounds' = distinct (op =) bounds'
         fun mk_prop_of_term concl =
           concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close>
         fun remove_assumption_id assumption_id prems =
           filter_out (curry (op =) assumption_id) prems
         fun add_assumption assumption concl =
           \<^Const>\<open>Pure.imp for \<open>mk_prop_of_term assumption\<close> \<open>mk_prop_of_term concl\<close>\<close>
         fun inline_assumption assumption assumption_id
             (VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
           mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
             (add_assumption assumption concl)
         fun find_input_steps_and_inline [] = []
           | find_input_steps_and_inline
               (VeriT_Node {id = id', rule, prems, concl, ...} :: steps) =
             if rule = input_rule then
               find_input_steps_and_inline (map (inline_assumption concl id') steps)
             else
               mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps
 
         fun free_bounds bounds (concl) =
           fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl
         val subproof = subproof
           |> flat o map linearize
           |> map (map_node_concl (fold add_assumption (assms @ inputs)))
           |> map (map_node_concl (free_bounds (bounds @ bounds')))
           |> find_input_steps_and_inline
         val concl = free_bounds bounds concl
       in
         subproof @ [mk_node id rule prems proof_ctxt concl]
       end
   in linearize end
 
 fun rule_of (VeriT_Replay_Node {rule,...}) = rule
 fun subproof_of (VeriT_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof
 
 
 (* Massage Skolems for Sledgehammer.
 
 We have to make sure that there is an "arrow" in the graph for skolemization steps.
 
 
 A. The normal easy case
 
 This function detects the steps of the form
   P \<longleftrightarrow> Q :skolemization
   Q       :resolution with P
 and replace them by
   Q       :skolemization
 Throwing away the step "P \<longleftrightarrow> Q" completely. This throws away a lot of information, but it does not
 matter too much for Sledgehammer.
 
 
 B. Skolems in subproofs
 Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer
 does not support more features like definitions. veriT is able to generate proofs with skolemization
 happening in subproofs inside the formula.
   (assume "A \<or> P"
    ...
    P \<longleftrightarrow> Q :skolemization in the subproof
    ...)
   hence A \<or> P \<longrightarrow> A \<or> Q :lemma
   ...
   R :something with some rule
 and replace them by
   R :skolemization with some rule
 Without any subproof
 *)
 fun remove_skolem_definitions_proof steps =
   let
     fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\<open>HOL.eq\<close>, typ) $ arg1) $ arg2)) =
        judgement $ ((Const(\<^const_name>\<open>HOL.implies\<close>, typ) $ arg1) $ arg2)
      | replace_equivalent_by_imp a = a (*This case is probably wrong*)
     fun remove_skolem_definitions (VeriT_Replay_Node {id = id, rule = rule, args = args,
          prems = prems,
         proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts,
         declarations = declarations,
         subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) =
     let
       val prems = prems
         |> filter_out (member (op =) prems_to_remove)
       val trivial_step = is_SH_trivial rule
       fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st)
              else fold has_skolem_substep (subproof_of st) NONE
         | has_skolem_substep _ a = a
       val promote_to_skolem = exists (fn t => member (op =) skolems t) prems
       val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE
       val promote_step = promote_to_skolem orelse promote_from_assms
       val skolem_step_to_skip = is_skolemization rule orelse
         (promote_from_assms andalso length prems > 1)
       val is_skolem = is_skolemization rule orelse promote_step
       val prems = prems
         |> filter_out (fn t => member (op =) skolems t)
         |> is_skolem ? filter_out (String.isPrefix id)
       val rule = (if promote_step then default_skolem_rule else rule)
       val subproof = subproof
         |> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*)
         |> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems)))
              (*no new definitions in subproofs*)
         |> flat
       val concl = concl
         |> is_skolem ? replace_equivalent_by_imp
       val step = (if skolem_step_to_skip orelse rule = veriT_def orelse trivial_step then []
         else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations
             (vars, assms', extra_assms', subproof)
           |> single)
       val defs = (if rule = veriT_def orelse trivial_step then id :: prems_to_remove
          else prems_to_remove)
       val skolems = (if skolem_step_to_skip then id :: skolems else skolems)
     in
       (step, (defs, skolems))
     end
   in
     fold_map remove_skolem_definitions steps ([], [])
     |> fst
     |> flat
   end
 
 local
   fun import_proof_and_post_process typs funs lines ctxt =
     let
       val compress = SMT_Config.compress_verit_proofs ctxt
       val smtlib_lines_without_qm =
         lines
         |> map single
         |> map SMTLIB.parse
         |> map remove_all_qm2
       val (raw_steps, _, _) =
         parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding
 
       fun process step (cx, cx') =
         let fun postprocess step (cx, cx') =
           let val (step, cx) = postprocess_proof compress ctxt step cx
           in (step, (cx, cx')) end
         in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end
       val step =
         (empty_context ctxt typs funs, [])
         |> fold_map process raw_steps
         |> (fn (steps, (cx, _)) => (flat steps, cx))
         |> compress? apfst combine_proof_steps
     in step end
 in
 
 fun parse typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
     val t = u
        |> remove_skolem_definitions_proof
        |> flat o (map linearize_proof)
     fun node_to_step (VeriT_Node {id, rule, prems, concl, ...}) =
       mk_step id rule prems [] concl []
   in
     (map node_to_step t, ctxt_of env)
   end
 
 fun parse_replay typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
     val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u)
   in
     (u, ctxt_of env)
   end
 end
 
 end;
diff --git a/src/HOL/Tools/SMT/z3_interface.ML b/src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML
+++ b/src/HOL/Tools/SMT/z3_interface.ML
@@ -1,195 +1,195 @@
 (*  Title:      HOL/Tools/SMT/z3_interface.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Interface to Z3 based on a relaxed version of SMT-LIB.
 *)
 
 signature Z3_INTERFACE =
 sig
   val smtlib_z3C: SMT_Util.class
 
   datatype sym = Sym of string * sym list
   type mk_builtins = {
     mk_builtin_typ: sym -> typ option,
     mk_builtin_num: theory -> int -> typ -> cterm option,
     mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
   val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic
   val mk_builtin_typ: Proof.context -> sym -> typ option
   val mk_builtin_num: Proof.context -> int -> typ -> cterm option
   val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
 
   val is_builtin_theory_term: Proof.context -> term -> bool
 end;
 
 structure Z3_Interface: Z3_INTERFACE =
 struct
 
 val z3C = ["z3"]
 
-val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ SMTLIB_Interface.bvsmlibC @ z3C
 
 
 (* interface *)
 
 local
   fun translate_config ctxt =
     {order = SMT_Util.First_Order,
-     logic = K "",
+     logic = K (K ""),
      fp_kinds = [BNF_Util.Least_FP],
      serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
 
   fun is_div_mod \<^Const_>\<open>divide \<^Type>\<open>int\<close>\<close> = true
     | is_div_mod \<^Const>\<open>modulo \<^Type>\<open>int\<close>\<close> = true
     | is_div_mod _ = false
 
   val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
 
   fun add_div_mod _ (thms, extra_thms) =
     if have_int_div_mod thms orelse have_int_div_mod extra_thms then
       (thms, @{thms div_as_z3div mod_as_z3mod} @ extra_thms)
     else (thms, extra_thms)
 
   val setup_builtins =
     SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, "*") #>
     SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3div\<close>, "div") #>
     SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3mod\<close>, "mod")
 in
 
 val _ = Theory.setup (Context.theory_map (
   setup_builtins #>
   SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
   SMT_Translate.add_config (smtlib_z3C, translate_config)))
 
 end
 
 
 (* constructors *)
 
 datatype sym = Sym of string * sym list
 
 
 (** additional constructors **)
 
 type mk_builtins = {
   mk_builtin_typ: sym -> typ option,
   mk_builtin_num: theory -> int -> typ -> cterm option,
   mk_builtin_fun: theory -> sym -> cterm list -> cterm option }
 
 fun chained _ [] = NONE
   | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
 
 fun chained_mk_builtin_typ bs sym =
   chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs
 
 fun chained_mk_builtin_num ctxt bs i T =
   let val thy = Proof_Context.theory_of ctxt
   in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end
 
 fun chained_mk_builtin_fun ctxt bs s cts =
   let val thy = Proof_Context.theory_of ctxt
   in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
 
 fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
 
 structure Mk_Builtins = Generic_Data
 (
   type T = (int * mk_builtins) list
   val empty = []
   fun merge data = Ord_List.merge fst_int_ord data
 )
 
 fun add_mk_builtins mk = Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
 
 fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
 
 
 (** basic and additional constructors **)
 
 fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME \<^typ>\<open>bool\<close>
   | mk_builtin_typ _ (Sym ("Int", _)) = SOME \<^typ>\<open>int\<close>
   | mk_builtin_typ _ (Sym ("bool", _)) = SOME \<^typ>\<open>bool\<close>  (*FIXME: legacy*)
   | mk_builtin_typ _ (Sym ("int", _)) = SOME \<^typ>\<open>int\<close>  (*FIXME: legacy*)
   | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
 
 fun mk_builtin_num _ i \<^typ>\<open>int\<close> = SOME (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> i)
   | mk_builtin_num ctxt i T =
       chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
 
 val mk_true = \<^cterm>\<open>\<not> False\<close>
 val mk_false = \<^cterm>\<open>False\<close>
 val mk_not = Thm.apply \<^cterm>\<open>HOL.Not\<close>
 val mk_implies = Thm.mk_binop \<^cterm>\<open>HOL.implies\<close>
 val mk_iff = Thm.mk_binop \<^cterm>\<open>(=) :: bool \<Rightarrow> _\<close>
 val conj = \<^cterm>\<open>HOL.conj\<close>
 val disj = \<^cterm>\<open>HOL.disj\<close>
 
 fun mk_nary _ cu [] = cu
   | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
 
 val eq = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>HOL.eq\<close> Thm.dest_ctyp0
 fun mk_eq ct cu = Thm.mk_binop (SMT_Util.instT' ct eq) ct cu
 
 val if_term =
   SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>If\<close> (Thm.dest_ctyp0 o Thm.dest_ctyp1)
 fun mk_if cc ct = Thm.mk_binop (Thm.apply (SMT_Util.instT' ct if_term) cc) ct
 
 val access = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>fun_app\<close> Thm.dest_ctyp0
 fun mk_access array = Thm.apply (SMT_Util.instT' array access) array
 
 val update =
   SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>fun_upd\<close> (Thm.dest_ctyp o Thm.dest_ctyp0)
 fun mk_update array index value =
   let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
   in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
 
 val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: int \<Rightarrow> _\<close>
 val add = \<^cterm>\<open>(+) :: int \<Rightarrow> _\<close>
 val int0 = Numeral.mk_cnumber \<^ctyp>\<open>int\<close> 0
 val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: int \<Rightarrow> _\<close>
 val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: int \<Rightarrow> _\<close>
 val mk_div = Thm.mk_binop \<^cterm>\<open>z3div\<close>
 val mk_mod = Thm.mk_binop \<^cterm>\<open>z3mod\<close>
 val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: int \<Rightarrow> _\<close>
 val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: int \<Rightarrow> _\<close>
 
 fun mk_builtin_fun ctxt sym cts =
   (case (sym, cts) of
     (Sym ("true", _), []) => SOME mk_true
   | (Sym ("false", _), []) => SOME mk_false
   | (Sym ("not", _), [ct]) => SOME (mk_not ct)
   | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
   | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
   | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
   | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
   | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
   | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu))
   | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
   | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *)
   | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
   | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
   | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
   | _ =>
     (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
       (Sym ("+", _), SOME \<^typ>\<open>int\<close>, _) => SOME (mk_nary add int0 cts)
     | (Sym ("-", _), SOME \<^typ>\<open>int\<close>, [ct]) => SOME (mk_uminus ct)
     | (Sym ("-", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_sub ct cu)
     | (Sym ("*", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_mul ct cu)
     | (Sym ("div", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_div ct cu)
     | (Sym ("mod", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_mod ct cu)
     | (Sym ("<", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_lt ct cu)
     | (Sym ("<=", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_le ct cu)
     | (Sym (">", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_lt cu ct)
     | (Sym (">=", _), SOME \<^typ>\<open>int\<close>, [ct, cu]) => SOME (mk_le cu ct)
     | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts))
 
 
 (* abstraction *)
 
 fun is_builtin_theory_term ctxt t =
   if SMT_Builtin.is_builtin_num ctxt t then true
   else
     (case Term.strip_comb t of
       (Const c, ts) => SMT_Builtin.is_builtin_fun ctxt c ts
     | _ => false)
 
 end;