diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 688cd21a498bd9365fa822300f588371785a1883..195645368a150948bf933528a8990cd3325939eb 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1282,7 +1282,7 @@ let prove ?timeout ?steplimit ~prover wpo =
then Task.return VCS.no_result (* Only generate *)
else
let drv , config , task = prover_task prover task in
- if false && is_trivial task then
+ if is_trivial task then
Task.return VCS.valid
else
let mode = get_mode () in
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json
index e0c64dbd19c005bd7baa08847082f1b9199a1e47..64863ed1b30a21d7b49779d2a2414d5090217709 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json
@@ -1,49 +1,34 @@
-{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 34, "valid": 34,
- "rank": 0 },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 34, "valid": 34 },
"qed": { "total": 8, "valid": 8 },
- "wp:main": { "total": 42, "valid": 42, "rank": 0 } },
+ "wp:main": { "total": 42, "valid": 42 } },
"wp:functions": { "f": { "f_ensures_f1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_f0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o9": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o6": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o5": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o4": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
@@ -53,107 +38,73 @@
"wp:main": { "total": 1,
"valid": 1 } },
"f_ensures_o2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_o0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a9": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a6": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a5": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a4": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a3": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_a0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i9": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i6": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i5": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
@@ -163,23 +114,17 @@
"wp:main": { "total": 1,
"valid": 1 } },
"f_ensures_i3": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_i0": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
@@ -189,59 +134,43 @@
"wp:main": { "total": 1,
"valid": 1 } },
"f_ensures_p8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_p7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_p6": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"f_ensures_p5": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_p4": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"f_ensures_p3": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_p2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_p1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"f_ensures_p0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 0 } },
+ "valid": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 34,
- "valid": 34,
- "rank": 0 },
+ "valid": 34 },
"qed": { "total": 8, "valid": 8 },
"wp:main": { "total": 42,
- "valid": 42,
- "rank": 0 } } } } }
+ "valid": 42 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
index 8a4506b88c4a87d8e13a03c7e04048e9fa5b3b67..eb84ef54e1719a8eb9e9af4afa0e1caba90ad8f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
@@ -53,5 +53,5 @@
[wp] Report out: 'tests/wp_acsl/result_qualif/e_imply.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-f 8 34 (1..8) 42 100%
+f 8 34 42 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
index d6ca451c6b4efa8cb9f5c7ff5e33fa5744bc2c70..6fe581a3fda56826a0a36332c0216385690fe68c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
@@ -1,11 +1,9 @@
{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 2, "valid": 2, "rank": 0 },
"wp:main": { "total": 2, "valid": 2, "rank": 1 } },
"wp:functions": { "foo": { "foo_assert_B": { "why3:Alt-Ergo,2.0.0":
- { "total": 1, "valid": 1,
- "rank": 0 },
+ { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 1 } },
+ "valid": 1 } },
"foo_assert_A": { "why3:Alt-Ergo,2.0.0":
{ "total": 1, "valid": 1,
"rank": 0 },
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index 6ade8dc8e47d7d62db7bc92fceb4ac95519e0ca2..d896e322fd3320bd1a0aaa355b0dd971e9b9eb6c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
@@ -16,5 +16,5 @@
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f3 1 - 1 100%
-g3 1 2 (1..12) 3 100%
+g3 1 2 3 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
index ec62cdf34b1f7eef83897b5dd0f04f40c77fc8c2..32a7cab92e8f4145b8359eaa4952a7778af2db67 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
@@ -1,14 +1,10 @@
-{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 0 },
- "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1, "valid": 1 } },
"wp:axiomatics": { "": { "lemma_foo": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 1 } },
+ "valid": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 0 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 1 } } } } }
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
index f9611321b0c07ecc9cd0cd6a62b5fd80c99f8ad4..fe6b5998b58d94698d5b245fe644dbde90c64297 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
@@ -11,5 +11,5 @@
[wp] Report out: 'tests/wp_bts/result_qualif/issue_447.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Lemma - 1 (1..12) 1 100%
+Lemma - 1 1 100%
-------------------------------------------------------------