diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 7bd5aab9ec4f2bdfb0b374da1624a0f213ba931f..f2cea60613c7fb5ea45327a50a723365f7dd6ece 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -47,14 +47,29 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
   | _ ->
     raise Not_an_integer
 
+let ikind_of_interv i =
+  if Ival.is_bottom i then IInt
+  else match Ival.min_and_max i with
+    | Some l, Some u ->
+      let is_pos = Integer.ge l Integer.zero in
+      let lkind = Cil.intKindForValue l is_pos in
+      let ukind = Cil.intKindForValue u is_pos in
+      (* kind corresponding to the interval *)
+      let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+      (* convert the kind to [IInt] whenever smaller. *)
+      if Cil.intTypeIncluded kind IInt then IInt else kind
+    | None, None -> raise Cil.Not_representable (* GMP *)
+    | None, Some _ | Some _, None ->
+      Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+
+(* TODO: why is it useful? Crash if not here, but why? *)
 (* Return the interval over which ranges the smallest typ containing [i]. *)
 let interv_of_typ_containing_interv i =
   try
-    let itv_kind = Misc.itv_kind i in
-    (* convert the kind to [IInt] whenever smaller. *)
-    let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
+    let kind = ikind_of_interv i in
     interv_of_typ (TInt(kind, []))
   with Cil.Not_representable ->
+    (* infinity *)
     Ival.inject_range None None
 
 let interv_of_unknown_block =
@@ -235,7 +250,8 @@ let rec infer t =
                 try
                   let i = interv_of_typ_containing_interv (infer arg) in
                   Env.add lv i
-                with Not_an_integer -> ())
+                with Not_an_integer ->
+                  ())
               li.l_profile
               _args;
             let i =
@@ -341,10 +357,10 @@ and build_ieqs t ieqs ivars =
           try
             let i = interv_of_typ_containing_interv (infer arg) in
             Env.add lv i;
-            Ctype (TInt(Misc.itv_kind i, []))
+            Ctype (TInt(ikind_of_interv i, []))
           with
-            | Cil.Not_representable -> Linteger
-            | Not_an_integer -> lv.lv_type)
+          | Cil.Not_representable -> Linteger
+          | Not_an_integer -> lv.lv_type)
         li.l_profile
         args
       in
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index a900728f952e7997ee44081f23324380921f3f35..68313272fe2c2b80fa9b7b9307d6e06a0c9d2168 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -52,6 +52,11 @@
 
 exception Not_an_integer
 
+val ikind_of_interv: Ival.t -> Cil_types.ikind
+(** @return the smallest ikind that contains the given interval.
+    @raise Cil.Not_representable if the given interval does not fit into any C
+    integral type. *)
+
 val interv_of_typ: Cil_types.typ -> Ival.t
 (** @return the smallest interval which contains the given C type.
     @raise Not_an_integer if the given type is not an integral type. *)
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 1d3e09cc8cc4fddf75e4da600dc76f55fe860081..efd0c173f596797f335f37afd6e1d8d3194b5a1d 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -356,19 +356,6 @@ let is_recursive li =
     in
     has_recursive_call t
 
-let itv_kind i =
-  if Ival.is_bottom i then IInt
-  else match Ival.min_and_max i with
-    | Some l, Some u ->
-      let is_pos = Integer.ge l Integer.zero in
-      let lkind = Cil.intKindForValue l is_pos in
-      let ukind = Cil.intKindForValue u is_pos in
-      (* kind corresponding to the interval *)
-      if Cil.intTypeIncluded lkind ukind then ukind else lkind
-    | None, None -> raise Cil.Not_representable (* GMP *)
-    | None, Some _ | Some _, None ->
-      Kernel.fatal ~current:true "ival: %a" Ival.pretty i
-
 (*
 Local Variables:
 compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index e4806f0e157d1a1c4e5db1c9af243e191a3a346e..b8270952d613595417fd4c0fd5a4de5eb80bb132 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -132,9 +132,6 @@ val fundec_of_kf: kernel_function -> fundec
 val is_recursive: logic_info -> bool
 (** [is_recursive li] returns true iff [li] is defined recursively. *)
 
-val itv_kind: Ival.t -> ikind
-(** Return the smallest iking that contains the given interval. *)
-
 (*
 Local Variables:
 compile-command: "make"
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index f03b128958dff04d84e50e294a364481ae06107f..22799c4839d7ff32dc7dbd5ef5c419abdb78f3f6 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -198,15 +198,13 @@ let integer_ty_of_typ ty = ty_of_logic_ty (Ctype ty)
    interval. It is the \theta operator of the JFLA's paper. *)
 let ty_of_interv ?ctx i =
   try
-    let itv_kind = Misc.itv_kind i in
-    (* convert the kind to [IInt] whenever smaller. *)
-    let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
+    let kind = Interval.ikind_of_interv i in
     (* ctx type whenever possible to prevent superfluous casts in the generated
        code *)
     (match ctx with
      | None | Some (Gmp | Other) -> C_type kind
      | Some (C_type ik as ctx) ->
-       if Cil.intTypeIncluded itv_kind ik then ctx else C_type kind)
+       if Cil.intTypeIncluded kind ik then ctx else C_type kind)
   with Cil.Not_representable ->
     Gmp