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