sig
  type why_prover = {
    command : string;
    driver : Why3.Driver.driver;
    limits : Why3.Call_provers.resource_limits;
  }
  val mk_why_prover :
    command:string ->
    Why3.Driver.driver ->
    Why3.Call_provers.resource_limits -> Rac.Why.why_prover
  val mk_check_term :
    ?metas:(Why3.Theory.meta * Why3.Theory.meta_arg list) list ->
    ?trans:Why3.Task.task Why3.Trans.tlist ->
    ?why_prover:Rac.Why.why_prover ->
    ?oracle_quant_var:Rac.oracle_quant_var ->
    config:Why3.Whyconf.config ->
    elim_eps:Why3.Task.task Why3.Trans.trans ->
    unit -> Why3.Pinterp_core.check_term
  val mk_check_term_lit :
    Why3.Whyconf.config ->
    Why3.Env.env ->
    ?metas:(string * string option) list ->
    ?trans:string ->
    why_prover:(string * Why3.Call_provers.resource_limits) option ->
    ?oracle_quant_var:Rac.oracle_quant_var ->
    unit -> Why3.Pinterp_core.check_term
  val mk_compute_term :
    ?metas:(Why3.Theory.meta * Why3.Theory.meta_arg list) list ->
    ?trans:Why3.Task.task list Why3.Trans.trans ->
    ?oracle_quant_var:Rac.oracle_quant_var ->
    unit -> Why3.Pinterp_core.compute_term
  val mk_compute_term_lit :
    Why3.Env.env ->
    ?metas:(string * string option) list ->
    ?trans:string ->
    ?oracle_quant_var:Rac.oracle_quant_var ->
    unit -> Why3.Pinterp_core.compute_term
end