sig
  type t
  val get_id : Wp.VC.t -> string
  val get_model : Wp.VC.t -> Wp.Model.t
  val get_description : Wp.VC.t -> string
  val get_property : Wp.VC.t -> Property.t
  val get_result : Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result
  val get_results : Wp.VC.t -> (Wp.VCS.prover * Wp.VCS.result) list
  val get_logout : Wp.VC.t -> Wp.VCS.prover -> string
  val get_logerr : Wp.VC.t -> Wp.VCS.prover -> string
  val get_sequent : Wp.VC.t -> Wp.Conditions.sequent
  val get_formula : Wp.VC.t -> Wp.Lang.F.pred
  val is_trivial : Wp.VC.t -> bool
  val is_proved : Wp.VC.t -> bool
  val clear : unit -> unit
  val proof : Property.t -> Wp.VC.t list
  val remove : Property.t -> unit
  val iter_ip : (Wp.VC.t -> unit) -> Property.t -> unit
  val iter_kf :
    (Wp.VC.t -> unit) -> ?bhv:string list -> Kernel_function.t -> unit
  val generate_ip : ?model:string -> Property.t -> Wp.VC.t Bag.t
  val generate_kf :
    ?model:string -> ?bhv:string list -> Kernel_function.t -> Wp.VC.t Bag.t
  val generate_call : ?model:string -> Cil_types.stmt -> Wp.VC.t Bag.t
  val prove :
    Wp.VC.t ->
    ?config:Wp.VCS.config ->
    ?mode:Wp.VCS.mode ->
    ?start:(Wp.VC.t -> unit) ->
    ?callin:(Wp.VC.t -> Wp.VCS.prover -> unit) ->
    ?callback:(Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
    Wp.VCS.prover -> bool Task.task
  val spawn :
    Wp.VC.t ->
    ?config:Wp.VCS.config ->
    ?start:(Wp.VC.t -> unit) ->
    ?callin:(Wp.VC.t -> Wp.VCS.prover -> unit) ->
    ?callback:(Wp.VC.t -> Wp.VCS.prover -> Wp.VCS.result -> unit) ->
    ?success:(Wp.VC.t -> Wp.VCS.prover option -> unit) ->
    ?pool:Task.pool -> (Wp.VCS.mode * Wp.VCS.prover) list -> unit
  val server : ?procs:int -> unit -> Task.server
  val command : Wp.VC.t Bag.t -> unit
end