diff --git a/src/plugins/wp/tests/why3/test_config_qualif b/src/plugins/wp/tests/why3/test_config_qualif
index 20cc940510516da835ce196f2116d17c92f852dc..d460c393a3886a28e1b52298662e0da78133aad3 100644
--- a/src/plugins/wp/tests/why3/test_config_qualif
+++ b/src/plugins/wp/tests/why3/test_config_qualif
@@ -1,6 +1,6 @@
FILEREG: .*\.why
DEPS: ~/.why3.conf
-CMD: why3 -L @PTEST_SHARE_DIR@/why3 prove -P Alt-Ergo,2.5.3
+CMD: why3 -L @PTEST_SHARE_DIR@/why3 prove -P Alt-Ergo,2.5.4
OPT:
COMMENT: the filter remove the information about time and steps
FILTER: sed -e 's|\(.*\)\( (.*)\)|\1|'
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
index 354ccb74d2244c27183571008f2892d492d662ab..00fcc7e2ae221b8b4852cf7d3613e377d587158a 100644
--- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
+++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_n.json
@@ -1,9 +1,8 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0204 },
- { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
+[ { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
"select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "not (bit_test off_0 15)",
"pattern": "!bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ],
- "Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0204,
- "steps": 52 } ] } } ]
+ "Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.027549,
+ "steps": 38 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
index 67707c14b561e32c4966a9632edfeebd7e1319bc..ca56f4319e46e35d7376d4ccccd13f9ebbc99e35 100644
--- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
+++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.0.session_qualif/script/lemma_res_y.json
@@ -1,9 +1,8 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0194 },
- { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
+[ { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
"select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "(bit_test off_0 15)",
"pattern": "bit_test$off15" },
- "children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0194,
- "steps": 52 } ],
+ "children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.021835,
+ "steps": 37 } ],
"Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ]
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 864714c2b1858ef24cb2792b56024597648f1a3f..00ab6f9978ea19333f0363248bb6364fa7ae643d 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,8 +1,8 @@
----------------------------------------------------------
WP Requirements for Qualif Tests
----------------------------------------------------------
-1. The Alt-Ergo theorem prover, version v2.5.3
-2. The Why3 platform, version 1.7.1
+1. The Alt-Ergo theorem prover, version v2.5.4
+2. The Why3 platform, version 1.7.2
3. The environment variable FRAMAC_WP_CACHEDIR is defined
4. The environment variable FRAMAC_WP_CACHE is defined
----------------------------------------------------------
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 6c923007a1824b9a86158c4527d8a020be54e708..beee3d22091cd02b1aa5d2156b7316f6f7f71565 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
@@ -5,7 +5,7 @@
[wp] [Valid] Goal job_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.3
+[wp] Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.4
[wp] [Valid] typed_job_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 3 / 3
Terminating: 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 234a6e8800cbb1e17294a80ef6c682dabc16a0f0..f447a53a23ff017dbbddeb48356325f836d63682 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -2,10 +2,10 @@
[kernel] Parsing unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_U32 (Tactic) (Qed 1/2)
-[wp] Proved goals: 0 / 1
- Unsuccess: 1
+[wp] [Valid] typed_lemma_U32 (Tactics 3) (Qed 4/4)
+[wp] Proved goals: 1 / 1
+ Script: 1 (Tactics 3) (Qed 4/4)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma - - 1 0.0%
+ Lemma - - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
index 692d239230f334e0e900e174b4552bc1b670ef07..9aba6ba2c937230978e14877ce4ee36237407981 100644
--- a/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
+++ b/src/plugins/wp/tests/wp_plugin/unsigned.0.session_qualif/script/lemma_U32.json
@@ -1,9 +1,28 @@
-[ { "prover": "script", "verdict": "unknown" },
- { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
+[ { "header": "Bitwise Eq.", "tactic": "Wp.bitwised",
"params": { "Wp.bitwised.range": 32 },
"select": { "select": "clause-goal",
"target": "(land 4294967295 x_0)=x_0",
"pattern": "=land$x4294967295$x" },
- "children": { "range": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
+ "children": { "range": [ { "header": "Split", "tactic": "Wp.split",
+ "params": {},
+ "select": { "select": "clause-goal",
+ "target": "(0<=x_0) /\\ (0<=(land 4294967295 x_0)) /\\ (x_0<=4294967295)",
+ "pattern": "&<=<=<=0$x0land$x42949672954294967295" },
+ "children": { "Goal 1/3": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Goal 2/3": [ { "header": "Bit Range",
+ "tactic": "Wp.bitrange",
+ "params":
+ { "positive-land": true,
+ "positive-lor": true },
+ "select":
+ { "select": "clause-goal",
+ "target": "0<=(land 4294967295 x_0)",
+ "pattern": "<=0land4294967295$x" },
+ "children":
+ { "bit-range":
+ [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
+ "Goal 3/3": [ { "prover": "qed",
+ "verdict": "valid" } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
index 41ee719bb82c103a86a5638b12b3a3b0d36c89aa..18d14b4efae46482cc8cf387507a54b4d09cff5d 100644
--- a/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/induction.0.session_qualif/script/lemma_ByInd.json
@@ -1,13 +1,12 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.04 },
- { "header": "Induction", "tactic": "Wp.induction",
+[ { "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
"pattern": "L_f$x" },
- "children": { "Base": [ { "prover": "Alt-Ergo:2.5.3", "verdict": "valid",
- "time": 0.0035, "steps": 14 } ],
- "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0247,
- "steps": 325 } ],
- "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0118,
- "steps": 32 } ] } } ]
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4", "verdict": "valid",
+ "time": 0.013909, "steps": 4 } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.02138,
+ "steps": 88 } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid",
+ "time": 0.026118, "steps": 116 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
index c3ad89aead453959667b97cd96a703614dbd5779..df8aacace3c8dcead7143954ab5ad0d0a2b0b642 100644
--- a/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/induction.1.session_qualif/script/lemma_ByInd.json
@@ -1,11 +1,10 @@
-[ { "prover": "script", "verdict": "unknown" },
- { "header": "Induction", "tactic": "Wp.induction",
+[ { "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "x_0",
"pattern": "$x" },
- "children": { "Base": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ] } } ]
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
index cf36ff92b88a3fa74100e38dfd2b0bca347ee5f0..0abf008d8c26163b7f2980f7e8e557cf23f5086e 100644
--- a/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/induction.2.session_qualif/script/lemma_ByInd.json
@@ -1,11 +1,10 @@
-[ { "prover": "script", "verdict": "unknown" },
- { "header": "Induction", "tactic": "Wp.induction",
+[ { "header": "Induction", "tactic": "Wp.induction",
"params": { "base": { "select": "kint", "val": "0" } },
"select": { "select": "inside-goal", "occur": 0, "target": "y_0",
"pattern": "$y" },
- "children": { "Base": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ],
- "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "timeout", "time": 10. } ] } } ]
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
index e79e12e8f04e51c50d45c2d74c5bf023fc887ae8..a0ac010c2cbfa4cbf699ee50a596161b3002a25b 100644
--- a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
+++ b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_char.json
@@ -1,28 +1,27 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0322 },
- { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
+[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(to_uint32 c_0)", "pattern": "to_uint32$c" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0082,
- "steps": 32 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.024,
- "steps": 155 },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.026061,
+ "steps": 22 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.031304,
+ "steps": 53 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
"select": { "select": "inside-goal",
"occur": 0,
"target": "(to_uint32\n (ui_0+((4294967296+c_0+(-4294967296*(c_0 div 4294967296))) mod 4294967296)))",
"pattern": "to_uint32+$ui%+42949672964294967296" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.0166,
"steps": 27 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.023,
"steps": 25 } ],
- "Upper": [ { "prover": "Alt-Ergo:2.5.3",
+ "Upper": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.0739,
"steps": 73 } ] } } ],
diff --git a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
index ae6b0e0b2d26b25441baaf6ff1912b32c61f5daa..c76a50b502a10731bccff57827a293037e099cf4 100644
--- a/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
+++ b/src/plugins/wp/tests/wp_tip/overflow.0.session_qualif/script/lemma_j_incr_short.json
@@ -1,28 +1,27 @@
-[ { "prover": "script", "verdict": "valid", "time": 0.0235 },
- { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
+[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(to_uint32 s_0)", "pattern": "to_uint32$s" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0069,
- "steps": 32 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
- "verdict": "valid", "time": 0.0166,
- "steps": 154 },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.028956,
+ "steps": 22 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
+ "verdict": "valid", "time": 0.030726,
+ "steps": 52 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
"select": { "select": "inside-goal",
"occur": 0,
"target": "(to_uint32\n (ui_0+((4294967296+s_0+(-4294967296*(s_0 div 4294967296))) mod 4294967296)))",
"pattern": "to_uint32+$ui%+42949672964294967296" },
- "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.3",
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.017,
"steps": 27 } ],
- "Lower": [ { "prover": "Alt-Ergo:2.5.3",
+ "Lower": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.0232,
"steps": 25 } ],
- "Upper": [ { "prover": "Alt-Ergo:2.5.3",
+ "Upper": [ { "prover": "Alt-Ergo:2.5.4",
"verdict": "valid",
"time": 0.2614,
"steps": 73 } ] } } ],