diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
index 5f84563cec3089f4f167469fff0929adb9efeb1d..c5f42638ec144f5d8687baf14c8df58825610e5b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
@@ -10,8 +10,8 @@
"pattern": "&<=<=<=0$x0land$x42949672954294967295" },
"children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid",
- "time": 0.0205,
- "steps": 14 } ],
+ "time": 0.021,
+ "steps": 12 } ],
"Goal 2/3": [ { "header": "Bit Range",
"tactic": "Wp.bitrange",
"params":
@@ -27,6 +27,6 @@
"verdict": "valid" } ] } } ],
"Goal 3/3": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "valid",
- "time": 0.0201,
- "steps": 14 } ] } } ],
+ "time": 0.0189,
+ "steps": 12 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
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 fe94e71f4e36bfc5145d9ee7166f985dad69dbfb..ac9e9645d05b5e943c48e0df926808e293879219 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
@@ -3,7 +3,7 @@
"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.3.0",
- "verdict": "valid", "time": 0.1131,
+ "verdict": "valid", "time": 0.0876,
"steps": 51 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
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 fe94e71f4e36bfc5145d9ee7166f985dad69dbfb..ac9e9645d05b5e943c48e0df926808e293879219 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
@@ -3,7 +3,7 @@
"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.3.0",
- "verdict": "valid", "time": 0.1131,
+ "verdict": "valid", "time": 0.0876,
"steps": 51 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
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 2fdf4f699b8fa852722346cb61744294e8705995..dae648761762db5157c8fda0543bbf868312682f 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
@@ -3,8 +3,8 @@
"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.3.0",
- "verdict": "valid", "time": 0.7529,
- "steps": 75 } ],
+ "verdict": "valid", "time": 0.8178,
+ "steps": 88 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 61905e9c1cf22653529a3de6753fbe2dd48c0bd8..0f29709407bc0b8a2e62bf0006c6883a7684e85c 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
@@ -3,8 +3,8 @@
"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.3.0",
- "verdict": "valid", "time": 0.0324,
+ "verdict": "valid", "time": 0.0318,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.4933,
- "steps": 404 } ] } } ]
+ "verdict": "valid", "time": 0.562,
+ "steps": 414 } ] } } ]
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 452a24b9d43114b37328901b917359252755c486..88270611f30de89ca035c371d975b464637ab1bf 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
@@ -3,8 +3,8 @@
"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.3.0",
- "verdict": "valid", "time": 0.5313,
- "steps": 65 } ],
+ "verdict": "valid", "time": 0.6393,
+ "steps": 63 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 67ead11b4b8fe83231abe07e53f92b0236d09580..bb9877d0edec46bfc076a60c8fec6e40a38d39dd 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
@@ -3,8 +3,8 @@
"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.3.0",
- "verdict": "valid", "time": 0.4321,
- "steps": 57 } ],
+ "verdict": "valid", "time": 0.4508,
+ "steps": 55 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 e4e625f3a148d53c54500eb5ad34d3806edd6fa5..bc59c057755459f749de24cab6d58ac381fc28e6 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
@@ -3,8 +3,8 @@
"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.3.0",
- "verdict": "valid", "time": 0.4321,
- "steps": 57 } ],
+ "verdict": "valid", "time": 0.4508,
+ "steps": 55 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",
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 b857b733938474844e7c9d655787f6035889b4cf..c128ee8585d1150eee8299f9655216d8f870f3e3 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
@@ -3,8 +3,8 @@
"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.3.0",
- "verdict": "valid", "time": 0.0324,
+ "verdict": "valid", "time": 0.0318,
"steps": 39 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.4933,
- "steps": 404 } ] } } ]
+ "verdict": "valid", "time": 0.562,
+ "steps": 414 } ] } } ]
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 5bbf5688947048214a064832b925b46eec8024cb..a233cfc63116980ec3afdda54cf88447e3faf3e3 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
@@ -3,8 +3,8 @@
"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.3.0",
- "verdict": "valid", "time": 0.3617,
- "steps": 72 } ],
+ "verdict": "valid", "time": 0.3477,
+ "steps": 70 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
"verdict": "timeout", "time": 10. },
{ "header": "Range", "tactic": "Wp.range",