diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index c95a783a03086d3a0f976595c0a8ac8bee1c26d4..b19f7e478bd77f9e680841b0e5403008695b9a50 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -812,6 +812,9 @@ type_spec:
 | SHORT          { LTint IShort }      /** [short] */
 | SIGNED SHORT   { LTint IShort }      /** [short] */
 | UNSIGNED SHORT { LTint IUShort }     /** [unsigned short] */
+| SHORT INT          { LTint IShort }      /** [short] */
+| SIGNED SHORT INT   { LTint IShort }      /** [short] */
+| UNSIGNED SHORT INT { LTint IUShort }     /** [unsigned short] */
 | LONG           { LTint ILong }       /** [long] */
 | SIGNED LONG    { LTint ILong }       /** [long] */
 | UNSIGNED LONG  { LTint IULong }      /** [unsigned long] */
diff --git a/tests/spec/cast_int.i b/tests/spec/cast_int.i
new file mode 100644
index 0000000000000000000000000000000000000000..21505c3ff130cd49409a775ca65eb8f328c7dac5
--- /dev/null
+++ b/tests/spec/cast_int.i
@@ -0,0 +1,6 @@
+unsigned short int toto;
+
+/*@ensures toto==(unsigned short int)param;*/
+int F(int param){
+return 0;
+}
diff --git a/tests/spec/oracle/cast_int.res.oracle b/tests/spec/oracle/cast_int.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..23501c9b3c51cb9516283692958b24e02dc3f771
--- /dev/null
+++ b/tests/spec/oracle/cast_int.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/spec/cast_int.i (no preprocessing)
+/* Generated by Frama-C */
+unsigned short toto;
+/*@ ensures toto ≡ (unsigned short)\old(param); */
+int F(int param)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+