src/HOL/Tools/SMT/smt_solver.ML

      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,
+     good_slices: (int * string) list,
      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
+  val good_slices: Proof.context -> string -> (int * string) list
 
   (*filter*)
   val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list ->
     int -> Time.time -> parsed_proof
 

    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,
+   good_slices: (int * string) list,
    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 *)
 
 type solver_info = {
   command: unit -> string list,
   smt_options: (string * string) list,
-  default_max_relevant: int,
+  good_slices: (int * string) list,
   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}
 

     | (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,
+fun add_solver ({name, class, avail, command, options, smt_options, good_slices, 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,
+      good_slices = good_slices,
       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

 
 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
+val good_slices = #good_slices 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