diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 976d4f69902446793d8abf72bb75bdb15cd283fb..a16e6432ea86c592c83361d76c04d7287372b6bb 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -96,12 +96,14 @@ let logicCType t =
   in plain_or_set logicCType t
 
 let plain_array_to_ptr ty =
+  let open Cil_const.CurrentLoc.Operators in
   match unroll_type ty with
   | Ctype(TArray(ty,lo,attr) as tarr) ->
     let length_attr =
       match lo with
       | None -> []
-      | Some _ ->
+      | Some e ->
+        let* CurrentLocUpdated = e.eloc in
         try
           let len = Cil.bitsSizeOf tarr in
           let len = try len / (Cil.bitsSizeOf ty)