sig
  val version : string
  val config : unit -> Why3.Whyconf.config
  val configure : unit -> unit
  val set_procs : int -> unit
  type t = Why3.Whyconf.prover
  val find_opt : string -> Why3Provers.t option
  type fallback =
      Exact of Why3Provers.t
    | Fallback of Why3Provers.t
    | NotFound
  val find_fallback : string -> Why3Provers.fallback
  val print_why3 : Why3Provers.t -> string
  val print_wp : Why3Provers.t -> string
  val title : Why3Provers.t -> string
  val name : Why3Provers.t -> string
  val compare : Why3Provers.t -> Why3Provers.t -> int
  val provers : unit -> Why3Provers.t list
  val provers_set : unit -> Why3.Whyconf.Sprover.t
  val is_available : Why3Provers.t -> bool
  val is_mainstream : Why3Provers.t -> bool
  val has_shortcut : Why3Provers.t -> string -> bool
end