diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index a1e2b5d26c42db639458ff127b2aa6aefe4ac4a9..e987bd4f6130a09335faf95ae8d34a7ae0a401d3 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -279,19 +279,30 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
 
 module Logic_binding = struct
 
+  let add_binding env logic_v vi =
+    try
+      let varinfos = Logic_var.Map.find logic_v env.var_mapping in
+      Stack.push vi varinfos;
+      env
+    with Not_found | Stack.Empty ->
+      let varinfos = Stack.create () in
+      Stack.push vi varinfos;
+      let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
+      { env with var_mapping = var_mapping }
+
   let add ?ty env logic_v =
     let ty = match ty with
       | Some ty -> ty
       | None -> match logic_v.lv_type with
-	| Ctype ty -> ty
-	| Linteger -> Gmpz.t ()
-	| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
-	| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
-	  let msg =
-	    Format.asprintf
-	      "logic variable of type %a" Logic_type.pretty lty
-	  in
-	  Error.not_yet msg
+        | Ctype ty -> ty
+        | Linteger -> Gmpz.t ()
+        | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
+        | Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
+          let msg =
+            Format.asprintf
+              "logic variable of type %a" Logic_type.pretty lty
+          in
+          Error.not_yet msg
     in
     let v, e, env = new_var
       ~loc:Location.unknown
@@ -301,29 +312,7 @@ module Logic_binding = struct
       ty
       (fun _ _ -> [])
     in
-    let env =
-      try
-        let varinfos = Logic_var.Map.find logic_v env.var_mapping in
-        Stack.push v varinfos;
-        env
-      with Not_found ->
-        let varinfos = Stack.create () in
-        Stack.push v varinfos;
-        let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
-        { env with var_mapping = var_mapping }
-    in
-    v, e, env
-
-  let add_existing_vi env lv vi =
-    try
-      let varinfos = Logic_var.Map.find lv env.var_mapping in
-      Stack.push vi varinfos;
-      env
-    with Not_found | Stack.Empty ->
-      let varinfos = Stack.create () in
-      Stack.push vi varinfos;
-      let var_mapping = Logic_var.Map.add lv varinfos env.var_mapping in
-      { env with var_mapping = var_mapping }
+    v, e, add_binding env logic_v v
 
   let get env logic_v =
     try
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index 1339e9357f34bfba1e66b0227af5ce7f30698b9b..abb50cb87e91c2115ee5637fec9ea0233799e123 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -68,8 +68,9 @@ module Logic_binding: sig
   val add: ?ty:typ -> t -> logic_var -> varinfo * exp * t
   (* Add a new C binding to the list of bindings for the logic variable. *)
 
-  val add_existing_vi: t -> logic_var -> varinfo -> t
-  (* [add_existing_vi env lv vi] defines [vi] as latest C binding for [lv]. *)
+  val add_binding: t -> logic_var -> varinfo -> t
+  (* [add_binding env lv vi] defines [vi] as the latest C binding for
+     [lv]. *)
 
   val get: t -> logic_var -> varinfo
   (* Return the latest C binding. *)
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index c5f9d07bf287f9558e6888e25e779d452228e3b2..11dbf3e154c34d6f32ded434ed983edfc93aa1f8 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -185,7 +185,7 @@ let add_varinfo_bindings ~loc kf env lfs =
         match Typing.ty_of_logic_ty lty with
         | Typing.C_type _ | Typing.Other ->
           (* Case A *)
-          Env.Logic_binding.add_existing_vi env lv vi_arg
+          Env.Logic_binding.add_binding env lv vi_arg
         | Typing.Gmp ->
           (* Case B *)
           let ty = Typing.typ_of_lty lv.lv_type in