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 is_trivial : Wp.VC.t -> bool   val get_formula : Wp.VC.t -> Wp.Lang.F.pred   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 ->     ?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 ->     ?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) ->     (Wp.VCS.mode * Wp.VCS.prover) list -> unit   val server : ?procs:int -> unit -> Task.server   val command : Wp.VC.t Bag.t -> unit end