diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 1f4c46afdf4cb8142337bcf4a011b6da92fcdc2e..5041723291b7ba862146e99dfadf6a62ee9ec26e 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -646,9 +646,22 @@ and is_matching_logic_var lv lv' env =
      | None ->
        (match Logic_var.find lv with
         | `Not_present -> false
-        | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''))
+        | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+        | exception Not_found ->
+          if lv.lv_name = "\\exit_status" && lv'.lv_name = "\\exit_status"
+          then begin Logic_var.add lv (`Same lv'); true end
+          else begin
+            match logic_var_correspondance lv env with
+            | None -> false
+            | Some lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+          end))
   | _ -> false
 
+and logic_var_correspondance lv env =
+  match find_candidate_logic_var lv env with
+  | None -> None
+  | Some lv' -> Logic_var.add lv (`Same lv'); Some lv'
+
 and is_same_term_offset lo lo' env =
   match lo, lo' with
   | TNoOffset, TNoOffset -> true
@@ -1212,6 +1225,16 @@ and logic_vars_env l l' env =
   else
     false, env
 
+and find_candidate_logic_var ?loc:_loc lv env =
+  let candidates = Logic_env.find_all_logic_functions lv.lv_name in
+  match List.find_opt (fun li -> li.l_profile = []) candidates with
+  | None -> Format.printf "No such var@."; None
+  | Some li ->
+    Format.printf "Found something@.";
+    if is_same_logic_var lv li.l_var_info env then
+      Some li.l_var_info
+    else None
+
 (* because of overloading, we have to check for a corresponding profile,
    leading to potentially recursive calls to is_same_* functions. *)
 and find_candidate_logic_info ?loc:_loc li env =
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
index 039e389d5e23a8896061fc28fbbd7ca7684c4784..4858468ec5f9cdf9344ab9dba021e730d4ad0548 100644
--- a/tests/syntax/ast_diff_1.i
+++ b/tests/syntax/ast_diff_1.i
@@ -45,6 +45,7 @@ int has_static_local(void) {
   return x;
 }
 
+/*@ exits \exit_status == 1; */
 int decl(void);
 
 int used_in_decl;
diff --git a/tests/syntax/ast_diff_2.i b/tests/syntax/ast_diff_2.i
index 3f9558f852fc84e0324b445b422301f7b1194b42..094bee8d12c9c449bf49dbad7d9e79c29fd1e9a3 100644
--- a/tests/syntax/ast_diff_2.i
+++ b/tests/syntax/ast_diff_2.i
@@ -46,6 +46,7 @@ int has_static_local(void) {
 
 int used_in_decl;
 
+/*@ exits \exit_status == 1; */
 int decl() {
   used_in_decl++;
   return used_in_decl;