diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 7dd358acc6900842611fed12bc90a0c096eaa60c..b46c539ca5100a4cb67bce7395195998f3582f92 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -105,6 +105,14 @@ predicate "\\is_plus_infinity"(float32) = "is_positive_infinite_f32";
 predicate "\\is_plus_infinity"(float64) = "is_positive_infinite_f64";
 predicate "\\is_minus_infinity"(float32) = "is_negative_infinite_f32";
 predicate "\\is_minus_infinity"(float64) = "is_negative_infinite_f64";
+predicate "\\le_float"(float32,float32) = "le_f32";
+predicate "\\lt_float"(float32,float32) = "lt_f32";
+predicate "\\eq_float"(float32,float32) = "eq_f32";
+predicate "\\ne_float"(float32,float32) = "ne_f64";
+predicate "\\le_double"(float64,float64) = "le_f64";
+predicate "\\lt_double"(float64,float64) = "lt_f64";
+predicate "\\eq_double"(float64,float64) = "eq_f64";
+predicate "\\ne_double"(float64,float64) = "ne_f64";
 logic bool "\\round_float"(rounding_mode,real) = "round_float";
 logic bool "\\round_double"(rounding_mode,real) = "round_double";
 
diff --git a/src/plugins/wp/tests/wp_acsl/float_compare.i b/src/plugins/wp/tests/wp_acsl/float_compare.i
new file mode 100644
index 0000000000000000000000000000000000000000..733948471e99000435635ea8c6e9e95d0e82923d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i
@@ -0,0 +1,11 @@
+/*@ lemma test_float_compare:
+      \forall float x,y;
+      \is_finite(x) && \is_finite(y) ==>
+      \le_float(x,y) ==> \lt_float(x,y) || \eq_float(x,y);
+*/
+
+/*@ lemma test_double_compare:
+      \forall double x,y;
+      \is_finite(x) && \is_finite(y) ==> \le_double(x,y) ==>
+         \lt_double(x,y) || \eq_double(x,y);
+*/
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
new file mode 100644
index 0000000000000000000000000000000000000000..ddab6355e44826b7418f0cb0c0b2f53d1b0ea8ff
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+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))
+
+------------------------------------------------------------
+
+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))
+
+------------------------------------------------------------