diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index b333a7531daf6713aa4a7ecbbff7d1631fb22f1f..b3da1ce5c066f68ccc4f69d913f4d298f9cf5db8 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1579,7 +1579,12 @@ let check_observables auto =
  | Some set ->
    let is_relevant name =
      try
-       ignore (Globals.Functions.find_by_name name)
+       let kf = Globals.Functions.find_by_name name in
+       if not (Kernel_function.is_definition kf) then
+         Aorai_option.warning
+           "Function %a is observable by the automaton but is not defined \
+            in the C code. It will be ignored in the instrumentation"
+           Printer.pp_varname (Kernel_function.get_name kf)
      with Not_found ->
        Aorai_option.abort "Observable %s doesn't match any function" name
    in