diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index a6980515b769b68a92569eddae7f031e06dbfadb..651c8a18ed53fae56d95eb3e837ad62a8f7623b8 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -297,7 +297,7 @@ class pane (gprovers : GuiConfig.provers) =
       | Proof p ->
         let main = ProofEngine.main p in
         let json = ProofScript.encode (ProofEngine.script p) in
-        ProofSession.save main json ;
+        ProofSession.save ~stdout:false main json ;
         ProofEngine.set_saved p true ;
         self#update
           (*
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 9a53e78ee79e4e6c7bca6cc621fe7623011d302c..d102a9a49bb7e70555cc1233518f665514ad4fba 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/src/plugins/wp/ProofSession.ml
@@ -93,11 +93,15 @@ let remove wpo =
       Hashtbl.replace files f NoScript ;
     end
 
-let save wpo js =
+let save ~stdout wpo js =
   let empty =
     match js with
     | `Null | `List [] | `Assoc [] -> true
     | _ -> false in
+  if stdout then
+    Wp_parameters.result "Proof script for %s:@.%a"
+      wpo.po_gid (Json.save_formatter ~pretty:true) js
+  else
   if empty then remove wpo else
     match get wpo with
     | Script f ->
diff --git a/src/plugins/wp/ProofSession.mli b/src/plugins/wp/ProofSession.mli
index 939e82f104b3055e465f5244f0e3e34aa1cca3d8..9d0f127fca16d2f67f831e991be1203587313d4b 100644
--- a/src/plugins/wp/ProofSession.mli
+++ b/src/plugins/wp/ProofSession.mli
@@ -29,7 +29,7 @@ val pp_script_for : Format.formatter -> Wpo.t -> unit
 
 val get : Wpo.t -> script
 val exists : Wpo.t -> bool
-val save : Wpo.t -> Json.t -> unit
+val save : stdout:bool -> Wpo.t -> Json.t -> unit
 val load : Wpo.t -> Json.t
 val remove : Wpo.t -> unit
 
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 05448172e2decf5ce103e76f4682730982c87fcd..879fa822652884e147de9e388a7282b088515d57 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -507,10 +507,10 @@ let has_proof wpo =
       (Hashtbl.add proofs wid ok ; ok)
     else false
 
-let save wpo =
+let save ~stdout wpo =
   let script = ProofEngine.script (ProofEngine.proof ~main:wpo) in
   Hashtbl.remove proofs wpo.Wpo.po_gid ;
-  ProofSession.save wpo (ProofScript.encode script)
+  ProofSession.save ~stdout wpo (ProofScript.encode script)
 
 let get wpo =
   match ProofEngine.get wpo with
diff --git a/src/plugins/wp/ProverScript.mli b/src/plugins/wp/ProverScript.mli
index 5038a97aec40cf3d3b81fc0ce14b650c05c11493..de3880d615b59aa944cb521ec57c195ea5f951c7 100644
--- a/src/plugins/wp/ProverScript.mli
+++ b/src/plugins/wp/ProverScript.mli
@@ -53,4 +53,4 @@ val search :
   unit
 
 val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
-val save : Wpo.t -> unit
+val save : stdout:bool -> Wpo.t -> unit
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 45a5e0af86e077685a0aaa15d095721e33eae09a..be99e86a3eb42d964be8794a86ce264a530c7a66 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1308,6 +1308,8 @@ See \texttt{-wp-interactive <mode>} option for details.
   (see \verb+-wp-smoke-tests+, defaults to 5 seconds).
 \item[\tt -wp-interactive-timeout <n>] sets the timeout (in seconds) for checking
   edited scripts with interactive provers (defaults to 30 seconds).
+\item[\tt -wp-(no)-script-on-stdout] displays generated proof scripts on stdout
+  instead of saving them on disk (default is: \texttt{no}).
 \item[\tt -wp-time-extra <n>] additional time allocated to provers when
   replaying a script. This is used to cope with variable machine load.
   Default is \verb+5s+.
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index e2a503d3ab70f561d5319eef678f34a0d548fd85..37197fd2a5acbc874e1edb1dd06a7a0b32458990 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -478,6 +478,7 @@ let do_list_scheduled_result () =
 type script = {
   mutable tactical : bool ;
   mutable update : bool ;
+  mutable on_stdout : bool ;
   mutable depth : int ;
   mutable width : int ;
   mutable backtrack : int ;
@@ -555,7 +556,7 @@ let dump_strategies =
                )))
 
 let default_script_mode () = {
-  tactical = false ; update=false ; provers = [] ;
+  tactical = false ; update=false ; on_stdout = false ; provers = [] ;
   depth=0 ; width = 0 ; auto=[] ; backtrack = 0 ;
 }
 
@@ -609,16 +610,17 @@ let do_update_session ~script goals =
                   | ProofScript.Tactic(n,_,_) -> n=0
                   | ProofScript.Error _ -> false in
                 let strategy = List.filter keep scripts in
+                let stdout = script.on_stdout in
                 if strategy <> [] then
                   begin
                     incr updated ;
-                    ProofSession.save goal (ProofScript.encode strategy)
+                    ProofSession.save ~stdout goal (ProofScript.encode strategy)
                   end
                 else
                 if not (ProofSession.exists goal) then
                   begin
                     incr invalid ;
-                    ProofSession.save goal (ProofScript.encode scripts)
+                    ProofSession.save ~stdout goal (ProofScript.encode scripts)
                   end
               end
         end goals ;
@@ -650,6 +652,9 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
     script.tactical <- tip ;
     script.update <- tip ;
   end ;
+  begin
+    script.on_stdout <- Wp_parameters.ScriptOnStdout.get ();
+  end ;
   let spawned = script.tactical || script.provers <> [] in
   begin
     if spawned then do_list_scheduled goals ;
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index da153c620d01ac5748f1fb26e4d9998e24888f3a..1c78f06e11e80018180777668c123942cf82c868 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,3 +1,5 @@
 PLUGIN: wp
+MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@
+MACRO: USING_WP_SESSION -wp-session @WP_SESSION@
 CMD: @frama-c@ -wp -wp-prover none -wp-print -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
 OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 395f0c6f754e0898ef3c7c570de157da9e5c3b4f..895b3f4d8bf4111e4f6df1692cdf3675fce834b5 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,3 +1,5 @@
 PLUGIN: wp
-CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report @PTEST_SUITE_DIR@/../qualif.report -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@
+MACRO: WP_SESSION @PTEST_DIR@/@PTEST_NAME@.@PTEST_NUMBER@.session@PTEST_CONFIG@
+MACRO: USING_WP_SESSION -wp-session @WP_SESSION@
+CMD: @frama-c@ -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache-env -wp-cache replay @PTEST_FILE@
 OPT:
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
index c55cf4d5c8907db89f1cb70eb449041ace623a33..5ffa367b087766ae34ec9d64007ae2c7193dda1b 100644
--- a/src/plugins/wp/tests/wp_acsl/checks.i
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -1,7 +1,7 @@
 /* run.config
-PLUGIN: wp,rtegen,scope,eva,report
+PLUGIN: @PTEST_PLUGIN@,rtegen,scope,eva,report,inout
    OPT: -then -eva -then -report
-PLUGIN: wp,rtegen
+PLUGIN: @PTEST_PLUGIN@,rtegen
    OPT: -wp-prop=@check
    OPT: -wp-prop=-@check
 */
diff --git a/src/plugins/wp/tests/wp_eva/test_config b/src/plugins/wp/tests/wp_eva/test_config
index b17ba9c087756386fee7b149e7f598e0ebbad315..5207a5c15a5b5a8fc714e645b5e5562340ca8d51 100644
--- a/src/plugins/wp/tests/wp_eva/test_config
+++ b/src/plugins/wp/tests/wp_eva/test_config
@@ -1 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -wp -wp-print -wp-prover none -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell
+PLUGIN: @PTEST_PLUGIN@,eva,scope,inout,reduc
+CMD: @frama-c@ -no-autoload-plugins -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -wp -wp-print -wp-prover none -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell
diff --git a/src/plugins/wp/tests/wp_eva/test_config_qualif b/src/plugins/wp/tests/wp_eva/test_config_qualif
index 5cc6f72566ce5f45d29d47a3ee4d208b904d271b..b9d5bf904c05cb9b2bfb19a84d135b651b8cecf1 100644
--- a/src/plugins/wp/tests/wp_eva/test_config_qualif
+++ b/src/plugins/wp/tests/wp_eva/test_config_qualif
@@ -1,2 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -then -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@
+PLUGIN: @PTEST_PLUGIN@,eva,scope,inout,reduc
+CMD: @frama-c@ -no-autoload-plugins -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -then -wp -wp-par 1 -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache-env -wp-cache replay @PTEST_FILE@
 OPT:
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json b/src/plugins/wp/tests/wp_gallery/binary-multiplication.0.session_qualif/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
similarity index 100%
rename from src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
rename to src/plugins/wp/tests/wp_gallery/binary-multiplication.0.session_qualif/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
index 6321440d676cbb0d589ad5932a81008fde0237f8..c365c6f448277fca904f52231225bc5af90dc7b4 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
@@ -3,7 +3,8 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack
+
+   OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack @USING_WP_SESSION@
 */
 
 // The use '-wp-prover=z3,why3:alt-ergo' or using Alt-Ergo 2.3.0 gives better results.
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/script/init_assigns_part3.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/script/init_assigns_part3.json
deleted file mode 100644
index 72aa1adcfdfe3a278be705aa18e1bb3bdab22252..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/script/init_assigns_part3.json
+++ /dev/null
@@ -1,23 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 16 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_147",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 1": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 2": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 3": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 4": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 5": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 6": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 7": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 8": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 9": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 10": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 11": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 12": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 13": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 14": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 15": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 16": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Upper 16": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
rename to src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
rename to src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
index 0b7d5eb92288c72651f118c1d584354728edfba9..e2e5cf5fba38b6d8860003cd779ae364c30805a3 100644
--- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
+++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i
@@ -3,7 +3,8 @@
  */
 
 /* run.config_qualif
-   OPT: -wp-prover script,alt-ergo
+
+   OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
  */
 
 typedef unsigned short ushort;
diff --git a/src/plugins/wp/tests/wp_plugin/config.sh b/src/plugins/wp/tests/wp_plugin/config.sh
index 5df845aecbc17f42e8671db4f388ed8e5cd44560..64004c51ddea7ee92b065d6e41e86d3a8f10019c 100755
--- a/src/plugins/wp/tests/wp_plugin/config.sh
+++ b/src/plugins/wp/tests/wp_plugin/config.sh
@@ -3,13 +3,9 @@
 ERGO=`alt-ergo -version`
 WHY3=`why3 --version`
 
-# sed command to prevent from diffs about the date: "(Month Year)" 
-COQC=`coqc --version | head -1 | sed -e 's: ([A-Z][a-z]* [0-9]*)$::'`
-
 echo "----------------------------------------------------------"
 echo "WP Requirements for Qualif Tests (3)"
 echo "----------------------------------------------------------"
 echo "1. The Alt-Ergo theorem prover, version ${ERGO}"
 echo "2. The ${WHY3}"
-echo "3. ${COQC}"
 echo "----------------------------------------------------------"
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
index 0b533489441b73bdce8cad8c2a0de1159e21b778..d270228212ed09c31e00ddc0500dd1623c87c1bd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
@@ -2,7 +2,7 @@
 [kernel] Parsing unroll.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] unroll.i:20: Warning: Missing assigns clause (assigns 'everything' instead)
+[wp] unroll.i:21: Warning: Missing assigns clause (assigns 'everything' instead)
 ------------------------------------------------------------
   Function unrolled_loop
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index 8262db901edcbcaff5e750ec62f8b2abc6e3b159..fc2bd44fdd5bf6ac2dc4cfe36213ff7ff1950c6a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -3,5 +3,4 @@ WP Requirements for Qualif Tests (3)
 ----------------------------------------------------------
 1. The Alt-Ergo theorem prover, version 2.2.0
 2. The Why3 platform, version 1.4.0
-3. The Coq Proof Assistant, version 8.13.0
 ----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
index c36ca9273ec6c6b60b340687598d8d1177e607e6..b7eb8ace826c22a6387619acb232ad4bc4c75b8d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
@@ -2,7 +2,7 @@
 [kernel] Parsing unroll.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] unroll.i:20: Warning: Missing assigns clause (assigns 'everything' instead)
+[wp] unroll.i:21: Warning: Missing assigns clause (assigns 'everything' instead)
 [wp] 1 goal scheduled
 [wp] [Script] Goal typed_unrolled_loop_ensures_zero : Valid
 [wp] Proved goals:    1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index 08ad6804231703160d824e710dd98a9abfbc47f0..23336fa9a008a0c3304ce41642a162894de69be7 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,5 +1,5 @@
 /* run.config_qualif
-PLUGIN: wp,rtegen,eva,scope
+PLUGIN: @PTEST_PLUGIN@,rtegen,eva,scope,inout
    OPT: -no-wp -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
  */
 /* run.config
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json b/src/plugins/wp/tests/wp_plugin/unroll.0.session_qualif/script/unrolled_loop_ensures_zero.json
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json
rename to src/plugins/wp/tests/wp_plugin/unroll.0.session_qualif/script/unrolled_loop_ensures_zero.json
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index 8e34f8f66edd7b4183b97299107d84c6b78c391c..021ceb05d916d53f2b67bce5c86c714481e51d4e 100644
--- a/src/plugins/wp/tests/wp_plugin/unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/unroll.i
@@ -3,7 +3,8 @@
 */
 
 /* run.config_qualif
-   OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script
+
+   OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script @USING_WP_SESSION@
 */
 
 enum {Max = 16};
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
rename to src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.i b/src/plugins/wp/tests/wp_plugin/unsigned.i
index b48f75fbbc3d9925d4f25f00ca77f8d7a292c9b0..a4075988005d6bb74ee68e849bcf67ae8789720f 100644
--- a/src/plugins/wp/tests/wp_plugin/unsigned.i
+++ b/src/plugins/wp/tests/wp_plugin/unsigned.i
@@ -3,7 +3,8 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover script
+
+   OPT: -wp-prover script @USING_WP_SESSION@
 */
 
 /*@
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_ensures.json b/src/plugins/wp/tests/wp_tip/clear.0.session/script/clear_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_ensures.json
rename to src/plugins/wp/tests/wp_tip/clear.0.session/script/clear_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json b/src/plugins/wp/tests/wp_tip/clear.0.session/script/clear_in_step_check.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json
rename to src/plugins/wp/tests/wp_tip/clear.0.session/script/clear_in_step_check.json
diff --git a/src/plugins/wp/tests/wp_tip/clear.i b/src/plugins/wp/tests/wp_tip/clear.i
index 38bb4997fe998982b6335db4dcbcc26d541cd45e..c4d1b5f53767129850bb885e4ca5eb6261a9d740 100644
--- a/src/plugins/wp/tests/wp_tip/clear.i
+++ b/src/plugins/wp/tests/wp_tip/clear.i
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
+
+   OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
 */
 /* run.config_qualif
    DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
rename to src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
rename to src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
rename to src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
diff --git a/src/plugins/wp/tests/wp_tip/induction.i b/src/plugins/wp/tests/wp_tip/induction.i
index 5ff948c0f86fd357cbf3cc3393e3a402887f08dd..df4e3fa378d1c13704c8af6e64803040b93b565f 100644
--- a/src/plugins/wp/tests/wp_tip/induction.i
+++ b/src/plugins/wp/tests/wp_tip/induction.i
@@ -3,9 +3,12 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover script,alt-ergo -wp-timeout 1
-   OPT: -wp-prover script,alt-ergo -wp-timeout 1
-   OPT: -wp-prover script,alt-ergo -wp-timeout 1
+
+   OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
+
+   OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
+
+   OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
 */
 
 // Script 0: induction on f(x) => success
diff --git a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.session/script/function_loop_invariant_X_preserved.json b/src/plugins/wp/tests/wp_tip/induction_typing.0.session/script/function_loop_invariant_X_preserved.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/induction_typing.session/script/function_loop_invariant_X_preserved.json
rename to src/plugins/wp/tests/wp_tip/induction_typing.0.session/script/function_loop_invariant_X_preserved.json
diff --git a/src/plugins/wp/tests/wp_tip/induction_typing.i b/src/plugins/wp/tests/wp_tip/induction_typing.i
index c7e34e57aad8acb2248ac0403f85191c29299325..4f9b82169e695cd8280fd6b609f1d97f42b4eb7e 100644
--- a/src/plugins/wp/tests/wp_tip/induction_typing.i
+++ b/src/plugins/wp/tests/wp_tip/induction_typing.i
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
+
+   OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
 */
 /* run.config_qualif
    DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/modmask.0.session/script/check_lemma_and_modulo_u.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
rename to src/plugins/wp/tests/wp_tip/modmask.0.session/script/check_lemma_and_modulo_u.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/modmask.0.session/script/check_lemma_and_modulo_us_255.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
rename to src/plugins/wp/tests/wp_tip/modmask.0.session/script/check_lemma_and_modulo_us_255.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/modmask.1.session/script/check_lemma_and_modulo_u.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
rename to src/plugins/wp/tests/wp_tip/modmask.1.session/script/check_lemma_and_modulo_u.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/modmask.1.session/script/check_lemma_and_modulo_us_255.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
rename to src/plugins/wp/tests/wp_tip/modmask.1.session/script/check_lemma_and_modulo_us_255.json
diff --git a/src/plugins/wp/tests/wp_tip/modmask.i b/src/plugins/wp/tests/wp_tip/modmask.i
index 1970a5e62026c8ec79c5414ac01097565831704b..4da4f942609c8aa048db60978c10cd676ee7c1a6 100644
--- a/src/plugins/wp/tests/wp_tip/modmask.i
+++ b/src/plugins/wp/tests/wp_tip/modmask.i
@@ -1,6 +1,8 @@
 /* run.config
-   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
-   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session
+
+   OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
+
+   OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
 */
 /* run.config_qualif
    DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index 85363bf27b51a638d6c2a5287d6a1f7a50e80470..ebcdcd1cd229d0de017357404831a238328bd6d8 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -4,7 +4,7 @@
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp:script:allgoals] 
-  Goal Post-condition (file clear.i, line 21) in 'clear':
+  Goal Post-condition (file clear.i, line 22) in 'clear':
   Assume {
     Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
         is_sint32(b_1) /\ is_sint32(b_2).
@@ -22,7 +22,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Check (file clear.i, line 32):
+  Goal Check (file clear.i, line 33):
   Assume { (* Admit *) Have: P_P /\ P_Q /\ P_R. }
   Prove: P_S(42).
   
@@ -145,4 +145,3 @@
   ------------------------------------------------------------
 [wp] [Script] Goal typed_clear_ensures : Unsuccess
 [wp] Proved goals:    0 / 2
-[wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
index 3029b122d792578ce355ad05c505dbb4ed763ad9..113403f25fbc37f948c666780eb6283b6f44e185 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
@@ -4,7 +4,7 @@
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp:script:allgoals] 
-  Goal Preservation of Invariant 'X' (file induction_typing.i, line 41):
+  Goal Preservation of Invariant 'X' (file induction_typing.i, line 42):
   Let a = L_list(LIST_0).
   Let a_1 = a ^ [ 1 ].
   Let x = 1 + i.
@@ -117,4 +117,3 @@
   ------------------------------------------------------------
 [wp] Proved goals:    1 / 2
   Qed:             1
-[wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
index b65abf98b7fcfae08fcaf1c97159d599c8c10f3e..9176f7834810f23617fc86c4a39271e1de24b202 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -60,4 +60,3 @@
 [wp] Proved goals:    2 / 2
   Qed:             0 
   Script:          2
-[wp] Updated session with 2 new valid scripts.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
index b65abf98b7fcfae08fcaf1c97159d599c8c10f3e..9176f7834810f23617fc86c4a39271e1de24b202 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -60,4 +60,3 @@
 [wp] Proved goals:    2 / 2
   Qed:             0 
   Script:          2
-[wp] Updated session with 2 new valid scripts.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 8dd05e202f000270a7db1fc840e0a1e0d73c6cb6..3538ceb7485fd7a277aa0f03ee783db8e35f0246 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -4,7 +4,7 @@
 [wp] Warning: Missing RTE guards
 [wp] 23 goals scheduled
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 36) in 'test_step_branch':
+  Goal Post-condition (file split.i, line 37) in 'test_step_branch':
   Assume {
     Type: is_sint32(a) /\ is_sint32(b).
     If a < b
@@ -15,31 +15,31 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 46) in 'test_step_or':
+  Goal Post-condition (file split.i, line 47) in 'test_step_or':
   Assume { (* Pre-condition *) Have: P_P \/ P_Q \/ P_R. }
   Prove: P_S.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 50) in 'test_step_and':
+  Goal Post-condition (file split.i, line 51) in 'test_step_and':
   Assume { (* Pre-condition *) Have: P_P /\ P_Q /\ P_R. }
   Prove: P_S.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 54) in 'test_step_peq':
+  Goal Post-condition (file split.i, line 55) in 'test_step_peq':
   Assume { (* Pre-condition *) Have: L_LQ = L_LP. }
   Prove: P_S.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 58) in 'test_step_pneq':
+  Goal Post-condition (file split.i, line 59) in 'test_step_pneq':
   Assume { (* Pre-condition *) Have: L_LQ != L_LP. }
   Prove: P_S.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 62) in 'test_step_neq':
+  Goal Post-condition (file split.i, line 63) in 'test_step_neq':
   Assume {
     Type: is_sint32(a) /\ is_sint32(b).
     (* Pre-condition *)
@@ -49,7 +49,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 66) in 'test_step_leq':
+  Goal Post-condition (file split.i, line 67) in 'test_step_leq':
   Assume {
     Type: is_sint32(a) /\ is_sint32(b).
     (* Pre-condition *)
@@ -59,14 +59,14 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 70) in 'test_step_lt':
+  Goal Post-condition (file split.i, line 71) in 'test_step_lt':
   Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: a < b.
   }
   Prove: P_S.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 74) in 'test_step_if':
+  Goal Post-condition (file split.i, line 75) in 'test_step_if':
   Assume {
     Type: is_sint32(a) /\ is_sint32(b).
     (* Pre-condition *)
@@ -76,7 +76,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 78) in 'test_step_fa_if':
+  Goal Post-condition (file split.i, line 79) in 'test_step_fa_if':
   Assume {
     (* Heap *)
     Type: is_sint32(a) /\ is_sint32(b).
@@ -87,7 +87,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 82) in 'test_step_fa_or':
+  Goal Post-condition (file split.i, line 83) in 'test_step_fa_or':
   Assume {
     (* Pre-condition *)
     Have: forall i : Z. P_P \/ P_Q \/ P_R \/ P_Pi(i) \/ P_Qi(i).
@@ -96,7 +96,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 86) in 'test_step_fa_and':
+  Goal Post-condition (file split.i, line 87) in 'test_step_fa_and':
   Assume {
     (* Pre-condition *)
     Have: forall i : Z. P_P /\ P_Q /\ P_R /\ P_Pi(i) /\ P_Qi(i).
@@ -105,7 +105,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 90) in 'test_inside_leq':
+  Goal Post-condition (file split.i, line 91) in 'test_inside_leq':
   Assume {
     Type: is_sint32(a) /\ is_sint32(b).
     (* Pre-condition *)
@@ -115,7 +115,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 94) in 'test_inside_lt':
+  Goal Post-condition (file split.i, line 95) in 'test_inside_lt':
   Assume {
     Type: is_sint32(a) /\ is_sint32(b).
     (* Pre-condition *)
@@ -125,7 +125,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 98) in 'test_inside_neq':
+  Goal Post-condition (file split.i, line 99) in 'test_inside_neq':
   Assume {
     Type: is_sint32(a) /\ is_sint32(b).
     (* Pre-condition *)
@@ -135,43 +135,43 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 102) in 'test_goal_and':
+  Goal Post-condition (file split.i, line 103) in 'test_goal_and':
   Assume { (* Pre-condition *) Have: P_S. }
   Prove: P_P /\ P_Q /\ P_R.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 106) in 'test_goal_eq':
+  Goal Post-condition (file split.i, line 107) in 'test_goal_eq':
   Assume { (* Pre-condition *) Have: P_S. }
   Prove: L_LQ = L_LP.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 110) in 'test_goal_neq':
+  Goal Post-condition (file split.i, line 111) in 'test_goal_neq':
   Assume { (* Pre-condition *) Have: P_S. }
   Prove: L_LQ != L_LP.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 114) in 'test_goal_if':
+  Goal Post-condition (file split.i, line 115) in 'test_goal_if':
   Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: P_S. }
   Prove: if (a < b) then P_P else P_Q.
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 118) in 'test_goal_ex_and':
+  Goal Post-condition (file split.i, line 119) in 'test_goal_ex_and':
   Assume { (* Pre-condition *) Have: P_S. }
   Prove: exists i : Z. P_P /\ P_Q /\ P_Pi(i) /\ P_Qi(i).
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 122) in 'test_goal_ex_or':
+  Goal Post-condition (file split.i, line 123) in 'test_goal_ex_or':
   Assume { (* Pre-condition *) Have: P_S. }
   Prove: exists i : Z. P_P \/ P_Q \/ P_Pi(i) \/ P_Qi(i).
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 126) in 'test_goal_ex_if':
+  Goal Post-condition (file split.i, line 127) in 'test_goal_ex_if':
   Assume {
     (* Heap *)
     Type: is_sint32(a) /\ is_sint32(b).
@@ -182,7 +182,7 @@
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
-  Goal Post-condition (file split.i, line 130) in 'test_goal_ex_imply':
+  Goal Post-condition (file split.i, line 131) in 'test_goal_ex_imply':
   Assume { (* Pre-condition *) Have: P_S. }
   Prove: exists i : Z. (P_Q -> (P_Pi(i) -> P_Qi(i))).
   
@@ -704,4 +704,3 @@
   ------------------------------------------------------------
 [wp] [Script] Goal typed_test_goal_ex_imply_ensures : Unsuccess
 [wp] Proved goals:    0 / 23
-[wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json
deleted file mode 100644
index 5a4345732238664a27f4c2cf710df871d69c5f6d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0549, "steps": 117 },
-  { "header": "Induction", "tactic": "Wp.induction",
-    "params": { "base": 0, "hsup": true, "hinf": true },
-    "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
-                "pattern": "L_f$x" },
-    "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
-                              "time": 0.0083, "steps": 6 } ],
-                  "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
-                                         "verdict": "valid", "time": 0.0549,
-                                         "steps": 117 } ],
-                  "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
-                                         "verdict": "valid", "time": 0.0274,
-                                         "steps": 86 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
rename to src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
rename to src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
diff --git a/src/plugins/wp/tests/wp_tip/overflow.i b/src/plugins/wp/tests/wp_tip/overflow.i
index 3150b39720d4fca966f1455bdc02778faa3ad5f1..34298d91ee6cd15218eaa30df4b27a7e8ddeae8d 100644
--- a/src/plugins/wp/tests/wp_tip/overflow.i
+++ b/src/plugins/wp/tests/wp_tip/overflow.i
@@ -3,7 +3,8 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover script,alt-ergo -wp-timeout 1
+
+   OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@
 */
 
 typedef unsigned int uint;
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_and_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_and_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_and_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_and_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_eq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_eq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_eq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_eq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_and_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_and_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_and_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_and_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_if_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_if_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_if_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_if_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_imply_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_imply_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_imply_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_imply_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_or_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_or_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_or_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_ex_or_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_if_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_if_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_if_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_if_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_neq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_neq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_neq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_goal_neq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_leq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_inside_leq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_leq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_inside_leq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_lt_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_inside_lt_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_lt_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_inside_lt_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_neq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_inside_neq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_neq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_inside_neq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_and_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_and_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_and_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_and_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_branch_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_branch_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_branch_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_branch_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_and_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_fa_and_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_and_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_fa_and_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_if_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_fa_if_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_if_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_fa_if_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_or_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_fa_or_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_or_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_fa_or_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_if_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_if_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_if_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_if_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_leq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_leq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_lt_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_lt_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_neq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_neq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_or_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_or_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_or_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_or_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_peq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_peq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_peq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_peq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json b/src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_pneq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json
rename to src/plugins/wp/tests/wp_tip/split.0.session/script/test_step_pneq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/split.i b/src/plugins/wp/tests/wp_tip/split.i
index 984bb90f40213dcc5bb5bdeaf54829475dc67f5e..27c531dbae2c92e8ed17eb4a5bb62f682ad44956 100644
--- a/src/plugins/wp/tests/wp_tip/split.i
+++ b/src/plugins/wp/tests/wp_tip/split.i
@@ -1,5 +1,6 @@
 /* run.config
-   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
+
+   OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@
 */
 /* run.config_qualif
    DONTRUN:
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Goal_Exist_And.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
rename to src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Goal_Exist_And.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Goal_Exist_And_bis.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
rename to src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Goal_Exist_And_bis.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Goal_Exist_Or.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
rename to src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Goal_Exist_Or.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Hyp_Forall_And.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
rename to src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Hyp_Forall_And.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Hyp_Forall_Or_bis.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
rename to src/plugins/wp/tests/wp_tip/tac_split_quantifiers.0.session_qualif/script/split_ensures_Hyp_Forall_Or_bis.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
index 4ec12dfda05815efbfd4544eb8190d8dec43dd73..fd890b44fd309b9274b16f57b3b612078a9682a2 100644
--- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
@@ -4,7 +4,8 @@
 
 /* run.config_qualif
    SCRIPT: TacNOP
-   OPT: -wp -wp-par 1 -wp-prover script
+
+   OPT: -wp -wp-par 1 -wp-prover script @USING_WP_SESSION@
 */
 
 
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json b/src/plugins/wp/tests/wp_tip/unroll.0.session_qualif/script/lemma_LEFT.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
rename to src/plugins/wp/tests/wp_tip/unroll.0.session_qualif/script/lemma_LEFT.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json b/src/plugins/wp/tests/wp_tip/unroll.0.session_qualif/script/lemma_RIGHT.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
rename to src/plugins/wp/tests/wp_tip/unroll.0.session_qualif/script/lemma_RIGHT.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json b/src/plugins/wp/tests/wp_tip/unroll.0.session_qualif/script/lemma_SUM.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
rename to src/plugins/wp/tests/wp_tip/unroll.0.session_qualif/script/lemma_SUM.json
diff --git a/src/plugins/wp/tests/wp_tip/unroll.i b/src/plugins/wp/tests/wp_tip/unroll.i
index c3392a979882d88ac32a403217b9a24fb4d55398..df1151d0372728c581ddaed68ce417a896d07c55 100644
--- a/src/plugins/wp/tests/wp_tip/unroll.i
+++ b/src/plugins/wp/tests/wp_tip/unroll.i
@@ -3,7 +3,8 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover script,none
+
+   OPT: -wp-prover script,none @USING_WP_SESSION@
  */
 
 /*@
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_exit_part2.json
deleted file mode 100644
index 5cf9423e22d177229d655f757dba2b49e66f51b7..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_exit_part2.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_108",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_normal_part2.json
deleted file mode 100644
index 5cf9423e22d177229d655f757dba2b49e66f51b7..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_normal_part2.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_108",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part2.json
deleted file mode 100644
index 9e5622f6d53b8ed49925306f393bad2c14f24d01..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part2.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_15",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part3.json
deleted file mode 100644
index 71fa062236e2f665a094d0563416c9c3c13e7e9d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part3.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_4",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_exit_part2.json
deleted file mode 100644
index 84546c12c64c29b6123fa2985dc0265895a3be59..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_107",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.11,
-                                 "steps": 47 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.1033,
-                                 "steps": 47 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0879,
-                                 "steps": 47 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.1018,
-                                 "steps": 47 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.107,
-                                 "steps": 47 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0761,
-                                 "steps": 47 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0982,
-                                 "steps": 47 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0885,
-                                 "steps": 47 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0754,
-                                 "steps": 47 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.1044,
-                                 "steps": 47 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_normal_part2.json
deleted file mode 100644
index ebfb03dd03a74b879334251e537c026783612072..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_107",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.1042,
-                                 "steps": 47 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.1018,
-                                 "steps": 47 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0916,
-                                 "steps": 47 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.091,
-                                 "steps": 47 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0978,
-                                 "steps": 47 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.1066,
-                                 "steps": 47 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0893,
-                                 "steps": 47 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0847,
-                                 "steps": 47 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.1061,
-                                 "steps": 47 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.101,
-                                 "steps": 47 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part2.json
deleted file mode 100644
index 337706ad80c763a279db36d9895ad3cb1eb74100..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_14",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.7322,
-                                 "steps": 71 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.7011,
-                                 "steps": 71 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.7025,
-                                 "steps": 71 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6781,
-                                 "steps": 71 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6647,
-                                 "steps": 71 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.8582,
-                                 "steps": 71 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.8677,
-                                 "steps": 71 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.8604,
-                                 "steps": 71 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.8716,
-                                 "steps": 71 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.8618,
-                                 "steps": 71 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part3.json
deleted file mode 100644
index 71fa062236e2f665a094d0563416c9c3c13e7e9d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_4",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_assigns_part2.json
deleted file mode 100644
index ce3491eaf9b6b359626e49a15b571adc3e4e0cdc..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_assigns_part2.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_128",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part2.json
deleted file mode 100644
index eb4dd79d6b43bf253e480a47fb317bad5110a219..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part2.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_21",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part3.json
deleted file mode 100644
index a7ba59113add3531d5d53557e9f721db53015f21..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part3.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_0",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part2.json
deleted file mode 100644
index 8d897fef8325d9cc0fcbe241470cb21a07f127ac..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part2.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_35",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part3.json
deleted file mode 100644
index 9e5622f6d53b8ed49925306f393bad2c14f24d01..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part3.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_15",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_assigns_part2.json
deleted file mode 100644
index bd817f1424eaabf85438e5a5a84a4ffaa7434415..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_assigns_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_167",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0512,
-                                 "steps": 35 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0528,
-                                 "steps": 35 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0513,
-                                 "steps": 35 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0521,
-                                 "steps": 35 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0529,
-                                 "steps": 35 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0489,
-                                 "steps": 35 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0508,
-                                 "steps": 35 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0509,
-                                 "steps": 35 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0493,
-                                 "steps": 35 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0517,
-                                 "steps": 35 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part2.json
deleted file mode 100644
index 9938bd712908b2b72d15baff1a8da37102ac1fa1..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_19",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6133,
-                                 "steps": 61 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6011,
-                                 "steps": 61 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6246,
-                                 "steps": 61 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6211,
-                                 "steps": 61 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6069,
-                                 "steps": 61 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5578,
-                                 "steps": 61 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6946,
-                                 "steps": 61 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6906,
-                                 "steps": 61 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6571,
-                                 "steps": 61 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5331,
-                                 "steps": 61 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part3.json
deleted file mode 100644
index a7ba59113add3531d5d53557e9f721db53015f21..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_0",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part2.json
deleted file mode 100644
index 0615766743729aba61617e09eb1b207760e71809..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_32",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6311,
-                                 "steps": 53 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6374,
-                                 "steps": 53 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6393,
-                                 "steps": 53 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5517,
-                                 "steps": 53 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6064,
-                                 "steps": 53 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6106,
-                                 "steps": 53 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.564,
-                                 "steps": 53 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5933,
-                                 "steps": 53 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5774,
-                                 "steps": 53 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5444,
-                                 "steps": 53 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part3.json
deleted file mode 100644
index 3b03ebb08ed2186a6fb144df309a1edb88129f41..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part3.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_14",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6148,
-                                 "steps": 53 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.612,
-                                 "steps": 53 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6102,
-                                 "steps": 53 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5953,
-                                 "steps": 53 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5773,
-                                 "steps": 53 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5457,
-                                 "steps": 53 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5134,
-                                 "steps": 53 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6069,
-                                 "steps": 53 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6142,
-                                 "steps": 53 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6253,
-                                 "steps": 53 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_assigns_part2.json
deleted file mode 100644
index a59995dbef46d00acbc4a725b55c41d75fd6bbf1..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_assigns_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_151",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0348,
-                                 "steps": 35 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0334,
-                                 "steps": 35 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0323,
-                                 "steps": 35 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0319,
-                                 "steps": 35 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0331,
-                                 "steps": 35 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0333,
-                                 "steps": 35 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0314,
-                                 "steps": 35 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0322,
-                                 "steps": 35 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0299,
-                                 "steps": 35 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.0294,
-                                 "steps": 35 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part2.json
deleted file mode 100644
index abc610f8dfaa4833f10b1da073652892c45316f5..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part2.json
+++ /dev/null
@@ -1,36 +0,0 @@
-[ { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_16",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6897,
-                                 "steps": 73 } ],
-                  "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6809,
-                                 "steps": 73 } ],
-                  "Value 2": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6865,
-                                 "steps": 73 } ],
-                  "Value 3": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6769,
-                                 "steps": 73 } ],
-                  "Value 4": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.6553,
-                                 "steps": 73 } ],
-                  "Value 5": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.7109,
-                                 "steps": 73 } ],
-                  "Value 6": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5708,
-                                 "steps": 73 } ],
-                  "Value 7": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5186,
-                                 "steps": 73 } ],
-                  "Value 8": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.5309,
-                                 "steps": 73 } ],
-                  "Value 9": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "valid", "time": 0.459,
-                                 "steps": 73 } ],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part3.json
deleted file mode 100644
index 08661a75e46b9fdefd13e403d180dd9d60096cd6..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part3.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. },
-  { "prover": "script", "verdict": "timeout", "time": 10. },
-  { "header": "Range", "tactic": "Wp.range",
-    "params": { "inf": 0, "sup": 9 },
-    "select": { "select": "inside-goal", "occur": 0, "target": "i_6",
-                "pattern": "$i" },
-    "children": { "Lower 0": [ { "prover": "qed", "verdict": "valid" } ],
-                  "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
-                                 "verdict": "timeout", "time": 10. } ],
-                  "Value 1": [], "Value 2": [], "Value 3": [], "Value 4": [],
-                  "Value 5": [], "Value 6": [], "Value 7": [], "Value 8": [],
-                  "Value 9": [],
-                  "Upper 9": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 9968c80e80f67454ab2f051b6341b0e93da7d4f0..4221a029a04f706a123cff2b85f71508f0caa367 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -30,6 +30,138 @@
   Qed:            11 
   Script:         12 
   Alt-Ergo:        0  (unsuccess: 12)
+[wp] Proof script for typed_init_t2_v2_loop_assigns_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0098,
+                                    "steps": 35 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0048,
+                                    "steps": 35 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_loop_assigns_part3:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0098,
+                                    "steps": 35 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0048,
+                                    "steps": 35 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0099,
+                                    "steps": 42 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0124,
+                                    "steps": 42 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_loop_assigns_2_part3:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_1<=i_2) /\\ (i_2<=j_1) /\\ (i_0<=9)",
+                  "pattern": "\\E$i0$i$j$j9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0094,
+                                    "steps": 26 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0101,
+                                    "steps": 26 } ] } } ]
+[wp] Proof script for typed_init_t2_v2_assigns_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_158) /\\ (i_1<=i_159) /\\ (0<=i_0) /\\ (i_158<=i_0) /\\ (i_159<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.011,
+                                    "steps": 16 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0092,
+                                    "steps": 16 } ] } } ]
+[wp] Proof script for typed_init_t2_v3_loop_assigns_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0139,
+                                    "steps": 45 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0127,
+                                    "steps": 45 } ] } } ]
+[wp] Proof script for typed_init_t2_v3_loop_assigns_part3:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0169,
+                                    "steps": 33 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0081,
+                                    "steps": 33 } ] } } ]
+[wp] Proof script for typed_init_t2_v3_assigns_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_149) /\\ (i_1<=i_150) /\\ (0<=i_0) /\\ (i_149<=i_0) /\\ (i_150<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.011,
+                                    "steps": 16 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0092,
+                                    "steps": 16 } ] } } ]
+[wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0124,
+                                    "steps": 43 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0121,
+                                    "steps": 43 } ] } } ]
+[wp] Proof script for typed_init_t2_bis_v2_loop_assigns_part3:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (i_2<=i_3) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (i_3<=i_2) /\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0074,
+                                    "steps": 31 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0078,
+                                    "steps": 31 } ] } } ]
+[wp] Proof script for typed_init_t2_bis_v2_assigns_exit_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0088,
+                                    "steps": 24 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0116,
+                                    "steps": 24 } ] } } ]
+[wp] Proof script for typed_init_t2_bis_v2_assigns_normal_part2:
+  [ { "header": "Split", "tactic": "Wp.split", "params": {},
+      "select": { "select": "clause-goal",
+                  "target": "exists i_0,i_1:int.\n(i_0<=i_138) /\\ (i_1<=i_139) /\\ (0<=i_0) /\\ (i_138<=i_0) /\\ (i_139<=i_1)\n/\\ (i_0<=9)",
+                  "pattern": "\\E$i$i0$i$i9" },
+      "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0088,
+                                    "steps": 24 } ],
+                    "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+                                    "verdict": "valid", "time": 0.0116,
+                                    "steps": 24 } ] } } ]
 [wp] Updated session with 12 new valid scripts.
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index 251dcd36298a05a068bd1d12adb9cc898e1de159..fec0099075211dc4d3902773c8ac1d6be01ed968 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,7 +1,7 @@
 /* run.config_qualif
-   EXECNOW: rm -rf @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.1.session/script
+
    OPT: -wp-prop=-lack,-tactic
-   OPT: -wp-prop=tactic -wp-auto=wp:split,wp:range -wp-prover=tip,alt-ergo
+   OPT: -wp-prop=tactic -wp-auto=wp:split,wp:range -wp-prover=tip,alt-ergo -wp-script-on-stdout
    OPT: -wp-prop=lack
  */
 /*@ requires \valid(a+(0..n-1)) ;
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 858b5dcb0f1616f1a2aff888c7ddafbe96cc7b87..899d35209bc245448bceab0b2bf94103048028dc 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -752,6 +752,14 @@ module Generate = False
     end)
 let () = on_reset Generate.clear
 
+let () = Parameter_customize.set_group wp_prover
+module ScriptOnStdout = False
+    (struct
+      let option_name = "-wp-script-on-stdout"
+      let help = "When enabled (default: no), display scripts on stdout \
+                  instead of writing them on disk."
+    end)
+
 let () = Parameter_customize.set_group wp_prover
 module Detect = Action
     (struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 2d40d716772da3218de5e669c68c4f29e0a81efd..3434739d907fd24c8f65445200b5c041a31400a7 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -111,6 +111,7 @@ module TerminatesVariantHyp : Parameter_sig.Bool
 
 module Detect: Parameter_sig.Bool
 module Generate:Parameter_sig.Bool
+module ScriptOnStdout: Parameter_sig.Bool
 module Provers: Parameter_sig.String_list
 module Interactive: Parameter_sig.String
 module RunAllProvers: Parameter_sig.Bool