diff --git a/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json b/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
new file mode 100644
index 0000000000000000000000000000000000000000..8ab9ce87bfcce6699c3d4d058f75fa169519f276
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
@@ -0,0 +1,39 @@
+{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 8 },
+ "wp:main": { "total": 4, "valid": 4, "rank": 8 } },
+ "wp:axiomatics": { "": { "lemma_test_float_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_float_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "wp:section": { "alt-ergo": { "total": 4,
+ "valid": 4,
+ "rank": 8 },
+ "wp:main": { "total": 4,
+ "valid": 4,
+ "rank": 8 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
index c376b86e98ce5ec321a21c7b88f978e7d29d847d..8ce615934da8264b474018856ccfe959b005583b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
@@ -8,17 +8,17 @@
Lemma InfN_not_finite:
Assume: 'InfP_not_finite' 'NaN_not_finite'
-Prove: (not (\is_finite x_0)) \/ (not (\is_minus_infinity x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_negative_infinite_f64 x_0))
------------------------------------------------------------
Lemma InfP_not_finite:
Assume: 'NaN_not_finite'
-Prove: (not (\is_finite x_0)) \/ (not (\is_plus_infinity x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_positive_infinite_f64 x_0))
------------------------------------------------------------
Lemma NaN_not_finite:
-Prove: (not (\is_finite x_0)) \/ (not (\is_NaN x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_NaN_f64 x_0))
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
index f4648555636b165df364b453c51b81c3aa30b7f2..a31e1893ff76431ccf8b5d83313080b8d476d614 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
@@ -8,28 +8,28 @@
Lemma test_double_compare:
Assume: 'test_float_compare'
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_double x_0 y_0)
- -> ((\lt_double x_0 y_0) \/ (\eq_double x_0 y_0))
+Prove: (is_finite_f64 x_0) -> (is_finite_f64 y_0) -> (le_f64 x_0 y_0)
+ -> ((eq_f64 x_0 y_0) \/ (lt_f64 x_0 y_0))
------------------------------------------------------------
Lemma test_double_compare_greater:
Assume: 'test_float_compare_greater' 'test_double_compare'
'test_float_compare'
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_double y_0 x_0)
- -> ((\lt_double y_0 x_0) \/ (\eq_double x_0 y_0))
+Prove: (is_finite_f64 x_0) -> (is_finite_f64 y_0) -> (le_f64 y_0 x_0)
+ -> ((eq_f64 x_0 y_0) \/ (lt_f64 y_0 x_0))
------------------------------------------------------------
Lemma test_float_compare:
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_float x_0 y_0)
- -> ((\lt_float x_0 y_0) \/ (\eq_float x_0 y_0))
+Prove: (is_finite_f32 x_0) -> (is_finite_f32 y_0) -> (le_f32 x_0 y_0)
+ -> ((eq_f32 x_0 y_0) \/ (lt_f32 x_0 y_0))
------------------------------------------------------------
Lemma test_float_compare_greater:
Assume: 'test_double_compare' 'test_float_compare'
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_float y_0 x_0)
- -> ((\lt_float y_0 x_0) \/ (\eq_float x_0 y_0))
+Prove: (is_finite_f32 x_0) -> (is_finite_f32 y_0) -> (le_f32 y_0 x_0)
+ -> ((eq_f32 x_0 y_0) \/ (lt_f32 y_0 x_0))
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..828ad921cb7fc2d46ee73514a319c1d5d5330e5c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 4 goals scheduled
+[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare_greater : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare_greater : Valid
+[wp] Proved goals: 4 / 4
+ Qed: 0
+ Alt-Ergo: 4
+[wp] Report 'tests/wp_acsl/float_compare.i.0.report.json'
+-------------------------------------------------------------
+Axiomatics WP Alt-Ergo Total Success
+Lemma - 4 (28..40) 4 100%
+-------------------------------------------------------------