diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index eaf5abc2297410e305c16be6538c1f193b4bf1cf..ff6fc08f5e8d05749968825aaf6463db4c5df880 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -395,13 +395,13 @@ module Logic_env
     let new_lq_bind =
       try Logic_var.Map.update x update env.let_quantif_bind
       with Not_found ->
-        match Logic_var.Map.find_opt x env.profile with
-        | Some i ->
-          (* The profile must remain unchanged, so if the variable is bound in
-             the profile, we add the refined interval in the other bindings,
-             which are checked first when finding the interval *)
-          Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
-        | None -> Options.abort "updating a variable not in environment"
+      match Logic_var.Map.find_opt x env.profile with
+      | Some i ->
+        (* The profile must remain unchanged, so if the variable is bound in
+           the profile, we add the refined interval in the other bindings,
+           which are checked first when finding the interval *)
+        Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
+      | None -> Options.abort "updating a variable not in environment"
     in
     {env with let_quantif_bind = new_lq_bind}
 
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 9aa1e9e288ff7a49a95530c89572803cd14850b2..9cafe69c93a70301e49ffe2d73ccf84a3d6120c4 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -93,11 +93,11 @@ module Logic_env : sig
   val find : t -> logic_var -> ival
 
   (** get the profile of the logic environment, i.e. bindings through function
-     arguments *)
+      arguments *)
   val get_profile : t -> Profile.t
 
-  (** refine the interval of a logic variable : replace an interval with a
-  more precise one *)
+  (** refine the interval of a logic variable: replace an interval with a more
+      precise one *)
   val refine : t -> logic_var -> ival -> t
 end
 
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index c4810803071a558384eafc8b4f4bb2ab3ffc3b41..833d84ed21d5755e1b3763d8da9ac37b62d9d232 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -903,6 +903,10 @@ and compute_logic_env_if_branches logic_env t =
   in
   let add_eq logic_env x v = Logic_env.refine logic_env x (get_res (ival v)) in
   let t_branch, f_branch =
+    (* we do not discriminate between strict and weak inequalities. This is
+       slighlty less precise but allow for better reusing of the code in the
+       case of recursive functions, the main advantage in typing
+       conditionals is for recursive functions. *)
     match t.term_node with
     | TBinOp(op, {term_node = TLval(TVar x, TNoOffset)}, v) ->
       begin