ProverTask (frama-c-wp.Wp.ProverTask)

val server : ?procs:int -> unit -> Frama_c_kernel.Task.server

If provided, the number of procs is forwarded to the Why3 and the server

val simplify : 
  ?start:(Wpo.t -> unit) ->
  ?result:(Wpo.t -> Prover.t -> VCS.result -> unit) ->
  ?commit:bool ->
  Wpo.t ->
  bool Frama_c_kernel.Task.task

val prove : 
  Wpo.t ->
  ?config:VCS.config ->
  ?mode:Prover.InteractiveMode.t ->
  ?start:(Wpo.t -> unit) ->
  ?progress:(Wpo.t -> string -> unit) ->
  ?result:(Wpo.t -> Prover.t -> VCS.result -> unit) ->
  Prover.t ->
  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 -> Prover.t -> VCS.result -> unit) ->
  ?success:(Wpo.t -> Prover.t option -> unit) ->
  (Prover.InteractiveMode.t * Prover.t) list ->
  unit