diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index fa4dbd4f4abde2c118f0def338e392cc02cc23f8..abb6cec90b200cbd2d0c8b71e1f877170720334a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2017/02/24] Fix crash with casts from non-integral terms to
+	        integral types (bts #2284).
 -* E-ACSL       [2017/02/17] Fix bug with goto which points to a labeled
 	        statement which must be instrumented.
 -* E-ACSL       [2017/01/23] Fix bug #2252 about pointer arithmetic with
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 829106397f773ed2b81524f951218ee91d7ea460..298cc1bdb3d2a75bee21cfe06d025f9ae8b04687 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -135,9 +135,22 @@ let rec infer t =
     Ival.bitwise_or i1 i2
   | TCastE (ty, t)
   | TCoerce (t, ty) ->
-    let it = infer t in
-    let ity = interv_of_typ ty in
-    Ival.meet it ity
+    (try
+       let it = infer t in
+       let ity = interv_of_typ ty in
+       Ival.meet it ity
+     with Not_an_integer ->
+       if Cil.isIntegralType ty then begin
+         (* heterogeneous cast from a non-integral term to an integral type:
+            consider that one eventually gets an integral type even if it is
+            not sure. *)
+         Options.warning
+           ~once:true "possibly unsafe cast from term '%a' to typ '%a'."
+           Printer.pp_term t
+           Printer.pp_typ ty;
+         interv_of_typ ty
+       end else
+         raise Not_an_integer)
   | Tif (_, t2, t3) ->
     let i2 = infer t2 in
     let i3 = infer t3 in
diff --git a/src/plugins/e-acsl/tests/gmp/cast.i b/src/plugins/e-acsl/tests/gmp/cast.i
index 3b35db1ab3324f806042d4eb11d4a1f9b14fe5f5..700d338841e3c8b337bbf333ed40279312eb8e21 100644
--- a/src/plugins/e-acsl/tests/gmp/cast.i
+++ b/src/plugins/e-acsl/tests/gmp/cast.i
@@ -12,11 +12,15 @@ int main(void) {
 
   /*@ assert y == (int)0; */ ; // cast from integer to int
   /*@ assert (unsigned int) y == (unsigned int)0; */ ; /* cast from integer
-  						          to unsigned int */
+                                                          to unsigned int */
 
   /*@ assert y != (int)0xfffffffffffffff; */ ; // cast from integer to int
   /*@ assert (unsigned int) y != (unsigned int)0xfffffffffffffff; */ ;
   /* cast from integer to unsigned int */
 
+  /* heterogeneous casts from/to integers */
+  int t[2] = { 0, 1 };
+  /*@ assert (float)x == t[(int)0.1]; */
+
   return 0;
 }
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
index 62cf4517ec4161f8f7b5400e1fdcb065a5222ca7..f284e44a2a360b394a3b40bc140cdf3f1f9ecf11 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
@@ -1,5 +1,7 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] warning: possibly unsafe cast from term '0.1' to typ 'int'.
+tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -15,4 +17,5 @@ FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns cl
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_assert
+[value] user error: type long double not implemented. Using double instead
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index 422f1d17fe82242788a3c32ec696e7c02a7cd77e..62bf6c7c53e7796a9defeaa4a99ba6f61080667d 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -1,5 +1,7 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] warning: possibly unsafe cast from term '0.1' to typ 'int'.
+tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -22,4 +24,7 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: preco
 [value] using specification for function __gmpz_clear
 [value] using specification for function __gmpz_get_ui
 [value] using specification for function __gmpz_init_set_ui
+[value] user error: type long double not implemented. Using double instead
+tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9;
+tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert __gen_e_acsl_cast_9 < 2;
 [value] done for function main