Module Wp.Prover

val simplify : ?start:( Wpo.t -> unit ) -> ?result:( Wpo.t -> VCS.prover -> VCS.result -> unit ) -> Wpo.t -> bool Frama_c_kernel.Task.task
val prove : Wpo.t -> ?config:VCS.config -> ?mode:VCS.mode -> ?start:( Wpo.t -> unit ) -> ?progress:( Wpo.t -> string -> unit ) -> ?result:( Wpo.t -> VCS.prover -> VCS.result -> unit ) -> VCS.prover -> bool Frama_c_kernel.Task.task
val spawn : Wpo.t -> delayed:bool -> ?config:VCS.config -> ?start:( Wpo.t -> unit ) -> ?progress:( Wpo.t -> string -> unit ) -> ?result:( Wpo.t -> VCS.prover -> VCS.result -> unit ) -> ?success:( Wpo.t -> VCS.prover option -> unit ) -> ?pool:Frama_c_kernel.Task.pool -> (VCS.mode * VCS.prover) list -> unit