diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 92b4d3ab5e75686733875057db959303dcc38b51..520ec3756d93e759b93cdee9d5031cfc6d60b376 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1710,10 +1710,10 @@ struct
     in
     let rec aux lty1 lty2 =
       match (unroll_type lty1), (unroll_type lty2) with
-      | t1, t2 when is_same_type t1 t2 -> t1
       | Ctype ty1, Ctype ty2 ->
         if isIntegralType ty1 && isIntegralType ty2 then
-          if (isSignedInteger ty1) <> (isSignedInteger ty2) then
+          if is_same_type lty1 lty2 then lty1
+          else if (isSignedInteger ty1) <> (isSignedInteger ty2) then
             (* in ACSL, the comparison between 0xFFFFFFFF seen as int and
                unsigned int is not true: we really have to operate at
                the integer level.
@@ -1760,6 +1760,7 @@ struct
       (* implicit conversion to set *)
       | Ltype ({lt_name = "set"} as lt,[t1]), t2
       | t1, Ltype({lt_name="set"} as lt,[t2]) -> Ltype(lt,[aux t1 t2])
+      | t1, t2 when is_same_type t1 t2 -> t1
       | _ ->
         C.error loc "types %a and %a are not convertible"
           Cil_printer.pp_logic_type lty1 Cil_printer.pp_logic_type lty2
diff --git a/tests/spec/float-acsl.i b/tests/spec/float-acsl.i
index 3e33afc86d04a3296bb6b760d4d59b1f141bd06b..571ae93e6660c86640c21825e2b737cc359e476e 100644
--- a/tests/spec/float-acsl.i
+++ b/tests/spec/float-acsl.i
@@ -1,3 +1,7 @@
+/* run.config*
+STDOPT: +"-kernel-msg-key printer:logic-coercions"
+*/
+
 /*@
   assigns \result \from \nothing;
   ensures \le_double(\result, (double)0.0);
@@ -21,6 +25,12 @@ double minus_one(void);
 */
 float minus_onef(void);
 
+/*@ requires x <= y;
+    assigns \result \from x,y;
+    ensures x <= \result <= y;
+*/
+float test(float x, float y);
+
 void main() {
   double mone = minus_one();
   float monef = minus_onef();
diff --git a/tests/spec/oracle/float-acsl.res.oracle b/tests/spec/oracle/float-acsl.res.oracle
index 5489ef5e7841f791f2fffeaa10f5492b5339e044..3aa9fe9e8fb11812f371cda4896911b40fad3dce 100644
--- a/tests/spec/oracle/float-acsl.res.oracle
+++ b/tests/spec/oracle/float-acsl.res.oracle
@@ -22,6 +22,17 @@ double minus_one(void);
  */
 float minus_onef(void);
 
+/*@ requires
+      /* (coercion to:ℝ */x/* ) */ ≤ /* (coercion to:ℝ */y/* ) */;
+    ensures
+      /* (coercion to:ℝ */\old(x)/* ) */ ≤
+      /* (coercion to:ℝ */\result/* ) */ ≤
+      /* (coercion to:ℝ */\old(y)/* ) */;
+    assigns \result;
+    assigns \result \from x, y;
+ */
+float test(float x, float y);
+
 void main(void)
 {
   double mone = minus_one();