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