sig
  val add_specific_equality :
    for_tau:(Lang.tau -> bool) -> mk_new_eq:Lang.F.binop -> unit
  val prove :
    ?timeout:int ->
    ?steplimit:int -> prover:Why3Provers.t -> Wpo.t -> VCS.result Task.task
  type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
  val set_mode : ProverWhy3.mode -> unit
  val get_mode : unit -> ProverWhy3.mode
  val get_hits : unit -> int
  val get_miss : unit -> int
  val get_removed : unit -> int
  val cleanup_cache : mode:ProverWhy3.mode -> unit
end