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