diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 425fd3c893ec654c90be53ef8328c9f5bb651296..f7aaf9c113d6d86152842cb3d7ceac06de1a0e50 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6541,7 +6541,12 @@ and mkCastTGen ?(check=true) ?context ?(fromsource=false) ?(force=false)
   then
     begin
       Kernel.debug ~dkey "no cast to perform";
-      (oldt, e)
+      let returned_type =
+        match newt with
+        | TNamed _ -> newt
+        | _ -> oldt
+      in
+      (returned_type, e)
     end
   else
     let newt = if fromsource then newt else !typeForInsertedCast e oldt newt in
diff --git a/tests/rte/oracle/addsub_typedef.res.oracle b/tests/rte/oracle/addsub_typedef.res.oracle
index 3c40e7028ebc3850682949bc120e4907f6867404..84af60c46ab6b5efd668f1bb79d551e03d68f8f8 100644
--- a/tests/rte/oracle/addsub_typedef.res.oracle
+++ b/tests/rte/oracle/addsub_typedef.res.oracle
@@ -12,7 +12,7 @@
 [rte] addsub_typedef.c:13: Warning: 
   guaranteed RTE:
   assert
-  signed_overflow: -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
+  signed_overflow: -2147483648 ≤ (tint)(-((int)((int)(-0x7fffffff) - 1))) - 1;
 /* Generated by Frama-C */
 typedef int tint;
 int main(void)
@@ -30,7 +30,7 @@ int main(void)
   /*@ assert rte: signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1; */
   /*@ assert
       rte: signed_overflow:
-        -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
+        -2147483648 ≤ (tint)(-((int)((int)(-0x7fffffff) - 1))) - 1;
   */
   z = - (-0x7fffffff - 1) - 1;
   z = 0x7fffffff + 0;
@@ -38,7 +38,8 @@ int main(void)
   /*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
   /*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
   z = x + y;
-  /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-0x7ffffffc) - y; */
+  /*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-0x7ffffffc) - y;
+  */
   z = -0x7ffffffc - y;
   /*@ assert rte: signed_overflow: -2147483647 ≤ x; */
   /*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-x) - 0x7ffffffc;