diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 65769f4abb2f683f699a787836eadc6161371462..c71ba7beb2f0a9a659179ead3e41fb8094b15c93 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,3 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 45 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report @PTEST_FILE@
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 45 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session @PTEST_FILE@
LOG: @PTEST_NAME@.@PTEST_NUMBER@.report.json
OPT:
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned/wp/typed/typed_lemma_U32.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/typed/typed_lemma_U32.json
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/unsigned/wp/typed/typed_lemma_U32.json
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/typed/typed_lemma_U32.json
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.i b/src/plugins/wp/tests/wp_plugin/unsigned.i
index 53b1efa1b8141219ec560df54259be1486ff3f5a..b48f75fbbc3d9925d4f25f00ca77f8d7a292c9b0 100644
--- a/src/plugins/wp/tests/wp_plugin/unsigned.i
+++ b/src/plugins/wp/tests/wp_plugin/unsigned.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -session tests/wp_plugin/unsigned -wp-prover script
+ OPT: -wp-prover script
*/
/*@
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And_bis.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And_bis.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And_bis.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_Or.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_Or.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_Or.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_Or.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Hyp_Forall_And.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_And.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Hyp_Forall_And.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_Or_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Hyp_Forall_Or_bis.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_Or_bis.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_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 7f99eb527c97c356d2045d5feca4cae3817e82a5..7d6f12f66d12dcc3006b3c17fb5bc2a54bbc3c66 100644
--- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -load-module tests/wp_tip/TacNOP.ml -wp -wp-par 1 -wp-prover script -session tests/wp_tip/tac_split_quantifiers
+ OPT: -load-module tests/wp_tip/TacNOP.ml -wp -wp-par 1 -wp-prover script
*/
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 60c38cd4360789439d93bed382ab118266e4ddee..0a25b0620ac8ce8de51629ac118b4e95b49a7503 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
@@ -10,8 +10,7 @@
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_assigns_part1 : Valid
-[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1'
-[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1/wp'
+[wp] Warning: creating session directory `tests/wp_typed/oracle_qualif/user_init.1.session'
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part3 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_exit_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..210fb9dcdcd1b875860205a132a1334f635dcb7a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0174,
+ "steps": 12 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0186,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..b90d48fad5680543bc67b77f431fb2f4433231d9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0183,
+ "steps": 12 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0199,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..6172c1f2b587434118ab4991a3749cb221979b05
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "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\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0242,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0275,
+ "steps": 28 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..7fcdb05a3ec940a683e9b423169dd863701b11d8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0244,
+ "steps": 16 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0246,
+ "steps": 22 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..9fac563fc175f530418341363ab373fa49a7e7c7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0083,
+ "steps": 9 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0075,
+ "steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..e14df9c1762d84477dfa05f6a6d953623c4828cc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json
@@ -0,0 +1,10 @@
+[ { "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\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0113,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0127,
+ "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..001f140e03bdd07fe151bdf34c350e7fffeff545
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json
@@ -0,0 +1,10 @@
+[ { "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_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0106,
+ "steps": 14 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0108,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..89a30ff9b663ab8d4b0e44827dcc7623fdc737db
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "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\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0175,
+ "steps": 18 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0191,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..41c6b0299134d6e110f77362a5f9b38e1da9127b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json
@@ -0,0 +1,10 @@
+[ { "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\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0191,
+ "steps": 18 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.021,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..b52f15827c394be02569a93a78a0570dbaef4b4b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0055,
+ "steps": 9 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0068,
+ "steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..94b6d3f27f21179f6c9a9caa86a6fb0e2d97fcf4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "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\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0115,
+ "steps": 23 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.013,
+ "steps": 27 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..0b50684631befa4320919568e23f54519c59dcb2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part3.json
@@ -0,0 +1,10 @@
+[ { "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\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0091,
+ "steps": 17 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0097,
+ "steps": 21 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index a34d4664bb4cdb7cdbe9e5738e75b0b78a2a5de0..1ba6792df7b0654b6786b247fcdb28c7e8516b15 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_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-1/
+ EXECNOW: rm -rf @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.1.session
OPT: -wp-prop=-lack,-tactic
- OPT: -wp-prop=tactic -wp-auto=wp:split -session @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-@PTEST_NUMBER@
+ OPT: -wp-prop=tactic -wp-auto=wp:split
OPT: -wp-prop=lack -wp-steps 300
*/
/*@ requires \valid(a+(0..n-1)) ;