diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml index e9bb77dc5b58e7db6a8c749cb56b436ddcc6f753..02390f98b1457e6db09d01ab35b71303f18d0f7e 100644 --- a/src/plugins/wp/ProverTask.ml +++ b/src/plugins/wp/ProverTask.ml @@ -292,9 +292,14 @@ let getprocs = function Some n -> n | None -> Wp_parameters.Procs.get () let server ?procs () = match !server with | Some s -> - Task.set_procs s (getprocs procs) ; s + let np = getprocs procs in + Task.set_procs s np ; + Why3Provers.set_procs np ; + s | None -> - let s = Task.server ~procs:(getprocs procs) () in + let np = getprocs procs in + let s = Task.server ~procs:np () in + Why3Provers.set_procs np ; Task.on_server_stop s Proof.savescripts ; server := Some s ; s diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml index 1bb6c8bd1834057ffb792bfb0ba0a0f1d03cf659..7499579fe54f7bb617847a092818a80cf72cac7b 100644 --- a/src/plugins/wp/Why3Provers.ml +++ b/src/plugins/wp/Why3Provers.ml @@ -35,6 +35,8 @@ let cfg = lazy let version = Why3.Config.version let config () = Lazy.force cfg +let set_procs = Why3.Controller_itp.set_session_max_tasks + let configure = let todo = ref true in begin fun () -> diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli index a68eeb567d8caab7089bd8d82af71bfbfb7c1a25..d08bf2d0337eb3f917644bacabc24d738aa61309 100644 --- a/src/plugins/wp/Why3Provers.mli +++ b/src/plugins/wp/Why3Provers.mli @@ -23,6 +23,7 @@ val version : string val config : unit -> Why3.Whyconf.config val configure : unit -> unit +val set_procs : int -> unit type t = Why3.Whyconf.prover