diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 11fa533ea141df075193d94c712f4d559d372822..0b919947228d1d074eb8f8152c0ab41b18c53d45 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -230,7 +230,8 @@ let mk_cast ?(loc=Cil_datatype.Location.unknown) ?(force=false) newt t =
     let typ = Cil.type_remove_attributes_for_logic_type newt
     in term ~loc (TCastE (typ, t)) (Ctype typ)
   in
-  let rec aux1 = function
+  let rec aux1 typ t =
+    match typ with
     | Ctype oldt ->
       if not (need_logic_cast oldt newt) && not force then t
       else begin
@@ -246,15 +247,21 @@ let mk_cast ?(loc=Cil_datatype.Location.unknown) ?(force=false) newt t =
                | _, TConst (Integer (i,_)) when Integer.is_zero i -> mk_cast t'
                | _ -> mk_cast t
               )
-            | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef -> aux2 (unroll_ltdef ty)
+            | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
+              aux2 (unroll_ltdef ty)
             | _ -> mk_cast t
           in aux2 t'.term_type
         | _ -> (* Do not remove old cast because they are conversions !!! *)
           mk_cast t
       end
-    | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef -> aux1 (unroll_ltdef ty)
+    | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
+      aux1 (unroll_ltdef ty) t
+    | Linteger | Lreal ->
+      (match t.term_node with
+       | TLogic_coerce (_,t') -> aux1 t'.term_type t'
+       | _ -> mk_cast t)
     | _ -> mk_cast t
-  in aux1 t.term_type
+  in aux1 t.term_type t
 
 let real_of_float s f =
   { r_literal = s ; r_nearest = f ; r_upper = f ; r_lower = f }
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index 70f83babb9c5c873079de8541d15687f36b4df0f..17478ac46f188ed3bd618d92ccdab4ea2d51c863 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -15,10 +15,11 @@ let check_expr_term check fct s e =
       | _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond e
   in
   let term' = Logic_utils.expr_to_term ~cast:false exp in
+  let term' = Logic_utils.mk_cast Cil.intType term' in
   if check && not (Cil_datatype.Term.equal term term') then
     Kernel.fatal
-      "translation of C expression %a inconsistent with logic term %a"
-      Printer.pp_exp exp Printer.pp_term term;
+      "translation of C expression %a is %a, inconsistent with logic term %a"
+      Printer.pp_exp exp Printer.pp_term term' Printer.pp_term term;
   let p = List.hd (Logic_env.find_all_logic_functions "int_eq") in
   let app = Logic_const.papp (p,[],[term;term']) in
   let post = Logic_const.new_predicate app in
diff --git a/tests/spec/oracle/expr_to_term.res.oracle b/tests/spec/oracle/expr_to_term.res.oracle
index ed2717ba97a03b3e45decf484c8d857f0519c5b6..a378207a1b9cec63fef9d84d30052cc663076a14 100644
--- a/tests/spec/oracle/expr_to_term.res.oracle
+++ b/tests/spec/oracle/expr_to_term.res.oracle
@@ -40,4 +40,21 @@ int main(void)
   return __retres;
 }
 
+/*@ ensures int_eq((int)(!(t ≢ 0)), (int)(!(t ≢ 0)));
+    ensures int_eq((int)(!(t ≢ 0)), (int)5);
+ */
+int g(void)
+{
+  int __retres;
+  if (! t) {
+    __retres = 2;
+    goto return_label;
+  }
+  else {
+    __retres = 3;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+