diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 449c92e448b927a00a536862a0c52d787750a068..473ce5547af126a357533a79d850e3fe18e452d3 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -395,6 +395,8 @@ module LF_env
 
   let find li profile = LFProf.Hashtbl.find tbl (li,profile)
 
+  let add li profile ival = LFProf.Hashtbl.add tbl (li,profile) ival
+
   exception Recursive
 
   let contain li = object
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 19a8ffa8033e803a01490d093a71cadf77b0fc15..008856976aa48dc11e4b8ac6c5459ca3c8e5870d 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -97,6 +97,8 @@ module LF_env : sig
 
   val clear : unit -> unit
 
+  val add : logic_info -> Profile.t -> ival -> unit
+
   val is_rec : logic_info -> bool
 
   val replace : logic_info -> Profile.t -> ival -> unit
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 1ec511d4c67a22cf49f0119a1137eb6498c09488..e66801dce797d4c965efb5ee438f851b97aea65d 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -21,7 +21,6 @@
 (**************************************************************************)
 
 open Cil_types
-open Cil_datatype
 open Analyses_types
 open Analyses_datatype
 
@@ -35,7 +34,6 @@ module Error = Error.Make(struct let phase = dkey end)
 (* Basic datatypes and operations *)
 (* ********************************************************************* *)
 
-
 let is_included i1 i2 = match i1, i2 with
   | Ival i1, Ival i2 -> Ival.is_included i1 i2
   | Float(k1, f1), Float(k2, f2) ->
@@ -357,15 +355,22 @@ let rec fixpoint ~(infer : force:bool ->
                    term ->
                    ival Error.result)
     li args_ival t' ival =
-  LF_env.replace li args_ival ival;
   let get_res = Error.map (fun x -> x) in
   let logic_env = Logic_env.make args_ival in
-  let inferred_ival = get_res (infer ~force:true ~logic_env t') in
-  if is_included inferred_ival ival
-  then
+  match li.l_type with
+  | Some (Ctype typ) ->
+    let ival = interv_of_typ typ in
+    LF_env.add li args_ival ival;
+    ignore (infer ~force:true ~logic_env t');
     ival
-  else
-    fixpoint ~infer li args_ival t' inferred_ival
+  | _ ->
+    LF_env.replace li args_ival ival;
+    let inferred_ival = get_res (infer ~force:true ~logic_env t') in
+    if is_included inferred_ival ival
+    then
+      ival
+    else
+      fixpoint ~infer li args_ival t' inferred_ival
 
 
 (* Memoization module which retrieves the computed info of some terms *)
@@ -739,7 +744,11 @@ let rec infer ~force ~logic_env t =
                fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
           | LBterm t' ->
             let logic_env = Logic_env.make profile in
-            get_res (infer ~force ~logic_env t')
+            (match li.l_type with
+             | Some (Ctype (typ)) ->
+               ignore ((infer ~force ~logic_env t'));
+               interv_of_typ typ;
+             | _ -> get_res (infer ~force ~logic_env t'))
           | _ -> assert false)
        | LBnone when li.l_var_info.lv_name = "\\sum" ||
                      li.l_var_info.lv_name = "\\product" ->
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 954ca8c4c84b69463dcf5be8bfd6e5a7aeafecc0..73b3208852b166bfa749ac1cfffe76881082fc07 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -359,9 +359,13 @@ let rec type_term
       let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
       dup ty
 
+    | TLval ((TVar {lv_type = Ctype (TInt (ik, _))}, _) as tlv) ->
+      type_term_lval ~profile tlv;
+      dup (C_integer ik)
+
     | TLval tlv ->
       let i = Interval.get_from_profile ~profile t in
-      let ty =  ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
+      let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
       type_term_lval ~profile tlv;
       (* Options.feedback "Type : %a" D.pretty ty; *)
       dup ty
@@ -585,10 +589,14 @@ let rec type_term
                     ~profile:new_profile
                     t_body))
             pending_typing;
-          dup (ty_of_interv
-                 ?ctx:ctx_body
-                 ~use_gmp_opt:(gmp && use_gmp_opt)
-                 (Interval.get_from_profile ~profile t))
+          (match li.l_type with
+           | Some (Ctype (TInt (ikind, _))) ->
+             dup (C_integer ikind)
+           | _ ->
+             dup (ty_of_interv
+                    ?ctx:ctx_body
+                    ~use_gmp_opt:(gmp && use_gmp_opt)
+                    (Interval.get_from_profile ~profile t)))
         | LBnone ->
           (match args with
            | [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ] ->