diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index b44b715ecd4f3ee957426eb5dddf4fb77e1191f7..b569d4c464ac42c22b60d2754012b19cedc00416 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -962,6 +962,8 @@ let filter_init_state restrict initial map acc =
   with Not_found -> acc
 
 let backward_analysis_aux stack kf ret_state =
+  let open Cil_const.CurrentLoc.Operators in
+  let* CurrentLocUpdated = Kernel_function.get_location kf in
   if Data_for_aorai.isIgnoredFunction kf then
     Aorai_option.fatal
       "Call backward analysis on ignored function %a" Kernel_function.pretty kf
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index ec532e726817a743ecc4be2a80e39ea3e94ebfbb..3d2eb83f556185e56f64e9b1f384528772864500 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -1,6 +1,6 @@
 [kernel] Parsing monostate.i (no preprocessing)
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] monostate.i:10: Warning: 
+[aorai] monostate.i:9: Warning: 
   Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
 [kernel] Parsing TMPDIR/aorai_monostate_0.i (no preprocessing)
 /* Generated by Frama-C */