diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 261c438947f7ae2a7db33086e00afa7d6209b9d3..4bf060e886e82db8a33f310900b4b111b7517737 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -550,8 +550,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
       let loc = best_loc ~loc e.eloc in
       let exp_type = Cil.typeOf e in
       let t = match kind with
-        | Signed_downcast | Unsigned_downcast
-          when Cil.isUnsignedInteger exp_type ->
+        | Signed_downcast | Unsigned_downcast ->
           let t = overflowed_expr_to_term ~loc e in
           (* Without this cast, the alarm is:
              - Signed_downcast: unsound ->
diff --git a/tests/rte/oracle/bts2314.res.oracle b/tests/rte/oracle/bts2314.res.oracle
index 7f03e2a42171b3dd99a99c20a96e10ecc7c8ab14..6ac02f4397c8dcaabd3024151ade9ac2c601a82a 100644
--- a/tests/rte/oracle/bts2314.res.oracle
+++ b/tests/rte/oracle/bts2314.res.oracle
@@ -12,8 +12,8 @@ void foo(int a, long b)
   s.num = (int)b;
   /*@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; */
   /*@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */
-  /*@ assert rte: signed_downcast: (int)s.num + a ≤ 63; */
-  /*@ assert rte: signed_downcast: -64 ≤ (int)s.num + a; */
+  /*@ assert rte: signed_downcast: (int)((int)s.num + a) ≤ 63; */
+  /*@ assert rte: signed_downcast: -64 ≤ (int)((int)s.num + a); */
   s.num = (int)((int)s.num + a);
   return;
 }
diff --git a/tests/rte/oracle/divmod.res.oracle b/tests/rte/oracle/divmod.res.oracle
index 19f1dcc24f0cd8d781244ea56176325ef02d54db..01fa69c0ee7564e13b0b4c72dd7c9440e3b6ccc7 100644
--- a/tests/rte/oracle/divmod.res.oracle
+++ b/tests/rte/oracle/divmod.res.oracle
@@ -20,7 +20,8 @@
   guaranteed RTE:
   assert
   signed_downcast:
-    (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+    (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+    2147483647;
 /* Generated by Frama-C */
 int main(void)
 {
@@ -70,7 +71,8 @@ int main(void)
   z = (-0x7ffffff - 1) / y;
   /*@ assert
       rte: signed_downcast:
-        (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+        (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+        2147483647;
   */
   z = (int)(-2147483648L / (long long)(-1L));
   z = (int)(0x80000000 / (unsigned int)(-1));
diff --git a/tests/rte/oracle/divmod_typedef.res.oracle b/tests/rte/oracle/divmod_typedef.res.oracle
index 17b553cb32d0c333a7e7195e5836d96d2355f90b..51b06e5796e1d2d9b536684513fdde9e05346750 100644
--- a/tests/rte/oracle/divmod_typedef.res.oracle
+++ b/tests/rte/oracle/divmod_typedef.res.oracle
@@ -20,7 +20,8 @@
   guaranteed RTE:
   assert
   signed_downcast:
-    (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+    (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+    2147483647;
 /* Generated by Frama-C */
 typedef int tint;
 typedef unsigned int tuint;
@@ -72,7 +73,8 @@ int main(void)
   z = (-0x7ffffff - 1) / y;
   /*@ assert
       rte: signed_downcast:
-        (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+        (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+        2147483647;
   */
   z = (int)(-2147483648L / (long long)(-1L));
   z = (int)(0x80000000 / (unsigned int)(-1));
diff --git a/tests/rte/oracle/downcast.0.res.oracle b/tests/rte/oracle/downcast.0.res.oracle
index 5963c8e9adf1d2b2f27d203e4b7974506da6c5e7..3097cab2fa8fbbf5cfd2ff45cf85dbdf95533a80 100644
--- a/tests/rte/oracle/downcast.0.res.oracle
+++ b/tests/rte/oracle/downcast.0.res.oracle
@@ -15,8 +15,8 @@ int main(void)
   unsigned short s;
   /*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
   /*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
-  /*@ assert rte: signed_downcast: (int)sx + (int)sy ≤ 127; */
-  /*@ assert rte: signed_downcast: -128 ≤ (int)sx + (int)sy; */
+  /*@ assert rte: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
+  /*@ assert rte: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
   sz = (signed char)((int)sx + (int)sy);
   /*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
   /*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
diff --git a/tests/rte/oracle/downcast.2.res.oracle b/tests/rte/oracle/downcast.2.res.oracle
index dd0102f2be08fce8cf04b6bae750fe7eb3c87cc7..8413d87dbce590d468e78725da53c7db6ed7e496 100644
--- a/tests/rte/oracle/downcast.2.res.oracle
+++ b/tests/rte/oracle/downcast.2.res.oracle
@@ -15,13 +15,13 @@ int main(void)
   unsigned short s;
   /*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
   /*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
-  /*@ assert rte: signed_downcast: (int)sx + (int)sy ≤ 127; */
-  /*@ assert rte: signed_downcast: -128 ≤ (int)sx + (int)sy; */
+  /*@ assert rte: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
+  /*@ assert rte: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
   sz = (signed char)((int)sx + (int)sy);
   /*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
   /*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
-  /*@ assert rte: unsigned_downcast: (int)sx + (int)sy ≤ 255; */
-  /*@ assert rte: unsigned_downcast: 0 ≤ (int)sx + (int)sy; */
+  /*@ assert rte: unsigned_downcast: (int)((int)sx + (int)sy) ≤ 255; */
+  /*@ assert rte: unsigned_downcast: 0 ≤ (int)((int)sx + (int)sy); */
   uc = (unsigned char)((int)sx + (int)sy);
   /*@ assert rte: unsigned_downcast: x ≤ 255; */
   /*@ assert rte: unsigned_downcast: 0 ≤ x; */
diff --git a/tests/rte/oracle/minus.0.res.oracle b/tests/rte/oracle/minus.0.res.oracle
index ea9f8124d527f4ea181094c622f5cee80f7cb128..19845be6ff9a94db7e3c6f1f4002cb948fa01932 100644
--- a/tests/rte/oracle/minus.0.res.oracle
+++ b/tests/rte/oracle/minus.0.res.oracle
@@ -36,11 +36,11 @@ int main(void)
   */
   /*@ assert
       rte: signed_downcast:
-        (int)((unsigned short)((int)(65535 + 3))) + x ≤ 32767;
+        (int)((int)((unsigned short)((int)(65535 + 3))) + x) ≤ 32767;
   */
   /*@ assert
       rte: signed_downcast:
-        -32768 ≤ (int)((unsigned short)((int)(65535 + 3))) + x;
+        -32768 ≤ (int)((int)((unsigned short)((int)(65535 + 3))) + x);
   */
   sz = (short)((int)((unsigned short)(65535 + 3)) + x);
   z = (int)(-0x80000000 - (unsigned int)1);
diff --git a/tests/rte/oracle/minus.1.res.oracle b/tests/rte/oracle/minus.1.res.oracle
index 8e295b1e3cf2aa1bbc7375da339f4b0a5c76b37f..9b6eb5d89be970a07ad71b9ed1aa03e45a1260c0 100644
--- a/tests/rte/oracle/minus.1.res.oracle
+++ b/tests/rte/oracle/minus.1.res.oracle
@@ -34,11 +34,11 @@ int main(void)
   */
   /*@ assert
       rte: signed_downcast:
-        (int)((unsigned short)((int)(65535 + 3))) + x ≤ 32767;
+        (int)((int)((unsigned short)((int)(65535 + 3))) + x) ≤ 32767;
   */
   /*@ assert
       rte: signed_downcast:
-        -32768 ≤ (int)((unsigned short)((int)(65535 + 3))) + x;
+        -32768 ≤ (int)((int)((unsigned short)((int)(65535 + 3))) + x);
   */
   sz = (short)((int)((unsigned short)(65535 + 3)) + x);
   /*@ assert
diff --git a/tests/rte_manual/oracle/signed_downcast.1.res.oracle b/tests/rte_manual/oracle/signed_downcast.1.res.oracle
index b53eac56ff97f956af17d3bac2eba60a09f75be7..508313da76c47284195fea82c66152577cad4f2c 100644
--- a/tests/rte_manual/oracle/signed_downcast.1.res.oracle
+++ b/tests/rte_manual/oracle/signed_downcast.1.res.oracle
@@ -9,8 +9,8 @@ int main(void)
   signed char cz;
   /*@ assert rte: signed_overflow: -2147483648 ≤ (int)cx + (int)cy; */
   /*@ assert rte: signed_overflow: (int)cx + (int)cy ≤ 2147483647; */
-  /*@ assert rte: signed_downcast: (int)cx + (int)cy ≤ 127; */
-  /*@ assert rte: signed_downcast: -128 ≤ (int)cx + (int)cy; */
+  /*@ assert rte: signed_downcast: (int)((int)cx + (int)cy) ≤ 127; */
+  /*@ assert rte: signed_downcast: -128 ≤ (int)((int)cx + (int)cy); */
   cz = (signed char)((int)cx + (int)cy);
   __retres = 0;
   return __retres;
diff --git a/tests/rte_manual/oracle/unsigned_downcast.res.oracle b/tests/rte_manual/oracle/unsigned_downcast.res.oracle
index 01400f1cd7410007739154ceded5ccfe7c3ac671..30bacde2ada88700dfcb48c5e4beeedda729f814 100644
--- a/tests/rte_manual/oracle/unsigned_downcast.res.oracle
+++ b/tests/rte_manual/oracle/unsigned_downcast.res.oracle
@@ -6,8 +6,8 @@ unsigned char f(int a, int b)
   unsigned char __retres;
   /*@ assert rte: signed_overflow: -2147483648 ≤ a + b; */
   /*@ assert rte: signed_overflow: a + b ≤ 2147483647; */
-  /*@ assert rte: unsigned_downcast: a + b ≤ 255; */
-  /*@ assert rte: unsigned_downcast: 0 ≤ a + b; */
+  /*@ assert rte: unsigned_downcast: (int)(a + b) ≤ 255; */
+  /*@ assert rte: unsigned_downcast: 0 ≤ (int)(a + b); */
   __retres = (unsigned char)(a + b);
   return __retres;
 }
diff --git a/tests/value/oracle/downcast.res.oracle b/tests/value/oracle/downcast.res.oracle
index 7df2a56ff7b744242508b6342252dd42019d2a48..18b563a5f18a5c227a7f0f3e1f69a537e4b39aad 100644
--- a/tests/value/oracle/downcast.res.oracle
+++ b/tests/value/oracle/downcast.res.oracle
@@ -16,9 +16,9 @@
 [eva] computing for function main1 <- main.
   Called from tests/value/downcast.i:152.
 [eva:alarm] tests/value/downcast.i:19: Warning: 
-  signed downcast. assert -128 ≤ (int)sx + (int)sy;
+  signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
 [eva:alarm] tests/value/downcast.i:19: Warning: 
-  signed downcast. assert (int)sx + (int)sy ≤ 127;
+  signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
 [eva:alarm] tests/value/downcast.i:22: Warning: 
   signed downcast. assert (unsigned int)(uy + uz) ≤ 2147483647;
 [eva] Recording results for main1
@@ -440,8 +440,8 @@ unsigned short s;
 int volatile v;
 void main1(void)
 {
-  /*@ assert Eva: signed_downcast: -128 ≤ (int)sx + (int)sy; */
-  /*@ assert Eva: signed_downcast: (int)sx + (int)sy ≤ 127; */
+  /*@ assert Eva: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
+  /*@ assert Eva: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
   sz = (signed char)((int)sx + (int)sy);
   uc = (unsigned char)((int)sx + (int)sy);
   uc = (unsigned char)x;
@@ -642,7 +642,7 @@ void main(void)
 [eva] computing for function main1 <- main.
   Called from tests/value/downcast.i:152.
 [eva:alarm] tests/value/downcast.i:20: Warning: 
-  unsigned downcast. assert 0 ≤ (int)sx + (int)sy;
+  unsigned downcast. assert 0 ≤ (int)((int)sx + (int)sy);
 [eva:alarm] tests/value/downcast.i:21: Warning: 
   unsigned downcast. assert 0 ≤ x;
 [eva:alarm] tests/value/downcast.i:21: Warning: 
@@ -688,9 +688,9 @@ void main(void)
 [eva] computing for function main6_val_warn_converted_signed <- main.
   Called from tests/value/downcast.i:157.
 [eva:alarm] tests/value/downcast.i:81: Warning: 
-  unsigned downcast. assert 0 ≤ -12;
+  unsigned downcast. assert 0 ≤ (int)(-12);
 [eva:alarm] tests/value/downcast.i:86: Warning: 
-  unsigned downcast. assert 0 ≤ -64000;
+  unsigned downcast. assert 0 ≤ (int)(-64000);
 [eva] tests/value/downcast.i:92: 
   Assigning imprecise value to y.
   The imprecision originates from Arithmetic {tests/value/downcast.i:92}
@@ -997,7 +997,7 @@ int volatile v;
 void main1(void)
 {
   sz = (signed char)((int)sx + (int)sy);
-  /*@ assert Eva: unsigned_downcast: 0 ≤ (int)sx + (int)sy; */
+  /*@ assert Eva: unsigned_downcast: 0 ≤ (int)((int)sx + (int)sy); */
   uc = (unsigned char)((int)sx + (int)sy);
   /*@ assert Eva: unsigned_downcast: 0 ≤ x; */
   /*@ assert Eva: unsigned_downcast: x ≤ 255; */
@@ -1081,12 +1081,12 @@ void main6_val_warn_converted_signed(void)
     short b = (short)e;
   }
   if (v) {
-    /*@ assert Eva: unsigned_downcast: 0 ≤ -12; */
+    /*@ assert Eva: unsigned_downcast: 0 ≤ (int)(-12); */
     unsigned long e_0 = (unsigned long)(-12);
     short b_0 = (short)e_0;
   }
   if (v) {
-    /*@ assert Eva: unsigned_downcast: 0 ≤ -64000; */
+    /*@ assert Eva: unsigned_downcast: 0 ≤ (int)(-64000); */
     unsigned int e_1 = (unsigned int)(-64000);
     short b_1 = (short)e_1;
   }
@@ -1191,9 +1191,9 @@ void main(void)
 [eva] computing for function main1 <- main.
   Called from tests/value/downcast.i:152.
 [eva:alarm] tests/value/downcast.i:19: Warning: 
-  signed downcast. assert -128 ≤ (int)sx + (int)sy;
+  signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
 [eva:alarm] tests/value/downcast.i:19: Warning: 
-  signed downcast. assert (int)sx + (int)sy ≤ 127;
+  signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2_bitfield <- main.
@@ -1556,8 +1556,8 @@ unsigned short s;
 int volatile v;
 void main1(void)
 {
-  /*@ assert Eva: signed_downcast: -128 ≤ (int)sx + (int)sy; */
-  /*@ assert Eva: signed_downcast: (int)sx + (int)sy ≤ 127; */
+  /*@ assert Eva: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
+  /*@ assert Eva: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
   sz = (signed char)((int)sx + (int)sy);
   uc = (unsigned char)((int)sx + (int)sy);
   uc = (unsigned char)x;