From 4f10ca195262912234b6489d692191a9b6a3f853 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 3 Mar 2020 10:12:41 +0100
Subject: [PATCH] [wp] upgrade prover versions
Why3: 1.2.1
Alt-Ergo: 2.3.0
Coq: 8.9.1
---
src/plugins/wp/Makefile.in | 8 +-
src/plugins/wp/VCS.ml | 2 +-
src/plugins/wp/tests/qualif.report | 2 +-
src/plugins/wp/tests/wp_acsl/logic.i | 2 +-
.../wp_acsl/oracle_qualif/logic.res.oracle | 14 +--
.../tests/wp_gallery/frama_c_hashtbl_solved.c | 2 +-
.../binary-multiplication.res.oracle | 16 ++--
.../script/init_assigns_part3.json | 25 ++++++
.../frama_c_hashtbl_solved.res.oracle | 14 +--
.../wp_plugin/oracle_qualif/config.res.oracle | 6 +-
.../oracle_qualif/fallback.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/trig.res.oracle | 8 +-
.../init_t2_bis_v1_assigns_exit_part2.json | 13 +++
.../init_t2_bis_v1_assigns_normal_part2.json | 13 +++
.../init_t2_bis_v1_loop_assigns_part2.json | 13 +++
.../init_t2_bis_v1_loop_assigns_part3.json | 13 +++
.../init_t2_bis_v2_assigns_exit_part2.json | 36 ++++++++
.../init_t2_bis_v2_assigns_normal_part2.json | 36 ++++++++
.../init_t2_bis_v2_loop_assigns_part2.json | 36 ++++++++
.../init_t2_bis_v2_loop_assigns_part3.json | 13 +++
.../script/init_t2_v1_assigns_part2.json | 13 +++
.../init_t2_v1_loop_assigns_2_part2.json | 13 +++
.../init_t2_v1_loop_assigns_2_part3.json | 13 +++
.../script/init_t2_v1_loop_assigns_part2.json | 13 +++
.../script/init_t2_v1_loop_assigns_part3.json | 13 +++
.../script/init_t2_v2_assigns_part2.json | 36 ++++++++
.../init_t2_v2_loop_assigns_2_part2.json | 36 ++++++++
.../init_t2_v2_loop_assigns_2_part3.json | 13 +++
.../script/init_t2_v2_loop_assigns_part2.json | 36 ++++++++
.../script/init_t2_v2_loop_assigns_part3.json | 36 ++++++++
.../script/init_t2_v3_assigns_part2.json | 36 ++++++++
.../script/init_t2_v3_loop_assigns_part2.json | 36 ++++++++
.../script/init_t2_v3_loop_assigns_part3.json | 13 +++
.../oracle_qualif/user_init.1.res.oracle | 1 +
.../init_t2_bis_v2_assigns_exit_part2.json | 10 +++
.../init_t2_bis_v2_assigns_normal_part2.json | 10 +++
.../init_t2_bis_v2_loop_assigns_part2.json | 38 ++++++++
.../init_t2_bis_v2_loop_assigns_part3.json | 86 +++++++++++++++++++
.../script/init_t2_v2_assigns_part2.json | 10 +++
.../init_t2_v2_loop_assigns_2_part2.json | 38 ++++++++
.../init_t2_v2_loop_assigns_2_part3.json | 86 +++++++++++++++++++
.../script/init_t2_v2_loop_assigns_part2.json | 38 ++++++++
.../script/init_t2_v2_loop_assigns_part3.json | 38 ++++++++
.../script/init_t2_v3_assigns_part2.json | 10 +++
.../script/init_t2_v3_loop_assigns_part2.json | 38 ++++++++
.../script/init_t2_v3_loop_assigns_part3.json | 86 +++++++++++++++++++
.../oracle_qualif/user_init.2.res.oracle | 2 +-
src/plugins/wp/tests/wp_typed/user_init.i | 4 +-
48 files changed, 1038 insertions(+), 38 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.session/script/init_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_exit_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_assigns_normal_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v1_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_exit_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_assigns_normal_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_bis_v2_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_2_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v1_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_2_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v2_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.session/script/init_t2_v3_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 9b3384e53f8..47549ee4316 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 db0cb3b6584..fe94b79d5a0 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 1e81d96a466..83c8419f1b0 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 7a54adc27e1..086100cee33 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 82b3b1d5d8c..4f622671cdd 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 1d455c31d80..f52b6b9b19f 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 31b0e5ca191..5efd85925f1 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 00000000000..bd263392345
--- /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 7ee8ff1e6b0..edd11a46ad8 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 2c728ac4288..49c2566726f 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 4b005c11a31..d488804035c 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 a4bc55ce426..6752a74f693 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 00000000000..5cf9423e22d
--- /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 00000000000..5cf9423e22d
--- /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 00000000000..9e5622f6d53
--- /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 00000000000..71fa062236e
--- /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 00000000000..84546c12c64
--- /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 00000000000..ebfb03dd03a
--- /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 00000000000..337706ad80c
--- /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 00000000000..71fa062236e
--- /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 00000000000..ce3491eaf9b
--- /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 00000000000..eb4dd79d6b4
--- /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 00000000000..a7ba59113ad
--- /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 00000000000..8d897fef832
--- /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 00000000000..9e5622f6d53
--- /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 00000000000..bd817f1424e
--- /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 00000000000..9938bd71290
--- /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 00000000000..a7ba59113ad
--- /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 00000000000..06157667437
--- /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 00000000000..3b03ebb08ed
--- /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 00000000000..a59995dbef4
--- /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 00000000000..abc610f8dfa
--- /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 00000000000..08661a75e46
--- /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 3f6e407c1d3..3a972745592 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 00000000000..cfbcd4dd1ca
--- /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 00000000000..cfbcd4dd1ca
--- /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 00000000000..ecb82b8fa1c
--- /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 00000000000..e395695e644
--- /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 00000000000..85ffcc33852
--- /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 00000000000..4b77a3694b5
--- /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 00000000000..aca21574a96
--- /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 00000000000..ba59bc83677
--- /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 00000000000..81b95722e76
--- /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 00000000000..736aad8f408
--- /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 00000000000..c5f4b0bf30c
--- /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 00000000000..ae77b380278
--- /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 58e3100351f..21d17e27f81 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 a22e23c5afc..6bda4f9640b 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 ;
--
GitLab