From c1ebf07973151ab4a35db327bfc7d0fb7eecd245 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 10 Sep 2019 17:21:38 +0200
Subject: [PATCH] [wp/cache] assign a session to each test
---
src/plugins/wp/tests/test_config_qualif | 2 +-
.../unsigned.0.session}/typed/typed_lemma_U32.json | 0
src/plugins/wp/tests/wp_plugin/unsigned.i | 2 +-
.../typed/typed_split_ensures_Goal_Exist_And.json | 0
.../typed/typed_split_ensures_Goal_Exist_And_bis.json | 0
.../typed/typed_split_ensures_Goal_Exist_Or.json | 0
.../typed/typed_split_ensures_Hyp_Forall_And.json | 0
.../typed/typed_split_ensures_Hyp_Forall_Or_bis.json | 0
src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i | 2 +-
.../wp_typed/oracle_qualif/user_init.1.res.oracle | 3 +--
.../typed/typed_init_t2_bis_v2_assigns_exit_part2.json | 10 ++++++++++
.../typed_init_t2_bis_v2_assigns_normal_part2.json | 10 ++++++++++
.../typed/typed_init_t2_bis_v2_loop_assigns_part2.json | 10 ++++++++++
.../typed/typed_init_t2_bis_v2_loop_assigns_part3.json | 10 ++++++++++
.../typed/typed_init_t2_v2_assigns_part2.json | 10 ++++++++++
.../typed/typed_init_t2_v2_loop_assigns_2_part2.json | 10 ++++++++++
.../typed/typed_init_t2_v2_loop_assigns_2_part3.json | 10 ++++++++++
.../typed/typed_init_t2_v2_loop_assigns_part2.json | 10 ++++++++++
.../typed/typed_init_t2_v2_loop_assigns_part3.json | 10 ++++++++++
.../typed/typed_init_t2_v3_assigns_part2.json | 10 ++++++++++
.../typed/typed_init_t2_v3_loop_assigns_part2.json | 10 ++++++++++
.../typed/typed_init_t2_v3_loop_assigns_part3.json | 10 ++++++++++
src/plugins/wp/tests/wp_typed/user_init.i | 4 ++--
23 files changed, 126 insertions(+), 7 deletions(-)
rename src/plugins/wp/tests/wp_plugin/{unsigned/wp => oracle_qualif/unsigned.0.session}/typed/typed_lemma_U32.json (100%)
rename src/plugins/wp/tests/wp_tip/{tac_split_quantifiers/wp => oracle_qualif/tac_split_quantifiers.0.session}/typed/typed_split_ensures_Goal_Exist_And.json (100%)
rename src/plugins/wp/tests/wp_tip/{tac_split_quantifiers/wp => oracle_qualif/tac_split_quantifiers.0.session}/typed/typed_split_ensures_Goal_Exist_And_bis.json (100%)
rename src/plugins/wp/tests/wp_tip/{tac_split_quantifiers/wp => oracle_qualif/tac_split_quantifiers.0.session}/typed/typed_split_ensures_Goal_Exist_Or.json (100%)
rename src/plugins/wp/tests/wp_tip/{tac_split_quantifiers/wp => oracle_qualif/tac_split_quantifiers.0.session}/typed/typed_split_ensures_Hyp_Forall_And.json (100%)
rename src/plugins/wp/tests/wp_tip/{tac_split_quantifiers/wp => oracle_qualif/tac_split_quantifiers.0.session}/typed/typed_split_ensures_Hyp_Forall_Or_bis.json (100%)
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part2.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part3.json
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 65769f4abb2..c71ba7beb2f 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,3 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 45 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report @PTEST_FILE@
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 45 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session @PTEST_FILE@
LOG: @PTEST_NAME@.@PTEST_NUMBER@.report.json
OPT:
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned/wp/typed/typed_lemma_U32.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/typed/typed_lemma_U32.json
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/unsigned/wp/typed/typed_lemma_U32.json
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/typed/typed_lemma_U32.json
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.i b/src/plugins/wp/tests/wp_plugin/unsigned.i
index 53b1efa1b81..b48f75fbbc3 100644
--- a/src/plugins/wp/tests/wp_plugin/unsigned.i
+++ b/src/plugins/wp/tests/wp_plugin/unsigned.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -session tests/wp_plugin/unsigned -wp-prover script
+ OPT: -wp-prover script
*/
/*@
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And_bis.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And_bis.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_And_bis.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_Or.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_Or.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_Or.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Goal_Exist_Or.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Hyp_Forall_And.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_And.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Hyp_Forall_And.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_Or_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Hyp_Forall_Or_bis.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_Or_bis.json
rename to src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/typed/typed_split_ensures_Hyp_Forall_Or_bis.json
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
index 7f99eb527c9..7d6f12f66d1 100644
--- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -load-module tests/wp_tip/TacNOP.ml -wp -wp-par 1 -wp-prover script -session tests/wp_tip/tac_split_quantifiers
+ OPT: -load-module tests/wp_tip/TacNOP.ml -wp -wp-par 1 -wp-prover script
*/
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 60c38cd4360..0a25b0620ac 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -10,8 +10,7 @@
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_assigns_part1 : Valid
-[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1'
-[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1/wp'
+[wp] Warning: creating session directory `tests/wp_typed/oracle_qualif/user_init.1.session'
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part3 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_exit_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json
new file mode 100644
index 00000000000..210fb9dcdcd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0174,
+ "steps": 12 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0186,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json
new file mode 100644
index 00000000000..b90d48fad56
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0183,
+ "steps": 12 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0199,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json
new file mode 100644
index 00000000000..6172c1f2b58
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0242,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0275,
+ "steps": 28 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json
new file mode 100644
index 00000000000..7fcdb05a3ec
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0244,
+ "steps": 16 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0246,
+ "steps": 22 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json
new file mode 100644
index 00000000000..9fac563fc17
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0083,
+ "steps": 9 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0075,
+ "steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json
new file mode 100644
index 00000000000..e14df9c1762
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0113,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0127,
+ "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json
new file mode 100644
index 00000000000..001f140e03b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0106,
+ "steps": 14 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0108,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json
new file mode 100644
index 00000000000..89a30ff9b66
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0175,
+ "steps": 18 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0191,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json
new file mode 100644
index 00000000000..41c6b029913
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0191,
+ "steps": 18 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.021,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json
new file mode 100644
index 00000000000..b52f15827c3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0055,
+ "steps": 9 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0068,
+ "steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part2.json
new file mode 100644
index 00000000000..94b6d3f27f2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part2.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0115,
+ "steps": 23 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.013,
+ "steps": 27 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part3.json
new file mode 100644
index 00000000000..0b50684631b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_loop_assigns_part3.json
@@ -0,0 +1,10 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-goal",
+ "target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
+ "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "children": { "Goal 1/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0091,
+ "steps": 17 } ],
+ "Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
+ "verdict": "valid", "time": 0.0097,
+ "steps": 21 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index a34d4664bb4..1ba6792df7b 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,7 +1,7 @@
/* run.config_qualif
- EXECNOW: rm -rf @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-1/
+ EXECNOW: rm -rf @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.1.session
OPT: -wp-prop=-lack,-tactic
- OPT: -wp-prop=tactic -wp-auto=wp:split -session @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@-session-@PTEST_NUMBER@
+ OPT: -wp-prop=tactic -wp-auto=wp:split
OPT: -wp-prop=lack -wp-steps 300
*/
/*@ requires \valid(a+(0..n-1)) ;
--
GitLab