sig
  type driver
  val load_driver_file_and_extras :
    Whyconf.main ->
    Env.env ->
    extra_dir:string option ->
    string -> (string * string list) list -> Driver.driver
  val load_driver_for_prover :
    Whyconf.main -> Env.env -> Whyconf.config_prover -> Driver.driver
  val resolve_driver_name :
    Whyconf.main -> string -> extra_dir:string option -> string -> string
  val file_of_task : Driver.driver -> string -> string -> Task.task -> string
  val file_of_theory : Driver.driver -> string -> Theory.theory -> string
  val get_filename :
    Driver.driver ->
    input_file:string -> theory_name:string -> goal_name:string -> string
  val print_task :
    ?old:Stdlib.in_channel ->
    Driver.driver -> Stdlib.Format.formatter -> Task.task -> unit
  val print_theory :
    ?old:Stdlib.in_channel ->
    Driver.driver -> Stdlib.Format.formatter -> Theory.theory -> unit
  val prove_task :
    command:string ->
    config:Whyconf.main ->
    limits:Call_provers.resource_limits ->
    ?old:string ->
    ?inplace:bool ->
    ?interactive:bool ->
    Driver.driver -> Task.task -> Call_provers.prover_call
  val prepare_task : Driver.driver -> Task.task -> Task.task
  val print_task_prepared :
    ?old:Stdlib.in_channel ->
    Driver.driver ->
    Stdlib.Format.formatter -> Task.task -> Printer.printing_info
  val prove_task_prepared :
    command:string ->
    config:Whyconf.main ->
    limits:Call_provers.resource_limits ->
    ?old:string ->
    ?inplace:bool ->
    ?interactive:bool ->
    Driver.driver -> Task.task -> Call_provers.prover_call
  val prove_buffer_prepared :
    command:string ->
    config:Whyconf.main ->
    limits:Call_provers.resource_limits ->
    ?input_file:string ->
    ?theory_name:string ->
    ?goal_name:string ->
    ?get_model:Printer.printing_info ->
    Driver.driver -> Stdlib.Buffer.t -> Call_provers.prover_call
  val syntax_map : Driver.driver -> Printer.syntax_map
  val meta_get_counterexmp : Theory.meta
  val get_counterexmp : Task.task -> bool
end