diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 653c64c01e79984f1d2e50dc82d0450bc349106d..031337e2cc9c4a4a50fdd358df0a54e8bd7ae80a 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -423,6 +423,8 @@ let loop_contract_pids kf stmt =
   | _ -> []
 
 let compile Key.{ kf ; smoking ; bhv ; prop } =
+  let open Cil_const.CurrentLoc.Operators in
+  let* CurrentLocUpdated = Kernel_function.get_location kf in
   let body, checkpath, reachability =
     if Kernel_function.has_definition kf then
       let cfg = Cfg.get_automaton kf in
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index ed8d44bafa9b41e21793538de8f5b97740f07e7f..00b1c4c922c906f63bed228dee820efb283ca964 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -236,6 +236,8 @@ let f_name = f_memo (Pretty_utils.to_string pp_float)
 let char c = Integer.to_int64_exn (Cil.charConstToInt c)
 
 let constant e =
+  let open Cil_const.CurrentLoc.Operators in
+  let* CurrentLocUpdated = e.eloc in
   match (Cil.constFold true e).enode with
   | Const(CInt64(k,_,_)) ->
     begin