Module ProverWhy3

module ProverWhy3: sig .. end

type goal = {
   file : string;
   theory : string;
   goal : string;
}
val assemble_goal : Wpo.t -> (string list * goal) option

None if the po is trivial

val prove : ?timeout:int -> prover:string -> Wpo.t -> VCS.result Task.task

The string must be a valid why3 prover identifier Return NoResult if it is already proved by Qed

module Goal: sig .. end