From c8a809098f27bb47cd77d92aaae944f5fc4ed740 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 12 Oct 2020 12:35:07 +0200
Subject: [PATCH] [wp] script updates
---
.../script/split_ensures_Goal_Exist_And.json | 26 ++-----------
.../split_ensures_Goal_Exist_And_bis.json | 36 ++---------------
.../script/split_ensures_Goal_Exist_Or.json | 16 ++------
.../script/split_ensures_Hyp_Forall_And.json | 20 ++--------
.../split_ensures_Hyp_Forall_Or_bis.json | 39 ++-----------------
.../wp/tests/wp_tip/tac_split_quantifiers.i | 4 +-
.../init_t2_bis_v2_assigns_exit_part2.json | 2 +-
.../init_t2_bis_v2_assigns_normal_part2.json | 2 +-
.../init_t2_bis_v2_loop_assigns_part2.json | 2 +-
.../init_t2_bis_v2_loop_assigns_part3.json | 2 +-
.../script/init_t2_v2_assigns_part2.json | 2 +-
.../init_t2_v2_loop_assigns_2_part2.json | 2 +-
.../init_t2_v2_loop_assigns_2_part3.json | 2 +-
.../script/init_t2_v2_loop_assigns_part2.json | 2 +-
.../script/init_t2_v2_loop_assigns_part3.json | 2 +-
.../script/init_t2_v3_assigns_part2.json | 2 +-
.../script/init_t2_v3_loop_assigns_part2.json | 2 +-
.../script/init_t2_v3_loop_assigns_part3.json | 2 +-
18 files changed, 33 insertions(+), 132 deletions(-)
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
index 7e4bcea281b..260f73c47cb 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
@@ -1,24 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_P1 i_0) /\\ (P_Q1 i_2) /\\ (P_P2 i_1 i_2)\n/\\ (exists i_3:int.\n (P_Q2 i_0 i_3))",
- "pattern": "\\E\\E\\E&P_P1P_Q1P_P2\\E#3#1#2#1P_Q2" },
- "children": { "Goal 1/2": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0511159896851 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int. (P_Q1 i_0) /\\ (P_P2 i_1 i_0)",
- "pattern": "\\E\\E&P_Q1P_P2#1#0#1" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0514709949493 } ] } } ],
- "Goal 2/2": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0521941184998 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0:int. (P_P1 i_0) /\\ (exists i_1:int.\n (P_Q2 i_0 i_1))",
- "pattern": "\\E&P_P1\\E#1P_Q2#1#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515058040619 } ] } } ] } } ]
+ "pattern": "\\E" },
+ "children": { "Goal 1/2": [], "Goal 2/2": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
index a908ac4adb3..212235b3fe9 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
@@ -1,34 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2,i_3:int.\n(P_Q1 1) /\\ (P_P2 i_0 i_1) /\\ (P_R2 i_1 i_2)\n/\\ (exists i_4:int.\n (P_Q2 i_3 i_4))",
- "pattern": "\\E\\E\\E\\E&P_Q1P_P2P_R2\\E1#4#3#3#2" },
- "children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0512578487396 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int. (P_Q2 i_0 i_1)",
- "pattern": "\\E\\EP_Q2#1#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515179634094 } ] } } ],
- "Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0517938137054 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1,i_2:int. (P_P2 i_2 i_1) /\\ (P_R2 i_1 i_0)",
- "pattern": "\\E\\E\\E&P_P2P_R2#0#1#1#2" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515098571777 } ] } } ],
- "Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0528788566589 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "(P_Q1 1)",
- "pattern": "P_Q11" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515050888062 } ] } } ] } } ]
+ "pattern": "\\EP_Q11" },
+ "children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
index db3e60070bd..c70dddec42c 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
@@ -1,16 +1,6 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_Q1 1) \\/ (P_P1 i_0) \\/ (P_P2 i_1 i_2) \\/ (exists i_3:int.\n (P_Q2 i_0 i_3))",
- "pattern": "\\E\\E\\E|P_Q1P_P1P_P2\\E1#3#2#1P_Q2" },
- "children": { "Distrib (exists or)": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515348911285 },
- { "header": "NOP",
- "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "(P_Q1 1) \\/ (exists i_0:int.\n (P_P1 i_0)) \\/ (exists i_0,i_1:int.\n (P_P2 i_1 i_0))\n\\/ (exists i_0,i_1:int.\n (P_Q2 i_0 i_1))",
- "pattern": "|P_Q1\\E\\E\\E1P_P1\\E\\E#0P_P2P_Q2#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0513439178467 } ] } } ] } } ]
+ "pattern": "\\EP_Q11" },
+ "children": { "Split": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
index bb1f7b0cb5b..5a6e83f4523 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
@@ -1,18 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2:int.\n(P_Q1 1) /\\ (P_P1 i_0) /\\ (P_P2 i_1 i_2) /\\ (forall i_3:int.\n (P_Q2 i_0 i_3))",
- "pattern": "\\F\\F\\F&P_Q1P_P1P_P2\\F1#3#2#1P_Q2" },
- "children": { "Distrib (forall and)": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.051558971405 },
- { "header": "NOP",
- "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0,
- "kind": "have",
- "target": "(P_Q1 1) /\\ (forall i_0:int.\n (P_P1 i_0)) /\\ (forall i_0,i_1:int.\n (P_P2 i_1 i_0))\n/\\ (forall i_0,i_1:int.\n (P_Q2 i_0 i_1))",
- "pattern": "&P_Q1\\F\\F\\F1P_P1\\F\\F#0P_P2P_Q2#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0513830184937 } ] } } ] } } ]
+ "pattern": "\\FP_Q11" },
+ "children": { "Split (distrib forall and)": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
index 815a03e3dd6..43bb875d32b 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
@@ -1,37 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2,i_3:int.\n(P_Q1 1) \\/ (P_P2 i_0 i_1) \\/ (P_R2 i_1 i_2)\n\\/ (forall i_4:int.\n (P_Q2 i_3 i_4))",
- "pattern": "\\F\\F\\F\\F|P_Q1P_P2P_R2\\F1#4#3#3#2" },
- "children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0511250495911 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0, "kind": "have",
- "target": "forall i_0,i_1:int. (P_Q2 i_0 i_1)",
- "pattern": "\\F\\FP_Q2#1#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515208244324 } ] } } ],
- "Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0517539978027 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0, "kind": "have",
- "target": "forall i_0,i_1,i_2:int. (P_P2 i_2 i_1) \\/ (P_R2 i_1 i_0)",
- "pattern": "\\F\\F\\F|P_P2P_R2#0#1#1#2" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515398979187 } ] } } ],
- "Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0528609752655 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0, "kind": "have",
- "target": "(P_Q1 1)",
- "pattern": "P_Q11" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.051561832428 } ] } } ] } } ]
+ "pattern": "\\FP_Q11" },
+ "children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
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 7d6f12f66d1..119e483c91c 100644
--- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
@@ -17,7 +17,7 @@
predicate R2(integer a1, integer a2) reads \nothing ;
} */
-/*@ ensures Goal_Exist_Or:
+/*@ ensures Goal_Exist_Or:
(\exists integer a, b, c ;
P1(a) || P2(b, c) || Q1(1) || \exists integer d ; Q2(a,d)) ;
@@ -29,7 +29,7 @@
(\exists integer a, b, c, d ;
P2(a, b) && R2(b, c) && Q1(1) && \exists integer e ; Q2(d,e)) ;
- @ ensures Hyp_Forall_And:
+ @ ensures Hyp_Forall_And:
(\forall integer a, b, c ;
P1(a) && P2(b, c) && Q1(1) && \forall integer d ; Q2(a,d)
) ==>
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
index a5f8a971b9f..e2661ac0ea5 100644
--- 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
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
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
index a5f8a971b9f..e2661ac0ea5 100644
--- 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
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
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
index 1a1c4c0451c..a9310f3d139 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0236,
"steps": 41 } ],
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
index 398a69be748..a5b7496b8bc 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.018,
"steps": 29 } ],
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
index d7d87cb0431..2ee61e01ef2 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
"steps": 16 } ],
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
index 9927a473006..6defa5bcd74 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0177,
"steps": 40 } ],
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
index e43bf2a0c07..07c88e21be0 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i0$i$j$j9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0154,
"steps": 24 } ],
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
index 8138f144480..6f266473c3d 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0167,
"steps": 33 } ],
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
index c110027873b..33301d71a33 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0167,
"steps": 33 } ],
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
index 2f0e9f12c12..cb380dd3e39 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
"steps": 16 } ],
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
index 0f331f4933d..a9966d41d85 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0196,
"steps": 39 } ],
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
index 9fc6a77f392..0be61590020 100644
--- 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
@@ -1,7 +1,7 @@
[ { "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" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0152,
"steps": 27 } ],
--
GitLab