diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 9b3384e53f80eca3ae39bf890145b484f61c43b4..47549ee4316744b5cde028b18701b28aa8e33dcb 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -145,10 +145,14 @@ wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt
./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt
- FRAMAC_WP_CACHE=update ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+ FRAMAC_WP_CACHE=update \
+ FRAMAC_WP_SCRIPT=update \
+ ./bin/ptests.opt src/plugins/wp/tests -config qualif
wp-qualif-cleanup: ./bin/toplevel.opt ./bin/ptests.opt
- FRAMAC_WP_CACHE=cleanup ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+ FRAMAC_WP_CACHE=cleanup \
+ FRAMAC_WP_SCRIPT=update \
+ ./bin/ptests.opt src/plugins/wp/tests -config qualif
# --------------------------------------------------------------------------
# --- Dynamic Plugin ---
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index db0cb3b658414c06416f3db62e8175d14ad769b7..fe94b79d5a03808c15a8e3972687be0c695026e5 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -69,7 +69,7 @@ let prover_of_name = function
match Why3Provers.find_fallback name with
| Exact p -> Some (Why3 p)
| Fallback p ->
- Wp_parameters.warning ~current:false
+ Wp_parameters.warning ~current:false ~once:true
"Prover '%s' not found, fallback to '%s'"
(String.concat ":" prv) (Why3Provers.print_wp p) ;
Some (Why3 p)
diff --git a/src/plugins/wp/tests/qualif.report b/src/plugins/wp/tests/qualif.report
index 1e81d96a466fd0404246893cc98257fa726b59af..83c8419f1b0cc37407075a035f75387c775162b8 100644
--- a/src/plugins/wp/tests/qualif.report
+++ b/src/plugins/wp/tests/qualif.report
@@ -5,7 +5,7 @@
------------------------------------------------------------
%chapter &25: WP &34:Alt-Ergo &43: Total &52:Success
@SECTION
- %name &25:%wp &34:%{Alt-Ergo,2.0.0,} &43:%total &52: %success%%
+ %name &25:%wp &34:%{alt-ergo} &43:%total &52: %success%%
@TAIL
------------------------------------------------------------
@END
diff --git a/src/plugins/wp/tests/wp_acsl/logic.i b/src/plugins/wp/tests/wp_acsl/logic.i
index 7a54adc27e1d6764c96cef25f3bdd3facdfbedbe..086100cee333d6503a88acb0e00d029d029347c3 100644
--- a/src/plugins/wp/tests/wp_acsl/logic.i
+++ b/src/plugins/wp/tests/wp_acsl/logic.i
@@ -2,7 +2,7 @@
OPT: -wp-model Typed
*/
/* run.config_qualif
- OPT: -wp -wp-model Typed -wp-steps 50
+ OPT: -wp -wp-model Typed
*/
// Test logic types defined from C types
//--------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
index 82b3b1d5d8cacf57b8964ce057e1c017a807deb3..4f622671cdd1a80fe80834e171d582f737a8eb23 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-steps 50 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -35,13 +35,13 @@
[wp] tests/wp_acsl/logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled
-[wp] [Alt-Ergo] Goal typed_h_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_h_ensures : Valid
[wp] [Qed] Goal typed_h_assigns_exit : Valid
[wp] [Qed] Goal typed_h_assigns_normal : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Valid
-[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_6 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_7 : Unsuccess (Stronger)
@@ -56,11 +56,11 @@
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_16 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_17 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_18 : Unsuccess (Stronger)
-[wp] Proved goals: 5 / 21
+[wp] Proved goals: 7 / 21
Qed: 3
- Alt-Ergo: 2 (unsuccess: 16)
+ Alt-Ergo: 4 (unsuccess: 14)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- h 2 - 3 66.7%
- main 1 2 18 16.7%
+ h 2 1 3 100%
+ main 1 3 18 22.2%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c b/src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c
index 1d455c31d8061aac54dea17290b1e62fe799a0fe..f52b6b9b19f46f34e7f32691ce5d112d23ce556e 100644
--- a/src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c
+++ b/src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -wp-prop=-left_unproved -then -wp-rte -wp -wp-prop=-left_unproved
+ OPT: -wp-prover=script,alt-ergo -wp-prop=-left_unproved -then -wp-rte -wp -wp-prop=-left_unproved
*/
/* ******************************* */
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 31b0e5ca191210a8c8c217f4b5db0df4214f9d7f..5efd85925f192e886ffcd95ca3ffeceec4ae98c0 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -10,7 +10,7 @@
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Unsuccess
+[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_preserved : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_established : Valid
@@ -21,15 +21,15 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
-[wp] Proved goals: 16 / 17
+[wp] Proved goals: 17 / 17
Qed: 4
- Alt-Ergo: 12 (unsuccess: 1)
+ Alt-Ergo: 13
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 3 4 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- BinaryMultiplication 3 9 13 92.3%
+ BinaryMultiplication 3 10 13 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
@@ -40,7 +40,7 @@
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Unsuccess
+[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_preserved : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_established : Valid
@@ -52,12 +52,12 @@
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 13 / 17
- Qed: 1
- Alt-Ergo: 12 (unsuccess: 1)
+ Qed: 0
+ Alt-Ergo: 13
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 3 4 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- BinaryMultiplication 3 9 13 92.3%
+ BinaryMultiplication 3 10 13 100%
------------------------------------------------------------
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
new file mode 100644
index 0000000000000000000000000000000000000000..bd263392345c0cb221651242d0ebd03855bf2e5a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/script/init_assigns_part3.json
@@ -0,0 +1,25 @@
+[ { "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 20. },
+ { "prover": "script", "verdict": "valid" },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 16 },
+ "select": { "select": "inside-goal", "occur": 0, "target": "i_112",
+ "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_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index 7ee8ff1e6b0b7f46cc178ffba2ceed6c2b4778cb..edd11a46ad8d1cf3c9f40c415e0030f2b5369217 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -76,7 +76,7 @@
[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_assigns_part1 : Valid
[wp] [Qed] Goal typed_init_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_assigns_part3 : Valid
+[wp] [Script] Goal typed_init_assigns_part3 : Valid
[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_complete_not_found_found : Valid
@@ -109,13 +109,14 @@
[wp] [Qed] Goal typed_size_assigns : Valid
[wp] Proved goals: 102 / 102
Qed: 69
- Alt-Ergo: 33
+ Script: 1
+ Alt-Ergo: 32
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
eq_string 11 4 15 100%
hash 6 1 7 100%
size 2 - 2 100%
- init 8 5 13 100%
+ init 8 4 13 100%
add 24 15 39 100%
mem_binding 18 8 26 100%
------------------------------------------------------------
@@ -224,7 +225,7 @@
[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_assigns_part1 : Valid
[wp] [Qed] Goal typed_init_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_assigns_part3 : Valid
+[wp] [Script] Goal typed_init_assigns_part3 : Valid
[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_complete_not_found_found : Valid
@@ -272,13 +273,14 @@
[wp] [Qed] Goal typed_size_assigns : Valid
[wp] Proved goals: 74 / 143
Qed: 16
- Alt-Ergo: 58
+ Script: 1
+ Alt-Ergo: 57
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
eq_string 11 7 18 100%
hash 7 3 10 100%
size 2 1 3 100%
- init 10 8 18 100%
+ init 10 7 18 100%
add 30 24 54 100%
mem_binding 25 15 40 100%
------------------------------------------------------------
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 2c728ac4288c0b7f9527d81fcf49882ac4050f1f..49c2566726f22ad51b96a3100e073b5a28db4e4d 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
@@ -1,7 +1,7 @@
----------------------------------------------------------
WP Requirements for Qualif Tests (3)
----------------------------------------------------------
-1. The Alt-Ergo theorem prover, version 2.0.0
-2. The Why3 platform, version 1.2.0
-3. The Coq Proof Assistant, version 8.7.2
+1. The Alt-Ergo theorem prover, version 2.3.0
+2. The Why3 platform, version 1.2.1
+3. The Coq Proof Assistant, version 8.9.1
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index 4b005c11a31b2e9dbfab45e3ecebf574424538f2..d488804035c965e0eb870fec18654e5612b19332 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.0.0'
+[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.3.0'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
index a4bc55ce426f46f0f19a9c08a38a529ac8b438f4..6752a74f6932c0be8c315866cd47a2d167bfa108 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
@@ -6,12 +6,12 @@
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_A : Valid
-[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Unsuccess
+[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Valid
[wp] [Qed] Goal typed_foo_call_fconcat_requires_qed_ok : Valid
-[wp] Proved goals: 3 / 4
+[wp] Proved goals: 4 / 4
Qed: 1
- Alt-Ergo: 2 (unsuccess: 1)
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- foo 1 2 4 75.0%
+ foo 1 3 4 100%
------------------------------------------------------------
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
new file mode 100644
index 0000000000000000000000000000000000000000..5cf9423e22d177229d655f757dba2b49e66f51b7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_exit_part2.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..5cf9423e22d177229d655f757dba2b49e66f51b7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_normal_part2.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..9e5622f6d53b8ed49925306f393bad2c14f24d01
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part2.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..71fa062236e2f665a094d0563416c9c3c13e7e9d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part3.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..84546c12c64c29b6123fa2985dc0265895a3be59
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..ebfb03dd03a74b879334251e537c026783612072
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..337706ad80c763a279db36d9895ad3cb1eb74100
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..71fa062236e2f665a094d0563416c9c3c13e7e9d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..ce3491eaf9b6b359626e49a15b571adc3e4e0cdc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_assigns_part2.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..eb4dd79d6b43bf253e480a47fb317bad5110a219
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part2.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..a7ba59113add3531d5d53557e9f721db53015f21
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part3.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..8d897fef8325d9cc0fcbe241470cb21a07f127ac
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part2.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..9e5622f6d53b8ed49925306f393bad2c14f24d01
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part3.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..bd817f1424eaabf85438e5a5a84a4ffaa7434415
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_assigns_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..9938bd712908b2b72d15baff1a8da37102ac1fa1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..a7ba59113add3531d5d53557e9f721db53015f21
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -0,0 +1,13 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..0615766743729aba61617e09eb1b207760e71809
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..3b03ebb08ed2186a6fb144df309a1edb88129f41
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part3.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..a59995dbef46d00acbc4a725b55c41d75fd6bbf1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_assigns_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..abc610f8dfaa4833f10b1da073652892c45316f5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part2.json
@@ -0,0 +1,36 @@
+[ { "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
new file mode 100644
index 0000000000000000000000000000000000000000..08661a75e46b9fdefd13e403d180dd9d60096cd6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part3.json
@@ -0,0 +1,13 @@
+[ { "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 3f6e407c1d3587161c1c31ffb4a34a9aaadf71e1..3a97274559283cd00d6f3e0ee43bc9a0bea53be0 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
@@ -36,6 +36,7 @@
Qed: 11
Script: 12
Alt-Ergo: 0 (unsuccess: 12)
+[wp] Updated session with 12 new valid scripts.
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init_t2_v2 3 - 8 100%
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..cfbcd4dd1cae5c544daa4aac1e583a7a981247b8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0906,
+ "steps": 51 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 8.328,
+ "steps": 1475 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..cfbcd4dd1cae5c544daa4aac1e583a7a981247b8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0906,
+ "steps": 51 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 8.328,
+ "steps": 1475 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..ecb82b8fa1ce61d65b27494b9f6a7798bb052a37
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -0,0 +1,38 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.744,
+ "steps": 75 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 9 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "i_9",
+ "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..e395695e644df46adf930462f341b6db2cd34e07
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -0,0 +1,86 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 19 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "i_3",
+ "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" } ],
+ "Value 17": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 18": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 19": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper 19": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "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": "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..85ffcc3385279300d24a894dafc306485638b100
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0324,
+ "steps": 39 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.6058,
+ "steps": 404 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..4b77a3694b53586839a90fcbbf35e218b3648cf6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -0,0 +1,38 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.4456,
+ "steps": 65 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 9 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "i_13",
+ "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..aca21574a962baa90bfddafa22738a2053a87b8b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -0,0 +1,86 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 19 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "j_0",
+ "pattern": "$j" },
+ "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" } ],
+ "Value 17": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 18": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 19": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper 19": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 9 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "i_1",
+ "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..ba59bc83677eca0c889af44aadeba3bdc56623a7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -0,0 +1,38 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.419,
+ "steps": 57 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "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": "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..81b95722e76973fe64cc00c7196917e3636a31eb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -0,0 +1,38 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.419,
+ "steps": 57 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 9 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "i_8",
+ "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..736aad8f408a77c810f7145e805cfe3c998ea6c9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0324,
+ "steps": 39 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.6058,
+ "steps": 404 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
new file mode 100644
index 0000000000000000000000000000000000000000..c5f4b0bf30c2b2461d314dad3c55bbc3df554ba2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -0,0 +1,38 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.4214,
+ "steps": 72 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 9 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "i_13",
+ "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
new file mode 100644
index 0000000000000000000000000000000000000000..ae77b380278e51f14e37e8071714f3f41f99afde
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -0,0 +1,86 @@
+[ { "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": "Alt-Ergo:2.0.0",
+ "verdict": "timeout", "time": 10. },
+ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 19 },
+ "select": { "select": "inside-goal",
+ "occur": 0, "target": "i_6",
+ "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" } ],
+ "Value 17": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 18": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Value 19": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper 19": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "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": "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" } ],
+ "Upper 9": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
index 58e3100351f71cf0a37e49f47ae3541080498d9a..21d17e27f81061c3125263f7bd5eb704e588d172 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-steps 300 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index a22e23c5afc69423bfbf574d37c64794359eb442..6bda4f9640bfb6620309aca3950bd93c093b81e5 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,8 +1,8 @@
/* run.config_qualif
EXECNOW: rm -rf @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.1.session/script
OPT: -wp-prop=-lack,-tactic
- OPT: -wp-prop=tactic -wp-auto=wp:split
- OPT: -wp-prop=lack -wp-steps 300
+ OPT: -wp-prop=tactic -wp-auto=wp:split,wp:range -wp-prover=tip,alt-ergo
+ OPT: -wp-prop=lack
*/
/*@ requires \valid(a+(0..n-1)) ;
@ requires n >= 0 ;