diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
index 7c556d4141806acc8dcdadc91ed88bbcb6347e44..0b99ce986f78cd07b8a6b5654f4ceff5ff32b1cb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
@@ -7,8 +7,8 @@
[wp] [alt-ergo] Goal typed_lemma_InfP_not_finite : Valid
[wp] [alt-ergo] Goal typed_lemma_NaN_not_finite : Valid
[wp] Proved goals: 3 / 3
- Qed: 0
- alt-ergo: 3
+ Qed: 0
+ Alt-Ergo (why3): 3
[wp] Report in: 'tests/wp_acsl/oracle_qualif/classify_float.1.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.1.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
index 282eb4ee097169d400ac6fda89f02bba2f624197..b6f8e5f4ca87390017b9a4dc815d79323749f75a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
@@ -27,8 +27,8 @@
[wp] [alt-ergo] Goal typed_f_ensures_sm2_mod_pos_neg : Valid
[wp] [alt-ergo] Goal typed_f_ensures_sm3_mod_neg_neg : Valid
[wp] Proved goals: 22 / 22
- Qed: 0
- alt-ergo: 22
+ Qed: 0
+ Alt-Ergo (why3): 22
[wp] Report in: 'tests/wp_acsl/oracle_qualif/div_mod.1.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/div_mod.1.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
index 2da222911d19ad271fd2deb124a14860cc20d05f..bb43d9e7d045942fca067cceb970333d2504e712 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
@@ -5,17 +5,17 @@
[wp] 2 goals scheduled
[wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
[wp] [Failed] Goal typed_lemma_ok_because_inconsistent
- alt-ergo: Failed Command './tests/inexistant-prover' not found
+ Alt-Ergo (why3): Failed Command './tests/inexistant-prover' not found
Coq: Failed Command './tests/inexistant-prover' not found
Alt-Ergo: Failed Command './tests/inexistant-prover' not found
[wp] [Failed] Goal typed_lemma_ok_because_consistent
- alt-ergo: Failed Command './tests/inexistant-prover' not found
+ Alt-Ergo (why3): Failed Command './tests/inexistant-prover' not found
Coq: Failed Command './tests/inexistant-prover' not found
Alt-Ergo: Failed Command './tests/inexistant-prover' not found
[wp] Proved goals: 0 / 2
- Alt-Ergo: 0 (failed: 2)
- Coq: 0 (failed: 2)
- alt-ergo: 0 (failed: 2)
+ Alt-Ergo: 0 (failed: 2)
+ Coq: 0 (failed: 2)
+ Alt-Ergo (why3): 0 (failed: 2)
[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_143.1.report.json'
[wp] Report out: 'tests/wp_bts/result_qualif/issue_143.1.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 396326b005b520a4b9cf7b9a8c19d8bc591b7d78..cfdf8aa156445dedfdb553323c23d47d1f6935d6 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -15,8 +15,8 @@
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 10 / 10
- Qed: 3
- alt-ergo: 7
+ Qed: 3
+ Alt-Ergo (why3): 7
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json'
-------------------------------------------------------------
@@ -44,8 +44,8 @@ BinaryMultiplication 2 - 9 100%
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 11 / 14
- Qed: 0
- alt-ergo: 11
+ Qed: 0
+ Alt-Ergo (why3): 11
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index df6617e5ab9f5edaf06c64480e7c4c954c62eecf..65f0dab3fc417628a1c4e112779701e6b28a123c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -22,8 +22,8 @@
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 17 / 17
- Qed: 4
- alt-ergo: 13
+ Qed: 4
+ Alt-Ergo (why3): 13
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json'
-------------------------------------------------------------
@@ -54,8 +54,8 @@ BinaryMultiplication 3 - 13 100%
[wp] [alt-ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 13 / 17
- Qed: 0
- alt-ergo: 13
+ Qed: 0
+ Alt-Ergo (why3): 13
[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json'
[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
index a1093f1b4861b2d3ae2f15713b6d96b92f040ac0..4e80668bd541c3350f12f087e7854e0aa3b64ef2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
@@ -6,8 +6,8 @@
[wp] 1 goal scheduled
[wp] [alt-ergo] Goal typed_abs_abs_ensures : Valid
[wp] Proved goals: 1 / 1
- Qed: 0
- alt-ergo: 1
+ Qed: 0
+ Alt-Ergo (why3): 1
[wp] Report in: 'tests/wp_plugin/oracle_qualif/abs.2.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/abs.2.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index 6a81ceb4c392d1afee59e84d5c7e119ffbe3f686..90b1a19b2993d1c6b2f0f8e1b361829f46706d81 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
@@ -6,8 +6,8 @@
[wp] [alt-ergo] Goal typed_lemma_ceil : Valid
[wp] [alt-ergo] Goal typed_lemma_floor : Valid
[wp] Proved goals: 2 / 2
- Qed: 0
- alt-ergo: 2
+ Qed: 0
+ Alt-Ergo (why3): 2
----------------------------------------------------------
Axiomatics WP Alt-Ergo(Why3) Total Success
Lemma - 2 2 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
index f2836be71fc2b21813b17e0dcbdcf2b9476b3b67..fbad8e13cb9ed4b5f52902228fc7be6d674f9596 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
@@ -9,7 +9,7 @@
[wp] 1 goal scheduled
[wp] [alt-ergo] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1
- alt-ergo: 0 (unsuccess: 1)
+ Alt-Ergo (why3): 0 (unsuccess: 1)
[wp] Report in: 'tests/wp_plugin/oracle_qualif/float_format.2.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/float_format.2.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
index bf2477d381d6f7b5ff8ba62a2a2c42c38ecb3b38..239622cf211e24a9c72b03b7488c734a20b1dd66 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
@@ -35,8 +35,8 @@
[wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos : Valid
[wp] [alt-ergo] Goal typed_ok_ensures_sqrt_pos0 : Valid
[wp] Proved goals: 30 / 30
- Qed: 5
- alt-ergo: 25
+ Qed: 5
+ Alt-Ergo (why3): 25
----------------------------------------------------------
Axiomatics WP Alt-Ergo(Why3) Total Success
Lemma 3 16 19 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index c8da0ce71468d4f596928935394adb03d0ec72de..b36de4de9c7ae2b32c3d2f362cde9f748dbb614e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -14,7 +14,7 @@
[wp] [alt-ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
[wp] [alt-ergo] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
[wp] Proved goals: 0 / 9
- alt-ergo: 0 (unsuccess: 9)
+ Alt-Ergo (why3): 0 (unsuccess: 9)
----------------------------------------------------------
Functions WP Alt-Ergo(Why3) Total Success
ko - - 9 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
index 6f80bff20c45fd87f851cdfef06e10d470d4b85a..96da4b6f6ab9a6e68d9dc3c34128b339e5e800a6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
@@ -8,8 +8,8 @@
[wp] [alt-ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Valid
[wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
[wp] Proved goals: 4 / 4
- Qed: 1
- alt-ergo: 3
+ Qed: 1
+ Alt-Ergo (why3): 3
[wp] Report in: 'tests/wp_plugin/oracle_qualif/nth.1.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/nth.1.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index e2333a2acdc2db9f6a13713185d468dc73581e4a..922a6a40b60d55d71f3e81dcf31586c4edd3b283 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
@@ -39,8 +39,8 @@
[wp] [Qed] Goal typed_caveat_sequence_g_not_called_ensures_ok_q2 : Valid
[wp] [alt-ergo] Goal typed_caveat_sequence_g_not_called_ensures_ok_q3 : Valid
[wp] Proved goals: 34 / 34
- Qed: 22
- alt-ergo: 12
+ Qed: 22
+ Alt-Ergo (why3): 12
[wp] Report in: 'tests/wp_plugin/oracle_qualif/sequence.1.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/sequence.1.report.json'
-------------------------------------------------------------