diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 39c437ff77f71ad07bd77057f2652d8c9e10f289..24d629f9c2cecfd7b349d077ff15e7c3229dc8b0 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -91,6 +91,7 @@ type op =
   | NE
   | NEG
   | ADD
+  | SUB
   | MUL
   | DIV
   | REAL
@@ -105,6 +106,7 @@ let op_name = function
   | NE -> "ne"
   | NEG -> "neg"
   | ADD -> "add"
+  | SUB -> "sub"
   | MUL -> "mul"
   | DIV -> "div"
   | REAL -> "of"
@@ -275,6 +277,7 @@ let compute_float op ulp xs =
   match op , xs with
   | NEG , [ x ] -> qmake ulp (Q.neg (exact x))
   | ADD , [ x ; y ] -> qmake ulp (Q.add (exact x) (exact y))
+  | SUB , [ x ; y ] -> qmake ulp (Q.sub (exact x) (exact y))
   | MUL , [ x ; y ] -> qmake ulp (Q.mul (exact x) (exact y))
   | DIV , [ x ; y ] ->
       let res = match Q.div (exact x) (exact y) with
@@ -293,6 +296,7 @@ let compute_real op xs =
   match op , xs with
   | NEG , [ x ] -> F.e_opp x
   | ADD , [ x ; y ] -> F.e_add x y
+  | SUB , [ x ; y ] -> F.e_sub x y
   | MUL , [ x ; y ] -> F.e_mul x y
   | DIV , [ x ; y ] -> F.e_div x y
   | (ROUND|REAL) , [ x ] -> x
@@ -350,6 +354,7 @@ let flt_le ft = Compute.get (Context.get model, ft, LE) |> fst
 let flt_lt ft = Compute.get (Context.get model, ft, LT) |> fst
 let flt_neg ft = Compute.get (Context.get model, ft, NEG) |> fst
 let flt_add ft = Compute.get (Context.get model, ft, ADD) |> fst
+let flt_sub ft = Compute.get (Context.get model, ft, SUB) |> fst
 let flt_mul ft = Compute.get (Context.get model, ft, MUL) |> fst
 let flt_div ft = Compute.get (Context.get model, ft, DIV) |> fst
 let flt_of_real ft = Compute.get (Context.get model, ft, ROUND) |> fst
@@ -435,16 +440,14 @@ let fcmp rop fop f x y =
   | Float -> p_call (fop f) [x;y]
 
 let fadd = fbinop e_add flt_add
+let fsub = fbinop e_sub flt_sub
 let fmul = fbinop e_mul flt_mul
 let fdiv = fbinop e_div flt_div
-
 let fopp f x =
   match Context.get model with
   | Real -> e_opp x
   | Float -> e_fun ~result:(ftau f) (flt_neg f) [x]
 
-let fsub f x y = fadd f x (fopp f y)
-
 let flt = fcmp p_lt flt_lt
 let fle = fcmp p_leq flt_le
 let feq = fcmp p_equal flt_eq
diff --git a/src/plugins/wp/Cfloat.mli b/src/plugins/wp/Cfloat.mli
index 344ddbc093e210b08c1b87114f4252cd21da307d..c685e9139ea638eadb6cf2a49ddc946c0033e8f1 100644
--- a/src/plugins/wp/Cfloat.mli
+++ b/src/plugins/wp/Cfloat.mli
@@ -50,6 +50,7 @@ type op =
   | NE
   | NEG
   | ADD
+  | SUB
   | MUL
   | DIV
   | REAL
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
index 3cfc3d7f07f7a38907537385c65ad9b590d72ee1..3f1bc5eb1b79440418007e44bed89924f9feb01a 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
@@ -145,10 +145,15 @@ theory Cfloat
   function add_f32 (x:f32) (y:f32) : f32 = F32.(.+) x y
   function add_f64 (x:f64) (y:f64) : f64 = F64.(.+) x y
 
+  (* Substraction *)
+
+  function sub_f32 (x:f32) (y:f32) : f32 = F32.(.-) x y
+  function sub_f64 (x:f64) (y:f64) : f64 = F64.(.-) x y
+
   (* Multiplication *)
 
-  function mul_f32 (x:f32) (y:f32) : f32 = F32.(.-) x y
-  function mul_f64 (x:f64) (y:f64) : f64 = F64.(.-) x y
+  function mul_f32 (x:f32) (y:f32) : f32 = F32.(.*) x y
+  function mul_f64 (x:f64) (y:f64) : f64 = F64.(.*) x y
 
   (* Division *)
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
index bd279cccc874f2274d8dfb05d4b76eb7d82e8dac..4249f034461a465c794b76fe03bd9cf26e1fa735 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
@@ -13,11 +13,11 @@
 Goal Post-condition (file tests/wp_plugin/float_real.i, line 14) in 'dequal':
 Assume {
   Type: is_sint32(dequal_0).
-  If lt_f64(add_f64(x, neg_f64(y)),
+  If lt_f64(sub_f64(x, y),
        to_f64((5902958103587057.0/590295810358705651712)))
   Then {
     If lt_f64(to_f64((-5902958103587057.0/590295810358705651712)),
-         add_f64(x, neg_f64(y)))
+         sub_f64(x, y))
     Then { (* Return *) Have: dequal_0 = 1. }
     Else { (* Return *) Have: dequal_0 = 0. }
   }