diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index d0e5544f07..751ade6880 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -67,6 +67,9 @@ jobs:
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
+      - name: Test incremental cram
+        run: opam exec -- dune runtest tests/incremental
+
       - name: Test unit
         run: opam exec -- dune runtest unittest
 
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 5455bb0cb7..2bec6b72fb 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -94,6 +94,9 @@ jobs:
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
+      - name: Test incremental cram
+        run: opam exec -- dune runtest tests/incremental
+
       - name: Test unit
         run: opam exec -- dune runtest unittest
 
@@ -179,6 +182,9 @@ jobs:
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 
+      - name: Test incremental cram
+        run: opam exec -- dune runtest tests/incremental
+
       - name: Test unit
         run: opam exec -- dune runtest unittest
 
diff --git a/src/autoTune.ml b/src/autoTune.ml
index 79d85d8009..8adf18b103 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -202,7 +202,7 @@ let activateLongjmpAnalysesWhenRequired () =
   let isLongjmp = function
     | LibraryDesc.Longjmp _ -> true
     | _ -> false
-in
+  in
   if hasFunction isLongjmp  then (
     print_endline @@ "longjmp -> enabling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\"";
     enableAnalyses longjmpAnalyses;
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 36627f360a..ff81ff6752 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -912,7 +912,7 @@ struct
       | Some {changes; _} -> changes
       | None -> empty_change_info ()
     in
-    List.(Printf.printf "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed));
+    List.(Printf.printf "change_info = { unchanged = %d; changed = %d (with unchangedHeader = %d); added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (BatList.count_matching (fun c -> c.unchangedHeader) c.changed) (length c.added) (length c.removed));
 
     let changed_funs = List.filter_map (function
         | {old = {def = Some (Fun f); _}; diff = None; _} ->
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index ce71b43392..269e90a4d7 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -3,34 +3,69 @@ open CilMaps
 
 module StringMap = Map.Make(String)
 
-type method_rename_assumption = {original_method_name: string; new_method_name: string; parameter_renames: string StringMap.t}
-type method_rename_assumptions = method_rename_assumption VarinfoMap.t
+(* Mapping with rename assumptions about functions collected during the comparison. An assumption means that the
+   comparison result so far is only correct, if the varinfos of a key-value pair in the mapping represent the same but
+   renamed function. It is a mapping from a varinfo in the old version to one in the new version. *)
+type method_rename_assumptions = varinfo VarinfoMap.t
 
-(*rename_mapping is carried through the stack when comparing the AST. Holds a list of rename assumptions.*)
-type rename_mapping = (string StringMap.t) * (method_rename_assumptions)
+(* Similiarly to method_rename_assumptions, just that rename assumptions about global variables are collected. *)
+type glob_var_rename_assumptions = varinfo VarinfoMap.t
 
-(*Compares two names, being aware of the rename_mapping. Returns true iff:
-  1. there is a rename for name1 -> name2 = rename(name1)
-  2. there is no rename for name1 -> name1 = name2*)
+(* On a successful match, these compinfo and enuminfo names have to be set to the snd element of the tuple. *)
+type renamesOnSuccess = (compinfo * compinfo) list * (enuminfo * enuminfo) list
+
+(* The rename_mapping is carried through the stack when comparing the AST. Holds a list of rename assumptions. The first
+   component is a map of rename assumptions about locals, i.e., parameters and local variables and is only used when
+   comparing functions. *)
+type rename_mapping = (string StringMap.t) * method_rename_assumptions * glob_var_rename_assumptions * renamesOnSuccess
+
+(* Compares two names, being aware of the rename_mapping. Returns true iff:
+   1. there is a rename for name1 -> name2 = rename(name1)
+   2. there is no rename for name1 -> name1 = name2 *)
 let rename_mapping_aware_name_comparison (name1: string) (name2: string) (rename_mapping: rename_mapping) =
-  let (local_c, method_c) = rename_mapping in
-  let existingAssumption: string option = StringMap.find_opt name1 local_c in
-
-  match existingAssumption with
-  | Some now ->
-    now = name2
-  | None ->
-    name1 = name2 (*Var names differ, but there is no assumption, so this can't be good*)
-
-let rename_mapping_to_string (rename_mapping: rename_mapping) =
-  let (local, methods) = rename_mapping in
-  let local_string = [%show: (string * string) list] (List.of_seq (StringMap.to_seq local)) in
-  let methods_string: string = List.of_seq (VarinfoMap.to_seq methods |> Seq.map snd) |>
-                               List.map (fun x -> match x with {original_method_name; new_method_name; parameter_renames} ->
-                                   "(methodName: " ^ original_method_name ^ " -> " ^ new_method_name ^
-                                   "; renamed_params=" ^ [%show: (string * string) list] (List.of_seq (StringMap.to_seq parameter_renames)) ^ ")") |>
-                               String.concat ", " in
-  "(local=" ^ local_string ^ "; methods=[" ^ methods_string ^ "])"
+  if GobConfig.get_bool "incremental.detect-renames" then (
+    let (local_c, method_c, _, _) = rename_mapping in
+    let existingAssumption: string option = StringMap.find_opt name1 local_c in
+
+    match existingAssumption with
+    | Some now ->
+      now = name2
+    | None ->
+      name1 = name2 (* Var names differ, but there is no assumption, so this can't be good *)
+  )
+  else name1 = name2
+
+(* Creates the mapping of local renames. If the locals do not match in size, an empty mapping is returned. *)
+let create_locals_rename_mapping (originalLocalNames: string list) (updatedLocalNames: string list): string StringMap.t =
+  if List.compare_lengths originalLocalNames updatedLocalNames = 0 then
+    List.combine originalLocalNames updatedLocalNames |>
+    List.filter (fun (original, now) -> not (original = now)) |>
+    List.map (fun (original, now) -> (original, now)) |>
+    (fun list ->
+       List.fold_left (fun map mapping -> StringMap.add (fst mapping) (snd mapping) map) StringMap.empty list
+    )
+  else StringMap.empty
+
+let is_rename_mapping_empty (rename_mapping: rename_mapping) =
+  let local, methods, glob_vars, _= rename_mapping in
+  StringMap.is_empty local && VarinfoMap.is_empty methods && VarinfoMap.is_empty glob_vars
+
+(* rename mapping forward propagation, takes the result from a call and propagates the rename mapping to the next call.
+   the second call is only executed if the previous call returned true *)
+let (&&>>) (prev_result: bool * rename_mapping) f : bool * rename_mapping =
+  let (prev_equal, updated_rename_mapping) = prev_result in
+  if prev_equal then f ~rename_mapping:updated_rename_mapping else false, updated_rename_mapping
+
+(* Same as && but propagates the rename mapping *)
+let (&&>) (prev_result: bool * rename_mapping) (b: bool) : bool * rename_mapping =
+  let (prev_equal, rename_mapping) = prev_result in
+  (prev_equal && b, rename_mapping)
+
+(* Same as Goblist.eq but propagates the rename_mapping *)
+let forward_list_equal ?(propF = (&&>>)) f l1 l2 ~(rename_mapping: rename_mapping) : bool * rename_mapping =
+  if ((List.compare_lengths l1 l2) = 0) then
+    List.fold_left2 (fun (b, r) x y -> propF (b, r) (f x y)) (true, rename_mapping) l1 l2
+  else false, rename_mapping
 
 (* hack: CIL generates new type names for anonymous types - we want to ignore these *)
 let compare_name (a: string) (b: string) =
@@ -38,36 +73,37 @@ let compare_name (a: string) (b: string) =
   let anon_union = "__anonunion_" in
   if a = b then true else BatString.(starts_with a anon_struct && starts_with b anon_struct || starts_with a anon_union && starts_with b anon_union)
 
-let rec eq_constant ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) (a: constant) (b: constant) =
+let rec eq_constant ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) (a: constant) (b: constant) : bool * rename_mapping =
   match a, b with
-  | CInt (val1, kind1, str1), CInt (val2, kind2, str2) -> Z.compare val1 val2 = 0 && kind1 = kind2 (* Ignore string representation, i.e. 0x2 == 2 *)
+  | CInt (val1, kind1, str1), CInt (val2, kind2, str2) -> Z.compare val1 val2 = 0 && kind1 = kind2, rename_mapping (* Ignore string representation, i.e. 0x2 == 2 *)
   | CEnum (exp1, str1, enuminfo1), CEnum (exp2, str2, enuminfo2) -> eq_exp exp1 exp2 ~rename_mapping ~acc (* Ignore name and enuminfo  *)
-  | a, b -> a = b
+  | a, b -> a = b, rename_mapping
 
-and eq_exp ?(no_const_vals = false) (a: exp) (b: exp) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) =
+and eq_exp (a: exp) (b: exp) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping =
   match a, b with
   | Const c1, Const c2 -> eq_constant c1 c2 ~rename_mapping ~acc
   | Lval lv1, Lval lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc
   | SizeOf typ1, SizeOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc
   | SizeOfE exp1, SizeOfE exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc
-  | SizeOfStr str1, SizeOfStr str2 -> str1 = str2 (* possibly, having the same length would suffice *)
+  | SizeOfStr str1, SizeOfStr str2 -> str1 = str2, rename_mapping (* possibly, having the same length would suffice *)
   | AlignOf typ1, AlignOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc
   | AlignOfE exp1, AlignOfE exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc
-  | UnOp (op1, exp1, typ1), UnOp (op2, exp2, typ2) -> op1 == op2 && eq_exp exp1 exp2 ~rename_mapping ~acc && eq_typ_acc typ1 typ2 ~rename_mapping ~acc
-  | BinOp (op1, left1, right1, typ1), BinOp (op2, left2, right2, typ2) ->  op1 = op2 && eq_exp left1 left2 ~rename_mapping ~acc && eq_exp right1 right2 ~rename_mapping ~acc && eq_typ_acc typ1 typ2 ~rename_mapping ~acc
-  | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc  && eq_exp exp1 exp2 ~rename_mapping ~acc
+  | UnOp (op1, exp1, typ1), UnOp (op2, exp2, typ2) ->
+    ((op1 == op2), rename_mapping) &&>> eq_exp exp1 exp2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
+  | BinOp (op1, left1, right1, typ1), BinOp (op2, left2, right2, typ2) ->  (op1 = op2, rename_mapping) &&>> eq_exp left1 left2 ~acc &&>> eq_exp right1 right2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
+  | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp exp1 exp2 ~acc
   | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc
   | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc
   | Real exp1, Real exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc
   | Imag exp1, Imag exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc
-  | Question (b1, t1, f1, typ1), Question (b2, t2, f2, typ2) -> eq_exp b1 b2 ~rename_mapping ~acc && eq_exp t1 t2 ~rename_mapping ~acc && eq_exp f1 f2 ~rename_mapping ~acc && eq_typ_acc typ1 typ2 ~rename_mapping ~acc
-  | AddrOfLabel _, AddrOfLabel _ -> false (* TODO: what to do? *)
-  | _, _ -> false
+  | Question (b1, t1, f1, typ1), Question (b2, t2, f2, typ2) -> eq_exp b1 b2 ~rename_mapping ~acc &&>> eq_exp t1 t2 ~acc &&>> eq_exp f1 f2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
+  | AddrOfLabel _, AddrOfLabel _ -> false, rename_mapping (* TODO: what to do? *)
+  | _, _ -> false, rename_mapping
 
 and eq_lhost (a: lhost) (b: lhost) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
     Var v1, Var v2 -> eq_varinfo v1 v2 ~rename_mapping ~acc
   | Mem exp1, Mem exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc
-  | _, _ -> false
+  | _, _ -> false, rename_mapping
 
 and global_typ_acc: (typ * typ) list ref = ref [] (* TODO: optimize with physical Hashtbl? *)
 
@@ -75,140 +111,180 @@ and mem_typ_acc (a: typ) (b: typ) acc = List.exists (fun p -> match p with (x, y
 
 and pretty_length () l = Pretty.num (List.length l)
 
-and eq_typ_acc (a: typ) (b: typ) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) =
+and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b: typ) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping =
+  (* Registers a compinfo rename or a enum rename*)
+  let register_rename_on_success = fun rename_mapping compinfo_option enum_option ->
+    let maybeAddTuple list option =
+      BatOption.map_default (fun v -> v :: list) list option
+    in
+
+    let (a, b, c, renames_on_success) = rename_mapping in
+    let (compinfoRenames, enumRenames) = renames_on_success in
+
+    let updatedCompinfoRenames = maybeAddTuple compinfoRenames compinfo_option in
+    let updatedEnumRenames = maybeAddTuple enumRenames enum_option in
+
+    a, b, c, (updatedCompinfoRenames, updatedEnumRenames)
+  in
+
   if Messages.tracing then Messages.tracei "compareast" "eq_typ_acc %a vs %a (%a, %a)\n" d_type a d_type b pretty_length acc pretty_length !global_typ_acc; (* %a makes List.length calls lazy if compareast isn't being traced *)
-  let r = match a, b with
-    | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc  && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc  && eq_exp lenExp1 lenExp2 ~rename_mapping ~acc &&  GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TArray (typ1, None, attr1), TArray (typ2, None, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc  && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TFun (typ1, (Some list1), varArg1, attr1), TFun (typ2, (Some list2), varArg2, attr2)
-      -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc  && GobList.equal (eq_args rename_mapping acc) list1 list2 && varArg1 = varArg2 &&
-         GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TFun (typ1, None, varArg1, attr1), TFun (typ2, None, varArg2, attr2)
-      ->  eq_typ_acc typ1 typ2 ~rename_mapping ~acc  && varArg1 = varArg2 &&
-          GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TNamed (typinfo1, attr1), TNamed (typinfo2, attr2) -> eq_typ_acc typinfo1.ttype typinfo2.ttype ~rename_mapping ~acc  && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2 (* Ignore tname, treferenced *)
-    | TNamed (tinf, attr), b -> eq_typ_acc tinf.ttype b ~rename_mapping ~acc  (* Ignore tname, treferenced. TODO: dismiss attributes, or not? *)
-    | a, TNamed (tinf, attr) -> eq_typ_acc a tinf.ttype ~rename_mapping ~acc  (* Ignore tname, treferenced . TODO: dismiss attributes, or not? *)
+  let r, updated_rename_mapping = match a, b with
+    | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2
+    | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp lenExp1 lenExp2 ~acc &&>>  forward_list_equal (eq_attribute ~acc) attr1 attr2
+    | TArray (typ1, None, attr1), TArray (typ2, None, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2
+    | TFun (typ1, (Some list1), varArg1, attr1), TFun (typ2, (Some list2), varArg2, attr2) ->
+      eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>>
+      forward_list_equal (eq_args ~fun_parameter_name_comparison_enabled ~acc) list1 list2 &&>
+      (varArg1 = varArg2) &&>>
+      forward_list_equal (eq_attribute ~acc) attr1 attr2
+    | TFun (typ1, None, varArg1, attr1), TFun (typ2, None, varArg2, attr2) ->
+      eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>
+      (varArg1 = varArg2) &&>>
+      forward_list_equal (eq_attribute ~acc) attr1 attr2
+    | TNamed (typinfo1, attr1), TNamed (typeinfo2, attr2) ->
+      eq_typ_acc typinfo1.ttype typeinfo2.ttype ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 (* Ignore tname, treferenced *)
+    | TNamed (tinf, attr), b -> eq_typ_acc tinf.ttype b ~rename_mapping ~acc (* Ignore tname, treferenced. TODO: dismiss attributes, or not? *)
+    | a, TNamed (tinf, attr) -> eq_typ_acc a tinf.ttype ~rename_mapping ~acc (* Ignore tname, treferenced . TODO: dismiss attributes, or not? *)
     (* The following two lines are a hack to ensure that anonymous types get the same name and thus, the same typsig *)
     | TComp (compinfo1, attr1), TComp (compinfo2, attr2) ->
       if mem_typ_acc a b acc || mem_typ_acc a b !global_typ_acc then (
         if Messages.tracing then Messages.trace "compareast" "in acc\n";
-        true
+        true, rename_mapping
       )
       else (
         let acc = (a, b) :: acc in
-        let res = eq_compinfo compinfo1 compinfo2 acc rename_mapping && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2 in
-        if res then begin
-          global_typ_acc := (a, b) :: !global_typ_acc;
-
-          (* Reset cnames and ckeys to the old value. Only affects anonymous structs/unions where names are not checked for equality. *)
-          compinfo2.cname <- compinfo1.cname;
-          compinfo2.ckey <- compinfo1.ckey;
-        end;
-        res
+        let (res, rm) = eq_compinfo compinfo1 compinfo2 acc rename_mapping &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 in
+        let updated_rm =
+          if res then (
+            global_typ_acc := (a, b) :: !global_typ_acc;
+            register_rename_on_success rm (Some((compinfo2, compinfo1))) None
+          ) else rm
+        in
+        res, updated_rm
       )
-    | TEnum (enuminfo1, attr1), TEnum (enuminfo2, attr2) -> let res = eq_enuminfo enuminfo1 enuminfo2 ~rename_mapping ~acc && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2 in (if res && enuminfo1.ename <> enuminfo2.ename then enuminfo2.ename <- enuminfo1.ename); res
-    | TBuiltin_va_list attr1, TBuiltin_va_list attr2 -> GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TVoid attr1, TVoid attr2 -> GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TInt (ik1, attr1), TInt (ik2, attr2) -> ik1 = ik2 && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | TFloat (fk1, attr1), TFloat (fk2, attr2) -> fk1 = fk2 && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
-    | _, _ -> false
+    | TEnum (enuminfo1, attr1), TEnum (enuminfo2, attr2) ->
+      let (res, rm) = eq_enuminfo enuminfo1 enuminfo2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 in
+      if res && enuminfo1.ename <> enuminfo2.ename then
+        res, register_rename_on_success rm None (Some((enuminfo2, enuminfo1)))
+      else res, rm
+    | TBuiltin_va_list attr1, TBuiltin_va_list attr2 -> forward_list_equal (eq_attribute ~acc) attr1 attr2 ~rename_mapping
+    | TVoid attr1, TVoid attr2 -> forward_list_equal (eq_attribute ~acc) attr1 attr2 ~rename_mapping
+    | TInt (ik1, attr1), TInt (ik2, attr2) -> (ik1 = ik2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2
+    | TFloat (fk1, attr1), TFloat (fk2, attr2) -> (fk1 = fk2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2
+    | _, _ -> false, rename_mapping
   in
   if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a\n" d_type a d_type b;
-  r
+  (r, updated_rename_mapping)
 
-
-and eq_eitems ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) (a: string * exp * location) (b: string * exp * location) = match a, b with
-    (name1, exp1, _l1), (name2, exp2, _l2) -> name1 = name2 && eq_exp exp1 exp2 ~rename_mapping ~acc
+and eq_eitems (a: string * exp * location) (b: string * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
+    (name1, exp1, _l1), (name2, exp2, _l2) -> (name1 = name2, rename_mapping) &&>> eq_exp exp1 exp2 ~acc
 (* Ignore location *)
 
 and eq_enuminfo (a: enuminfo) (b: enuminfo) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) =
-  compare_name a.ename b.ename &&
-  GobList.equal (eq_attribute ~rename_mapping ~acc) a.eattr b.eattr &&
-  GobList.equal (eq_eitems ~rename_mapping ~acc) a.eitems b.eitems
+  (compare_name a.ename b.ename, rename_mapping) &&>>
+  forward_list_equal (eq_attribute ~acc) a.eattr b.eattr &&>>
+  forward_list_equal (eq_eitems ~acc) a.eitems b.eitems
 (* Ignore ereferenced *)
 
-and eq_args (rename_mapping: rename_mapping) (acc: (typ * typ) list) (a: string * typ * attributes) (b: string * typ * attributes) = match a, b with
+(*param: fun_parameter_name_comparison_enabled when set to false, skips the comparison of the names*)
+and eq_args ?(fun_parameter_name_comparison_enabled: bool = true) (a: string * typ * attributes) (b: string * typ * attributes) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with
     (name1, typ1, attr1), (name2, typ2, attr2) ->
-    rename_mapping_aware_name_comparison name1 name2 rename_mapping && eq_typ_acc typ1 typ2 ~rename_mapping ~acc && GobList.equal (eq_attribute ~rename_mapping ~acc) attr1 attr2
+    ((not fun_parameter_name_comparison_enabled) || rename_mapping_aware_name_comparison name1 name2 rename_mapping, rename_mapping) &&>>
+    eq_typ_acc typ1 typ2 ~acc &&>>
+    forward_list_equal (eq_attribute ~acc) attr1 attr2
 
-and eq_attrparam ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) (a: attrparam) (b: attrparam) = match a, b with
-  | ACons (str1, attrparams1), ACons (str2, attrparams2) -> str1 = str2 && GobList.equal (eq_attrparam ~rename_mapping ~acc) attrparams1 attrparams2
+and eq_attrparam (a: attrparam) (b: attrparam) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with
+  | ACons (str1, attrparams1), ACons (str2, attrparams2) -> (str1 = str2, rename_mapping) &&>> forward_list_equal (eq_attrparam ~acc) attrparams1 attrparams2
   | ASizeOf typ1, ASizeOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc
   | ASizeOfE attrparam1, ASizeOfE attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc
-  | ASizeOfS typsig1, ASizeOfS typsig2 -> typsig1 = typsig2
+  | ASizeOfS typsig1, ASizeOfS typsig2 -> typsig1 = typsig2, rename_mapping
   | AAlignOf typ1, AAlignOf typ2 -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc
   | AAlignOfE attrparam1, AAlignOfE attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc
-  | AAlignOfS typsig1, AAlignOfS typsig2 -> typsig1 = typsig2
-  | AUnOp (op1, attrparam1), AUnOp (op2, attrparam2) -> op1 = op2 && eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc
-  | ABinOp (op1, left1, right1), ABinOp (op2, left2, right2) -> op1 = op2 && eq_attrparam left1 left2 ~rename_mapping ~acc && eq_attrparam right1 right2 ~rename_mapping ~acc
-  | ADot (attrparam1, str1), ADot (attrparam2, str2) -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc && str1 = str2
+  | AAlignOfS typsig1, AAlignOfS typsig2 -> typsig1 = typsig2, rename_mapping
+  | AUnOp (op1, attrparam1), AUnOp (op2, attrparam2) -> (op1 = op2, rename_mapping) &&>> eq_attrparam attrparam1 attrparam2 ~acc
+  | ABinOp (op1, left1, right1), ABinOp (op2, left2, right2) -> (op1 = op2, rename_mapping) &&>> eq_attrparam left1 left2 ~acc &&>> eq_attrparam right1 right2 ~acc
+  | ADot (attrparam1, str1), ADot (attrparam2, str2) -> (str1 = str2, rename_mapping) &&>> eq_attrparam attrparam1 attrparam2 ~acc
   | AStar attrparam1, AStar attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc
   | AAddrOf attrparam1, AAddrOf attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc
-  | AIndex (left1, right1), AIndex (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc && eq_attrparam right1 right2 ~rename_mapping ~acc
-  | AQuestion (left1, middle1, right1), AQuestion (left2, middle2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc && eq_attrparam middle1 middle2 ~rename_mapping ~acc && eq_attrparam right1 right2 ~rename_mapping ~acc
-  | a, b -> a = b
+  | AIndex (left1, right1), AIndex (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam right1 right2 ~acc
+  | AQuestion (left1, middle1, right1), AQuestion (left2, middle2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam middle1 middle2 ~acc &&>> eq_attrparam right1 right2 ~acc
+  | a, b -> a = b, rename_mapping
+
+and eq_attribute (a: attribute) (b: attribute) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) = match a, b with
+  | Attr (name1, params1), Attr (name2, params2) -> (name1 = name2, rename_mapping) &&>> forward_list_equal (eq_attrparam ~acc) params1 params2
 
-and eq_attribute  ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) (a: attribute) (b: attribute) = match a, b with
-  | Attr (name1, params1), Attr (name2, params2) -> name1 = name2 && GobList.equal (eq_attrparam ~rename_mapping ~acc ) params1 params2
+and eq_varinfo (a: varinfo) (b: varinfo) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) =
 
-and eq_varinfo  (a: varinfo) (b: varinfo) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) =
+  let (locals_renames, method_rename_mappings, glob_vars, renames_on_success) = rename_mapping in
 
-  let (_, method_rename_mappings) = rename_mapping in
+  let compare_local_and_global_var =
+    if a.vglob then
+      let present_mapping = VarinfoMap.find_opt a glob_vars in
+
+      match present_mapping with
+      | Some (knownNowVarinfo) ->
+        b.vname = knownNowVarinfo.vname, method_rename_mappings, glob_vars
+      | None -> (
+          let update_glob_vars = VarinfoMap.add a b glob_vars in
+          true, method_rename_mappings, update_glob_vars
+        )
+    else rename_mapping_aware_name_comparison a.vname b.vname rename_mapping, method_rename_mappings, glob_vars
+  in
 
   (*When we compare function names, we can directly compare the naming from the rename_mapping if it exists.*)
-  let isNamingOk = match b.vtype with
-    | TFun(_, _, _, _) -> (
+  let isNamingOk, updated_method_rename_mappings, updatedGlobVarMapping = match a.vtype, b.vtype with
+    | TFun(_, aParamSpec, _, _), TFun(_, bParamSpec, _, _) -> (
         let specific_method_rename_mapping = VarinfoMap.find_opt a method_rename_mappings in
         match specific_method_rename_mapping with
-        | Some method_rename_mapping -> method_rename_mapping.original_method_name = a.vname && method_rename_mapping.new_method_name = b.vname
-        | None -> a.vname = b.vname
+        | Some new_varinfo ->
+          let is_naming_ok = new_varinfo.vname = b.vname in
+          is_naming_ok, method_rename_mappings, glob_vars
+        | None ->
+          if a.vname <> b.vname then
+            true, VarinfoMap.add a b method_rename_mappings, glob_vars
+          else true, method_rename_mappings, glob_vars
       )
-    | _ -> rename_mapping_aware_name_comparison a.vname b.vname rename_mapping
+    | _, _ -> compare_local_and_global_var
   in
 
   (*If the following is a method call, we need to check if we have a mapping for that method call. *)
-  let typ_rename_mapping = match b.vtype with
-    | TFun(_, _, _, _) -> (
-        let new_locals = VarinfoMap.find_opt a method_rename_mappings in
-
-        match new_locals with
-        | Some locals ->
-          (locals.parameter_renames, method_rename_mappings)
-        | None -> (StringMap.empty, method_rename_mappings)
-      )
-    | _ -> rename_mapping
+  let fun_parameter_name_comparison_enabled = match b.vtype with
+    | TFun(_, _, _, _) -> false
+    | _ -> true
   in
 
-  let typeCheck = eq_typ_acc a.vtype b.vtype ~rename_mapping:typ_rename_mapping ~acc  in
-  let attrCheck = GobList.equal (eq_attribute ~rename_mapping ~acc ) a.vattr b.vattr in
+  (*Ignore rename mapping for type check, as it doesn't change anyway. We only need the renames_on_success*)
+  let (typeCheck, (_, _, _, updated_renames_on_success)) = eq_typ_acc ~fun_parameter_name_comparison_enabled a.vtype b.vtype ~rename_mapping:(StringMap.empty, VarinfoMap.empty, VarinfoMap.empty, renames_on_success) ~acc in
 
-  isNamingOk && typeCheck && attrCheck && a.vstorage = b.vstorage && a.vglob = b.vglob && a.vaddrof = b.vaddrof
+  (isNamingOk && typeCheck, (locals_renames, updated_method_rename_mappings, updatedGlobVarMapping, updated_renames_on_success)) &&>>
+  forward_list_equal (eq_attribute ~acc) a.vattr b.vattr &&>
+  (a.vstorage = b.vstorage) &&> (a.vglob = b.vglob) &&> (a.vaddrof = b.vaddrof)
 (* Ignore the location, vid, vreferenced, vdescr, vdescrpure, vinline *)
 
 (* Accumulator is needed because of recursive types: we have to assume that two types we already encountered in a previous step of the recursion are equivalent *)
-and eq_compinfo (a: compinfo) (b: compinfo) (acc: (typ * typ) list) (rename_mapping: rename_mapping) =
-  a.cstruct = b.cstruct &&
-  compare_name a.cname b.cname &&
-  GobList.equal (fun a b-> eq_fieldinfo a b ~rename_mapping ~acc ) a.cfields b.cfields &&
-  GobList.equal (eq_attribute ~rename_mapping ~acc ) a.cattr b.cattr &&
-  a.cdefined = b.cdefined (* Ignore ckey, and ignore creferenced *)
+and eq_compinfo (a: compinfo) (b: compinfo) (acc: (typ * typ) list) (rename_mapping: rename_mapping) : bool * rename_mapping =
+  (a.cstruct = b.cstruct, rename_mapping) &&>
+  compare_name a.cname b.cname &&>>
+  forward_list_equal (fun a b -> eq_fieldinfo a b ~acc) a.cfields b.cfields &&>>
+  forward_list_equal (eq_attribute ~acc ) a.cattr b.cattr &&>
+  (a.cdefined = b.cdefined) (* Ignore ckey, and ignore creferenced *)
 
 and eq_fieldinfo (a: fieldinfo) (b: fieldinfo) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) =
   if Messages.tracing then Messages.tracei "compareast" "fieldinfo %s vs %s\n" a.fname b.fname;
-  let r = a.fname = b.fname && eq_typ_acc a.ftype b.ftype ~rename_mapping ~acc  && a.fbitfield = b.fbitfield &&  GobList.equal (eq_attribute ~rename_mapping ~acc) a.fattr b.fattr in
+  let (r, rm) = (a.fname = b.fname, rename_mapping) &&>>
+                eq_typ_acc a.ftype b.ftype ~acc &&> (a.fbitfield = b.fbitfield) &&>>
+                forward_list_equal (eq_attribute ~acc) a.fattr b.fattr in
   if Messages.tracing then Messages.traceu "compareast" "fieldinfo %s vs %s\n" a.fname b.fname;
-  r
+  (r, rm)
 
-and eq_offset (a: offset) (b: offset) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
-    NoOffset, NoOffset -> true
-  | Field (info1, offset1), Field (info2, offset2) -> eq_fieldinfo info1 info2 ~rename_mapping ~acc && eq_offset offset1 offset2 ~rename_mapping ~acc
-  | Index (exp1, offset1), Index (exp2, offset2) -> eq_exp exp1 exp2 ~rename_mapping ~acc && eq_offset offset1 offset2 ~rename_mapping ~acc
-  | _, _ -> false
+and eq_offset (a: offset) (b: offset) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with
+    NoOffset, NoOffset -> true, rename_mapping
+  | Field (info1, offset1), Field (info2, offset2) -> eq_fieldinfo info1 info2 ~rename_mapping ~acc &&>> eq_offset offset1 offset2 ~acc
+  | Index (exp1, offset1), Index (exp2, offset2) -> eq_exp exp1 exp2 ~rename_mapping ~acc &&>> eq_offset offset1 offset2 ~acc
+  | _, _ -> false, rename_mapping
 
-and eq_lval (a: lval) (b: lval) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
-    (host1, off1), (host2, off2) -> eq_lhost host1 host2 ~rename_mapping ~acc && eq_offset off1 off2 ~rename_mapping ~acc
+and eq_lval (a: lval) (b: lval) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) : bool * rename_mapping = match a, b with
+    (host1, off1), (host2, off2) -> eq_lhost host1 host2 ~rename_mapping ~acc &&>> eq_offset off1 off2 ~acc
 
 let eq_typ =
   eq_typ_acc ~acc:[]
@@ -226,14 +302,19 @@ let eq_offset =
   eq_offset ~acc:[]
 
 let eq_instr (a: instr) (b: instr) ~(rename_mapping: rename_mapping) = match a, b with
-  | Set (lv1, exp1, _l1, _el1), Set (lv2, exp2, _l2, _el2) -> eq_lval lv1 lv2 ~rename_mapping && eq_exp exp1 exp2 ~rename_mapping
+  | Set (lv1, exp1, _l1, _el1), Set (lv2, exp2, _l2, _el2) -> eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp exp1 exp2
   | Call (Some lv1, f1, args1, _l1, _el1), Call (Some lv2, f2, args2, _l2, _el2) ->
-    eq_lval lv1 lv2 ~rename_mapping && eq_exp f1 f2 ~rename_mapping && GobList.equal (eq_exp ~rename_mapping) args1 args2
+    eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp f1 f2 &&>> forward_list_equal eq_exp args1 args2
   | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) ->
-    eq_exp f1 f2 ~rename_mapping && GobList.equal (eq_exp ~rename_mapping) args1 args2
-  | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) -> GobList.equal String.equal tmp1 tmp2 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_lval z1 z2 ~rename_mapping) ci1 ci2 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_exp z1 z2 ~rename_mapping) dj1 dj2 && GobList.equal String.equal rk1 rk2(* ignore attributes and locations *)
+    eq_exp f1 f2 ~rename_mapping &&>> forward_list_equal eq_exp args1 args2
+  | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) ->
+    (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&>
+    GobList.equal String.equal rk1 rk2(* ignore attributes and locations *)
   | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2 ~rename_mapping
-  | _, _ -> false
+  | _, _ -> false, rename_mapping
+
 
 let eq_label (a: label) (b: label) = match a, b with
     Label (lb1, _l1, s1), Label (lb2, _l2, s2) -> lb1 = lb2 && s1 = s2
@@ -251,35 +332,40 @@ let eq_stmt_with_location ((a, af): stmt * fundec) ((b, bf): stmt * fundec) =
    through the cfg and only compares the currently visited node (The cil blocks inside an if statement should not be
    compared together with its condition to avoid a to early and not precise detection of a changed node inside).
    Switch, break and continue statements are removed during cfg preparation and therefore need not to be handeled *)
+
 let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): stmtkind * fundec) ~(rename_mapping: rename_mapping) =
-  let eq_block' = fun x y -> if cfg_comp then true else eq_block (x, af) (y, bf) ~rename_mapping in
+  let eq_block' = fun x y ~(rename_mapping:rename_mapping) -> if cfg_comp then true, rename_mapping else eq_block (x, af) (y, bf) ~rename_mapping in
   match a, b with
-  | Instr is1, Instr is2 -> GobList.equal (eq_instr ~rename_mapping) is1 is2
+  | Instr is1, Instr is2 -> forward_list_equal eq_instr is1 is2 ~rename_mapping
   | Return (Some exp1, _l1), Return (Some exp2, _l2) -> eq_exp exp1 exp2 ~rename_mapping
-  | Return (None, _l1), Return (None, _l2) -> true
-  | Return _, Return _ -> false
-  | Goto (st1, _l1), Goto (st2, _l2) -> eq_stmt_with_location (!st1, af) (!st2, bf)
-  | Break _, Break _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true
-  | Continue _, Continue _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true
-  | If (exp1, then1, else1, _l1, _el1), If (exp2, then2, else2, _l2, _el2) -> eq_exp exp1 exp2 ~rename_mapping && eq_block' then1 then2 && eq_block' else1 else2
-  | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 ~rename_mapping && eq_block' block1 block2 && GobList.equal (fun a b -> eq_stmt (a,af) (b,bf) ~rename_mapping) stmts1 stmts2
-  | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2
-  | Block block1, Block block2 -> eq_block' block1 block2
-  | _, _ -> false
+  | Return (None, _l1), Return (None, _l2) -> true, rename_mapping
+  | Return _, Return _ -> false, rename_mapping
+  | Goto (st1, _l1), Goto (st2, _l2) -> eq_stmt_with_location (!st1, af) (!st2, bf), rename_mapping
+  | Break _, Break _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true, rename_mapping
+  | Continue _, Continue _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true, rename_mapping
+  | If (exp1, then1, else1, _l1, _el1), If (exp2, then2, else2, _l2, _el2) -> eq_exp exp1 exp2 ~rename_mapping &&>>
+                                                                              eq_block' then1 then2 &&>>
+                                                                              eq_block' else1 else2
+  | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 ~rename_mapping &&>> eq_block' block1 block2 &&>> forward_list_equal (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
+  | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2 ~rename_mapping
+  | Block block1, Block block2 -> eq_block' block1 block2 ~rename_mapping
+  | _, _ -> false, rename_mapping
 
 and eq_stmt ?cfg_comp ((a, af): stmt * fundec) ((b, bf): stmt * fundec) ~(rename_mapping: rename_mapping) =
-  GobList.equal eq_label a.labels b.labels &&
-  eq_stmtkind ?cfg_comp (a.skind, af) (b.skind, bf) ~rename_mapping
+  (GobList.equal eq_label a.labels b.labels, rename_mapping) &&>>
+  eq_stmtkind ?cfg_comp (a.skind, af) (b.skind, bf)
 
-and eq_block ((a, af): Cil.block * fundec) ((b, bf): Cil.block * fundec) ~(rename_mapping: rename_mapping) =
-  a.battrs = b.battrs && GobList.equal (fun x y -> eq_stmt (x, af) (y, bf) ~rename_mapping) a.bstmts b.bstmts
+and eq_block ((a, af): Cil.block * fundec) ((b, bf): Cil.block * fundec) ~(rename_mapping: rename_mapping) : bool * rename_mapping =
+  (a.battrs = b.battrs, rename_mapping) &&>> forward_list_equal (fun x y -> eq_stmt (x, af) (y, bf)) a.bstmts b.bstmts
 
 let rec eq_init (a: init) (b: init) ~(rename_mapping: rename_mapping) = match a, b with
   | SingleInit e1, SingleInit e2 -> eq_exp e1 e2 ~rename_mapping
-  | CompoundInit (t1, l1), CompoundInit (t2, l2) -> eq_typ t1 t2 ~rename_mapping && GobList.equal (fun (o1, i1) (o2, i2) -> eq_offset o1 o2 ~rename_mapping && eq_init i1 i2 ~rename_mapping) l1 l2
-  | _, _ -> false
+  | CompoundInit (t1, l1), CompoundInit (t2, l2) ->
+    eq_typ t1 t2 ~rename_mapping &&>>
+    forward_list_equal (fun (o1, i1) (o2, i2) ~rename_mapping:rename_mapping -> eq_offset o1 o2 ~rename_mapping &&>> eq_init i1 i2) l1 l2
+  | _, _ -> false, rename_mapping
 
-let eq_initinfo (a: initinfo) (b: initinfo) (rename_mapping: rename_mapping) = match a.init, b.init with
+let eq_initinfo (a: initinfo) (b: initinfo) ~(rename_mapping: rename_mapping) = match a.init, b.init with
   | (Some init_a), (Some init_b) -> eq_init init_a init_b ~rename_mapping
-  | None, None -> true
-  | _, _ -> false
+  | None, None -> true, rename_mapping
+  | _, _ -> false, rename_mapping
diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
index 93bb855606..0d35df1fa3 100644
--- a/src/incremental/compareCFG.ml
+++ b/src/incremental/compareCFG.ml
@@ -1,12 +1,19 @@
 open MyCFG
 open Queue
 open GoblintCil
-open CilMaps
 include CompareAST
 
-let eq_node (x, fun1) (y, fun2) =
-  let empty_rename_mapping: rename_mapping = (StringMap.empty, VarinfoMap.empty) in
-  (* don't allow pseudo return node to be equal to normal return node, could make function unchanged, but have different sallstmts *)
+(*Non propagating version of &&>>. Discards the new rename_mapping and alwas propagates the one in prev_result. However propagates the renames_on_success*)
+let (&&<>) (prev_result: bool * rename_mapping) f : bool * rename_mapping =
+  let (prev_equal, prev_rm) = prev_result in
+  let (a, b, c, _) = prev_rm in
+
+  if prev_equal then
+    let (r, ((_, _, _, updated_renames_on_success) : rename_mapping)) = f ~rename_mapping:prev_rm in
+    (r, (a, b, c, updated_renames_on_success))
+  else false, prev_rm
+
+let eq_node (x, fun1) (y, fun2) ~rename_mapping =
   let isPseudoReturn f sid =
     let pid = CfgTools.get_pseudo_return_id f in
     sid == pid in
@@ -14,30 +21,29 @@ let eq_node (x, fun1) (y, fun2) =
   | Statement s1, Statement s2 ->
     let p1 = isPseudoReturn fun1 s1.sid in
     let p2 = isPseudoReturn fun2 s2.sid in
-    ((p1 && p2) || not (p1 || p2)) && eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2) ~rename_mapping:empty_rename_mapping
-  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar ~rename_mapping:empty_rename_mapping
-  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar ~rename_mapping:empty_rename_mapping
-  | _ -> false
+    ((p1 && p2) || not (p1 || p2), rename_mapping) &&>> eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2)
+  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar ~rename_mapping
+  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar ~rename_mapping
+  | _ -> false, rename_mapping
 
 (* TODO: compare ASMs properly instead of simply always assuming that they are not the same *)
-let eq_edge x y =
-  let empty_rename_mapping: rename_mapping = (StringMap.empty, VarinfoMap.empty) in
+let eq_edge x y ~rename_mapping =
   match x, y with
-  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 ~rename_mapping:empty_rename_mapping && eq_exp rv1 rv2 ~rename_mapping:empty_rename_mapping
-  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 ~rename_mapping:empty_rename_mapping && GobList.equal (eq_exp ~rename_mapping:empty_rename_mapping) ars1 ars2
+  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 ~rename_mapping &&<> eq_exp rv1 rv2
+  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 ~rename_mapping &&<> forward_list_equal eq_exp ars1 ars2
   | Proc (Some r1,f1,ars1), Proc (Some r2,f2,ars2) ->
-    eq_lval r1 r2 ~rename_mapping:empty_rename_mapping && eq_exp f1 f2 ~rename_mapping:empty_rename_mapping && GobList.equal (eq_exp ~rename_mapping:empty_rename_mapping) ars1 ars2
-  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar ~rename_mapping:empty_rename_mapping
-  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar ~rename_mapping:empty_rename_mapping
-  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 ~rename_mapping:empty_rename_mapping && eq_varinfo fd1.svar fd2.svar ~rename_mapping:empty_rename_mapping
-  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 ~rename_mapping:empty_rename_mapping && b1 = b2
-  | ASM _, ASM _ -> false
-  | Skip, Skip -> true
-  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2 ~rename_mapping:empty_rename_mapping
-  | _ -> false
+    eq_lval r1 r2 ~rename_mapping &&<> eq_exp f1 f2 &&<> forward_list_equal eq_exp ars1 ars2
+  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar ~rename_mapping
+  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar ~rename_mapping
+  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 ~rename_mapping &&<> eq_varinfo fd1.svar fd2.svar
+  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 ~rename_mapping &&> (b1 = b2)
+  | ASM _, ASM _ -> false, rename_mapping
+  | Skip, Skip -> true, rename_mapping
+  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2 ~rename_mapping
+  | _ -> false, rename_mapping
 
 (* The order of the edges in the list is relevant. Therefore compare them one to one without sorting first *)
-let eq_edge_list xs ys = GobList.equal eq_edge xs ys
+let eq_edge_list xs ys = forward_list_equal ~propF:(&&<>) eq_edge xs ys
 
 let to_edge_list ls = List.map (fun (loc, edge) -> edge) ls
 
@@ -50,13 +56,14 @@ type biDirectionNodeMap = {node1to2: node NH.t; node2to1: node NH.t}
  * in the succesors of fromNode2 in the new CFG. Matching node tuples are added to the waitingList to repeat the matching
  * process on their successors. If a node from the old CFG can not be matched, it is added to diff and no further
  * comparison is done for its successors. The two function entry nodes make up the tuple to start the comparison from. *)
-let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 fun2 =
+
+let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 fun2 rename_mapping : biDirectionNodeMap * unit NH.t * rename_mapping =
   let diff = NH.create 113 in
   let same = {node1to2=NH.create 113; node2to1=NH.create 113} in
   let waitingList : (node * node) t = Queue.create () in
 
-  let rec compareNext () =
-    if Queue.is_empty waitingList then ()
+  let rec compareNext rename_mapping : rename_mapping =
+    if Queue.is_empty waitingList then rename_mapping
     else
       let fromNode1, fromNode2 = Queue.take waitingList in
       let outList1 = CfgOld.next fromNode1 in
@@ -64,23 +71,25 @@ let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 f
 
       (* Find a matching edge and successor node for (edgeList1, toNode1) in the list of successors of fromNode2.
        * If successful, add the matching node tuple to same, else add toNode1 to the differing nodes. *)
-      let findMatch (edgeList1, toNode1) =
-        let rec aux remSuc = match remSuc with
-          | [] -> NH.replace diff toNode1 ()
+      let findMatch (edgeList1, toNode1) rename_mapping : rename_mapping =
+        let rec aux remSuc rename_mapping : rename_mapping = match remSuc with
+          | [] -> NH.replace diff toNode1 (); rename_mapping
           | (locEdgeList2, toNode2)::remSuc' ->
             let edgeList2 = to_edge_list locEdgeList2 in
-            if eq_node (toNode1, fun1) (toNode2, fun2) && eq_edge_list edgeList1 edgeList2 then
+            let (isEq, updatedRenameMapping) = (true, rename_mapping) &&>> eq_node (toNode1, fun1) (toNode2, fun2) &&>> eq_edge_list edgeList1 edgeList2 in
+            if isEq then
               begin
                 match NH.find_opt same.node1to2 toNode1 with
-                | Some n2 -> if not (Node.equal n2 toNode2) then NH.replace diff toNode1 ()
-                | None -> NH.replace same.node1to2 toNode1 toNode2; NH.replace same.node2to1 toNode2 toNode1; Queue.add (toNode1, toNode2) waitingList
+                | Some n2 -> if not (Node.equal n2 toNode2) then NH.replace diff toNode1 (); updatedRenameMapping
+                | None -> NH.replace same.node1to2 toNode1 toNode2; NH.replace same.node2to1 toNode2 toNode1; Queue.add (toNode1, toNode2) waitingList;
+                  updatedRenameMapping
               end
-            else aux remSuc' in
-        aux outList2 in
+            else aux remSuc' updatedRenameMapping in
+        aux outList2 rename_mapping in
       (* For a toNode1 from the list of successors of fromNode1, check whether it might have duplicate matches.
        * In that case declare toNode1 as differing node. Else, try finding a match in the list of successors
        * of fromNode2 in the new CFG using findMatch. *)
-      let iterOuts (locEdgeList1, toNode1) =
+      let iterOuts (locEdgeList1, toNode1) rename_mapping : rename_mapping =
         let edgeList1 = to_edge_list locEdgeList1 in
         (* Differentiate between a possibly duplicate Test(1,false) edge and a single occurence. In the first
          * case the edge is directly added to the diff set to avoid undetected ambiguities during the recursive
@@ -91,13 +100,18 @@ let compareCfgs (module CfgOld : CfgForward) (module CfgNew : CfgForward) fun1 f
         let posAmbigEdge edgeList = let findTestFalseEdge (ll,_) = testFalseEdge (snd (List.hd ll)) in
           let numDuplicates l = List.length (List.find_all findTestFalseEdge l) in
           testFalseEdge (List.hd edgeList) && (numDuplicates outList1 > 1 || numDuplicates outList2 > 1) in
-        if posAmbigEdge edgeList1 then NH.replace diff toNode1 ()
-        else findMatch (edgeList1, toNode1) in
-      List.iter iterOuts outList1; compareNext () in
+        if posAmbigEdge edgeList1 then (NH.replace diff toNode1 (); rename_mapping)
+        else findMatch (edgeList1, toNode1) rename_mapping in
+      let updatedRenameMapping = List.fold_left (fun rm e -> iterOuts e rm) rename_mapping outList1 in
+      compareNext updatedRenameMapping
+  in
 
   let entryNode1, entryNode2 = (FunctionEntry fun1, FunctionEntry fun2) in
-  NH.replace same.node1to2 entryNode1 entryNode2; NH.replace same.node2to1 entryNode2 entryNode1;
-  Queue.push (entryNode1,entryNode2) waitingList; compareNext (); (same, diff)
+  NH.replace same.node1to2 entryNode1 entryNode2;
+  NH.replace same.node2to1 entryNode2 entryNode1;
+  Queue.push (entryNode1,entryNode2) waitingList;
+  let updatedRenameMapping = compareNext rename_mapping in
+  same, diff, updatedRenameMapping
 
 (* This is the second phase of the CFG comparison of functions. It removes the nodes from the matching node set 'same'
  * that have an incoming backedge in the new CFG that can be reached from a differing new node. This is important to
@@ -120,7 +134,8 @@ let reexamine f1 f2 (same : biDirectionNodeMap) (diffNodes1 : unit NH.t) (module
   repeat ();
   NH.to_seq same.node1to2, NH.to_seq_keys diffNodes1
 
-let compareFun (module CfgOld : CfgForward) (module CfgNew : CfgBidir) fun1 fun2 =
-  let same, diff = Timing.wrap "compare-phase1" (fun () -> compareCfgs (module CfgOld) (module CfgNew) fun1 fun2) () in
+
+let compareFun (module CfgOld : CfgForward) (module CfgNew : CfgBidir) fun1 fun2 rename_mapping : (node * node) list * node list * rename_mapping =
+  let same, diff, rename_mapping = Timing.wrap "compare-phase1" (fun () -> compareCfgs (module CfgOld) (module CfgNew) fun1 fun2 rename_mapping) () in
   let unchanged, diffNodes1 = Timing.wrap "compare-phase2" (fun () -> reexamine fun1 fun2 same diff (module CfgOld) (module CfgNew)) () in
-  List.of_seq unchanged, List.of_seq diffNodes1
+  List.of_seq unchanged, List.of_seq diffNodes1, rename_mapping
diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index b218cb18e0..f89a72f8be 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -1,14 +1,36 @@
 open GoblintCil
 open MyCFG
-open CilMaps
 include CompareAST
 include CompareCFG
+include CilMaps
 
 module GlobalMap = Map.Make(String)
 
 type global_def = Var of varinfo | Fun of fundec
 type global_col = {decls: varinfo option; def: global_def option}
 
+let name_of_global_col gc = match gc.def with
+  | Some (Fun f) -> f.svar.vname
+  | Some (Var v) -> v.vname
+  | None -> match gc.decls with
+    | Some v -> v.vname
+    | None -> raise (Failure "empty global record")
+
+let compare_global_col gc1 gc2 = compare (name_of_global_col gc1) (name_of_global_col gc2)
+let equal_name_global_col gc1 gc2 = compare_global_col gc1 gc2 == 0
+
+let get_varinfo gc = match gc.decls, gc.def with
+  | _, Some (Var v) -> v
+  | _, Some (Fun f) -> f.svar
+  | Some v, _ -> v
+  | _ -> failwith "A global should have at least a declaration or a definition"
+
+module GlobalColMap = Map.Make(
+  struct
+    type t = global_col
+    let compare = compare_global_col
+  end)
+
 let name_of_global g = match g with
   | GVar (v,_,_) -> v.vname
   | GFun (f,_) -> f.svar.vname
@@ -57,80 +79,218 @@ let unchanged_to_change_status = function
   | true -> Unchanged
   | false -> Changed
 
+let empty_rename_mapping: rename_mapping = (StringMap.empty, VarinfoMap.empty, VarinfoMap.empty, ([], []))
+
 let should_reanalyze (fdec: Cil.fundec) =
   List.mem fdec.svar.vname (GobConfig.get_string_list "incremental.force-reanalyze.funs")
 
+let performRenames (renamesOnSuccess: renamesOnSuccess) =
+  begin
+    let (compinfoRenames, enumRenames) = renamesOnSuccess in
+    (* Reset cnames and ckeys to the old value. Only affects anonymous structs/unions where names are not checked for equality. *)
+    List.iter (fun (compinfo2, compinfo1) -> compinfo2.cname <- compinfo1.cname; compinfo2.ckey <- compinfo1.ckey) compinfoRenames;
+    List.iter (fun (enum2, enum1) -> enum2.ename <- enum1.ename) enumRenames;
+  end
+
+let preservesSameNameMatches n_old oldMap n_new newMap = n_old = n_new || (not (GlobalMap.mem n_old newMap) && not (GlobalMap.mem n_new oldMap))
+
+let addToFinalMatchesMapping oV nV final_matches =
+  VarinfoMap.add oV nV (fst final_matches), VarinfoMap.add nV oV (snd final_matches)
+
+let empty_rename_assms m = VarinfoMap.for_all (fun vo vn -> vo.vname = vn.vname) m
+
+let already_matched oV nV final_matches =
+  match VarinfoMap.find_opt oV (fst final_matches) with
+  | None -> false
+  | Some v -> v.vid = oV.vid
+
+(* looks up the result of the already executed comparison and returns true if it is unchanged, false if it is changed.
+   Throws an exception if not found. *)
+let change_info_lookup old_glob new_glob change_info =
+  List.exists (fun (u : unchanged_global) -> equal_name_global_col u.old old_glob && equal_name_global_col u.current new_glob) change_info.unchanged
+
+(* Compares two varinfos of globals. finalizeOnlyExactMatch=true allows to check a rename assumption and discard the comparison result in case they do not match *)
+let eq_glob_var ?(finalizeOnlyExactMatch=false) oV gc_old oldMap nV gc_new newMap change_info final_matches =
+  if already_matched oV nV final_matches then
+    (* check if this function was already matched and lookup the result *)
+    change_info_lookup gc_old gc_new change_info, change_info, final_matches
+  else if not (preservesSameNameMatches oV.vname oldMap nV.vname newMap) then
+    (* do not allow for matches between differently named variables if one of the variables names exists in both, the new and old file *)
+    false, change_info, final_matches
+  else (
+    let identical, (_, function_dependencies, global_var_dependencies, renamesOnSuccess) = eq_varinfo oV nV ~rename_mapping:empty_rename_mapping in
+
+    if not finalizeOnlyExactMatch || identical then
+      performRenames renamesOnSuccess; (* updates enum names and compinfo names and keys that were collected during comparison of this matched function *)
+    if identical then (
+      change_info.unchanged <- {old = gc_old; current = gc_new} :: change_info.unchanged;
+      true, change_info, addToFinalMatchesMapping oV nV final_matches
+    ) else if not finalizeOnlyExactMatch then (
+      change_info.changed <- {old = gc_old; current = gc_new; unchangedHeader = true; diff = None} :: change_info.changed;
+      false, change_info, addToFinalMatchesMapping oV nV final_matches
+    ) else
+      false, change_info, final_matches
+  )
+let compare_varinfo_exact = eq_glob_var ~finalizeOnlyExactMatch:true
+
 (* If some CFGs of the two functions to be compared are provided, a fine-grained CFG comparison is done that also determines which
  * nodes of the function changed. If on the other hand no CFGs are provided, the "old" AST comparison on the CIL.file is
  * used for functions. Then no information is collected regarding which parts/nodes of the function changed. *)
-let eqF (old: Cil.fundec) (current: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) =
-  if should_reanalyze current then
-    ForceReanalyze current, None
-  else
-    (* let unchangedHeader = eq_varinfo old.svar current.svar && GobList.equal eq_varinfo old.sformals current.sformals in *)
-    let emptyRenameMapping = (StringMap.empty, VarinfoMap.empty) in
-
-    (* Compares the two varinfo lists, returning as a first element, if the size of the two lists are equal,
-       and as a second a rename_mapping, holding the rename assumptions *)
-    let rec rename_mapping_aware_compare (alocals: varinfo list) (blocals: varinfo list) (rename_mapping: string StringMap.t) = match alocals, blocals with
-      | [], [] -> true, rename_mapping
-      | origLocal :: als, nowLocal :: bls ->
-        let new_mapping = StringMap.add origLocal.vname nowLocal.vname rename_mapping in
-
-        (*TODO: maybe optimize this with eq_varinfo*)
-        rename_mapping_aware_compare als bls new_mapping
-      | _, _ -> false, rename_mapping
-    in
-
-    let unchangedHeader, headerRenameMapping = match cfgs with
-      | None -> (
-          let headerSizeEqual, headerRenameMapping = rename_mapping_aware_compare old.sformals current.sformals (StringMap.empty) in
-          let actHeaderRenameMapping = (headerRenameMapping, global_rename_mapping) in
-          eq_varinfo old.svar current.svar ~rename_mapping:actHeaderRenameMapping && GobList.equal (eq_varinfo ~rename_mapping:actHeaderRenameMapping) old.sformals current.sformals, headerRenameMapping
-        )
-      | Some _ -> (
-          eq_varinfo old.svar current.svar ~rename_mapping:emptyRenameMapping && GobList.equal (eq_varinfo ~rename_mapping:emptyRenameMapping) old.sformals current.sformals, StringMap.empty
-        )
-    in
-    if not unchangedHeader then ChangedFunHeader current, None
+let eqF (old: Cil.fundec) (current: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) (global_function_rename_mapping: method_rename_assumptions) (global_var_rename_mapping: glob_var_rename_assumptions) =
+  let identical, diffOpt, (_, renamed_method_dependencies, renamed_global_vars_dependencies, renamesOnSuccess) =
+    if should_reanalyze current then
+      ForceReanalyze current, None, empty_rename_mapping
     else
-      (* Here the local variables are checked to be equal *)
-      (*flag: when running on cfg, true iff the locals are identical; on ast: if the size of the locals stayed the same*)
-      let sameLocals, local_rename =
-        match cfgs with
-        | None -> rename_mapping_aware_compare old.slocals current.slocals headerRenameMapping
-        | Some _ -> GobList.equal (eq_varinfo ~rename_mapping:emptyRenameMapping) old.slocals current.slocals, StringMap.empty
-      in
-      let rename_mapping: rename_mapping = (local_rename, global_rename_mapping) in
-
-      if not sameLocals then
-        (Changed, None)
+
+      let add_locals_to_rename_mapping la lb map =
+        try
+          List.fold_left2 (fun map a b -> StringMap.add a.vname b.vname map) map la lb
+        with Invalid_argument _ -> map in
+
+      let parameterMapping = add_locals_to_rename_mapping old.sformals current.sformals StringMap.empty in
+      let renameMapping = (parameterMapping, global_function_rename_mapping, global_var_rename_mapping, ([], [])) in
+
+      (* compare the function header based on the collected rename assumptions for parameters *)
+      let unchangedHeader, renameMapping = eq_varinfo old.svar current.svar ~rename_mapping:renameMapping
+                                           &&>> forward_list_equal eq_varinfo old.sformals current.sformals in
+
+      if not unchangedHeader then ChangedFunHeader current, None, empty_rename_mapping
       else
-        match cfgs with
-        | None -> unchanged_to_change_status (eq_block (old.sbody, old) (current.sbody, current) ~rename_mapping), None
-        | Some (cfgOld, (cfgNew, cfgNewBack)) ->
-          let module CfgOld : MyCFG.CfgForward = struct let next = cfgOld end in
-          let module CfgNew : MyCFG.CfgBidir = struct let prev = cfgNewBack let next = cfgNew end in
-          let matches, diffNodes1 = compareFun (module CfgOld) (module CfgNew) old current in
-          if diffNodes1 = [] then (Unchanged, None)
-          else (Changed, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1})
-
-let eq_glob (old: global_col) (current: global_col) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) =
-  match old.def, current.def with
-  | Some (Var x), Some (Var y) -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None (* ignore the init_info - a changed init of a global will lead to a different start state *)
-  | Some (Fun f), Some (Fun g) -> eqF f g cfgs global_rename_mapping
-  | None, None -> (match old.decls, current.decls with
-      | Some x, Some y -> unchanged_to_change_status (eq_varinfo x y ~rename_mapping:(StringMap.empty, VarinfoMap.empty)), None
-      | _, _ -> failwith "should never collect any empty entries in GlobalMap")
-  | _, _ -> Changed, None (* it is considered to be changed (not added or removed) because a global collection only exists in the map
-                             if there is at least one declaration or definition for this global *)
+        (* include matching of local variables into rename mapping *)
+        let renameMapping = match renameMapping with
+          | (pm, gf, gv, re) -> (add_locals_to_rename_mapping old.slocals current.slocals pm, gf, gv, re) in
+        let sameLocals, renameMapping = forward_list_equal eq_varinfo old.slocals current.slocals ~rename_mapping:renameMapping in
+
+        if not sameLocals then
+          (Changed, None, empty_rename_mapping)
+        else
+          match cfgs with
+          | None ->
+            let (identical, new_rename_mapping) = eq_block (old.sbody, old) (current.sbody, current) ~rename_mapping:renameMapping in
+            unchanged_to_change_status identical, None, new_rename_mapping
+          | Some (cfgOld, (cfgNew, cfgNewBack)) ->
+            let module CfgOld : MyCFG.CfgForward = struct let next = cfgOld end in
+            let module CfgNew : MyCFG.CfgBidir = struct let prev = cfgNewBack let next = cfgNew end in
+            let matches, diffNodes1, updated_rename_mapping = compareFun (module CfgOld) (module CfgNew) old current renameMapping in
+            if diffNodes1 = [] then (Unchanged, None, updated_rename_mapping)
+            else (Changed, Some {unchangedNodes = matches; primObsoleteNodes = diffNodes1}, updated_rename_mapping)
+  in
+  identical, diffOpt, renamed_method_dependencies, renamed_global_vars_dependencies, renamesOnSuccess
+
+let eqF_only_consider_exact_match gc_old gc_new change_info final_matches oldMap newMap =
+  match gc_old.def, gc_new.def with
+  | None, None -> (
+      match gc_old.decls, gc_new.decls with
+      | Some old_var, Some new_var ->
+        compare_varinfo_exact old_var gc_old oldMap new_var gc_new newMap change_info final_matches
+      | _ -> failwith "A global collection should never be empty")
+  | Some (Fun f1), Some (Fun f2) -> (
+      if already_matched f1.svar f2.svar final_matches then
+        (* check if this function was already matched and lookup the result *)
+        change_info_lookup gc_old gc_new change_info, change_info, final_matches
+      else if not (preservesSameNameMatches f1.svar.vname oldMap f2.svar.vname newMap) then
+        (* check that names of match are each only contained in new or old file *)
+        false, change_info, final_matches
+      else
+        (* the exact comparison is always uses the AST comparison because only when unchanged this match is manifested *)
+        let doMatch, diff, fun_deps, global_deps, renamesOnSuccess = eqF f1 f2 None VarinfoMap.empty VarinfoMap.empty in
+        match doMatch with
+        | Unchanged when empty_rename_assms (VarinfoMap.filter (fun vo vn -> not (vo.vname = f1.svar.vname && vn.vname = f2.svar.vname)) fun_deps) && empty_rename_assms global_deps ->
+          performRenames renamesOnSuccess;
+          change_info.unchanged <- {old = gc_old; current = gc_new} :: change_info.unchanged;
+          let final_matches = addToFinalMatchesMapping f1.svar f2.svar final_matches in
+          true, change_info, final_matches
+        | Unchanged -> false, change_info, final_matches
+        | Changed -> false, change_info, final_matches
+        | ChangedFunHeader _ -> false, change_info, final_matches
+        | ForceReanalyze _ -> false, change_info, final_matches)
+  | _, _ -> false, change_info, final_matches
+
+let eqF_check_contained_renames ~renameDetection f1 f2 oldMap newMap cfgs gc_old gc_new (change_info, final_matches) =
+  let doMatch, diff, function_dependencies, global_var_dependencies, renamesOnSuccess = eqF f1 f2 cfgs VarinfoMap.empty VarinfoMap.empty in
+  performRenames renamesOnSuccess; (* updates enum names and compinfo names and keys that were collected during comparison of this matched function *)
+
+  (* for rename detection, check whether the rename assumptions collected during the function comparison actually match exactly,
+     otherwise check that the function comparison was successful without collecting any rename assumptions *)
+  let dependenciesMatch, change_info, final_matches =
+    if renameDetection then
+      let extract_globs _ gc map =
+        let v = get_varinfo gc in
+        VarinfoMap.add v gc map in
+      let var_glob_old = GlobalMap.fold extract_globs oldMap VarinfoMap.empty in
+      let var_glob_new = GlobalMap.fold extract_globs newMap VarinfoMap.empty in
+      let funDependenciesMatch, change_info, final_matches = VarinfoMap.fold (fun f_old_var f_new_var (acc, ci, fm) ->
+          let gc_old = VarinfoMap.find f_old_var var_glob_old in
+          let gc_new = VarinfoMap.find f_new_var var_glob_new in
+          if acc then
+            eqF_only_consider_exact_match gc_old gc_new ci fm oldMap newMap
+          else false, ci, fm
+        ) function_dependencies (true, change_info, final_matches) in
+      let globalDependenciesMatch, change_info, final_matches = VarinfoMap.fold (fun old_var new_var (acc, ci, fm) ->
+          let glob_old = VarinfoMap.find old_var var_glob_old in
+          let glob_new = VarinfoMap.find new_var var_glob_new in
+          if acc then
+            compare_varinfo_exact old_var glob_old oldMap new_var glob_new newMap ci fm
+          else false, ci, fm
+        ) global_var_dependencies (true, change_info, final_matches) in
+      funDependenciesMatch && globalDependenciesMatch, change_info, final_matches
+    else
+      empty_rename_assms function_dependencies && empty_rename_assms global_var_dependencies, change_info, final_matches in
+
+  let append_to_changed ~unchangedHeader ~diff =
+    change_info.changed <- {current = gc_new; old = gc_old; unchangedHeader; diff} :: change_info.changed
+  in
+  (match doMatch with
+   | Unchanged when dependenciesMatch ->
+     change_info.unchanged <- {old = gc_old; current = gc_new} :: change_info.unchanged
+   | Unchanged ->
+     (* no diff is stored, also when comparing functions based on CFG because currently there is no mechanism to detect which part was affected by the *)
+     append_to_changed ~unchangedHeader:true ~diff:None
+   | Changed -> append_to_changed ~unchangedHeader:true ~diff:diff
+   | _ -> (* this can only be ForceReanalyze or ChangedFunHeader *)
+     change_info.exclude_from_rel_destab <- VarinfoSet.add f1.svar change_info.exclude_from_rel_destab;
+     append_to_changed ~unchangedHeader:false ~diff:None);
+  change_info, addToFinalMatchesMapping f1.svar f2.svar final_matches
+
+let eq_glob ?(matchVars=true) ?(matchFuns=true) ?(renameDetection=false) oldMap newMap cfgs gc_old gc_new (change_info, final_matches) =
+  match gc_old.def, gc_new.def with
+  | Some (Var v1), Some (Var v2) when matchVars -> let _, ci, fm = eq_glob_var v1 gc_old oldMap v2 gc_new newMap change_info final_matches in ci, fm
+  | Some (Fun f1), Some (Fun f2) when matchFuns ->
+    eqF_check_contained_renames ~renameDetection f1 f2 oldMap newMap cfgs gc_old gc_new (change_info, final_matches)
+  | None, None -> (match gc_old.decls, gc_new.decls with
+      | Some v1, Some v2 when matchVars -> let _, ci, fm = eq_glob_var v1 gc_old oldMap v2 gc_new newMap change_info final_matches in ci, fm
+      | _ -> change_info, final_matches (* a global collection should never be empty *))
+  (* Without rename detection a global definition or declaration that does not have respective counterpart in the other version is considered to be changed (not added or removed)
+     because a global collection only exists in the map if there is at least one declaration or definition for this global.
+     For the rename detection they can only be added to changed when the according flag is set, because there would be duplicates when iterating over the globals several times. *)
+  | Some (Var _), None
+  | None, Some (Var _) -> if matchVars then (
+      change_info.changed <- {old = gc_old; current = gc_new; diff = None; unchangedHeader = true} :: change_info.changed;
+      change_info, addToFinalMatchesMapping (get_varinfo gc_old) (get_varinfo gc_new) final_matches)
+    else
+      change_info, final_matches
+  | _, _ -> if matchVars && matchFuns then (
+      change_info.changed <- {old = gc_old; current = gc_new; diff = None; unchangedHeader = true} :: change_info.changed;
+      change_info, addToFinalMatchesMapping (get_varinfo gc_old) (get_varinfo gc_new) final_matches)
+    else
+      change_info, final_matches
+
+let addNewGlobals name gc_new (change_info, final_matches) =
+  if not (VarinfoMap.mem (get_varinfo gc_new) (snd final_matches)) then
+    change_info.added <- gc_new :: change_info.added;
+  (change_info, final_matches)
+
+let addOldGlobals name gc_old (change_info, final_matches) =
+  if not (VarinfoMap.mem (get_varinfo gc_old) (fst final_matches)) then
+    change_info.removed <- gc_old :: change_info.removed;
+  (change_info, final_matches)
 
 let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
   let cfgs = if GobConfig.get_string "incremental.compare" = "cfg"
     then Some Batteries.(CfgTools.getCFG oldAST |> Tuple3.first, CfgTools.getCFG newAST |> Tuple3.get12)
     else None in
 
-  let addGlobal map global  =
+  let addGlobal map global =
     try
       let name, col = match global with
         | GVar (v,_,_) -> v.vname, {decls = None; def = Some (Var v)}
@@ -150,63 +310,38 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
       Not_found -> map
   in
 
-  (* Store a map from functionNames in the old file to the function definition*)
+  (* Store a map from global names in the old file to the globals declarations and/or definition *)
   let oldMap = Cil.foldGlobals oldAST addGlobal GlobalMap.empty in
   let newMap = Cil.foldGlobals newAST addGlobal GlobalMap.empty in
 
-  let generate_global_rename_mapping name current_global =
-    try
-      let old_global = GlobalMap.find name oldMap in
-      match old_global.def, current_global.def with
-      | Some (Fun f1), Some (Fun f2) ->
-        let renamed_params: string StringMap.t = if List.compare_lengths f1.sformals f2.sformals = 0 then
-            let mappings = List.combine f1.sformals f2.sformals |>
-                           List.filter (fun (original, now) -> not (original.vname = now.vname)) |>
-                           List.map (fun (original, now) -> (original.vname, now.vname)) |>
-                           List.to_seq
-            in
-            StringMap.add_seq mappings StringMap.empty
-          else StringMap.empty in
-        if not (f1.svar.vname = f2.svar.vname) || (StringMap.cardinal renamed_params) > 0 then
-          Some (f1.svar, {original_method_name = f1.svar.vname; new_method_name = f2.svar.vname; parameter_renames = renamed_params})
-        else None
-      | _, _ -> None
-    with Not_found -> None
-  in
-
-  let global_rename_mapping: method_rename_assumptions = GlobalMap.fold (fun name global_col current_global_rename_mapping ->
-      match generate_global_rename_mapping name global_col with
-      | Some (funVar, rename_mapping) -> VarinfoMap.add funVar rename_mapping current_global_rename_mapping
-      | None -> current_global_rename_mapping
-    ) newMap VarinfoMap.empty in
-
   let changes = empty_change_info () in
   global_typ_acc := [];
-  let findChanges map name current_global global_rename_mapping =
+
+  let findChanges ?(matchVars=true) ?(matchFuns=true) ?(renameDetection=false) oldMap newMap cfgs name gc_new (change_info, final_matches) =
     try
-      let old_global = GlobalMap.find name map in
-      (* Do a (recursive) equal comparison ignoring location information *)
-      let change_status, diff = eq old_global current_global cfgs global_rename_mapping in
-      let append_to_changed ~unchangedHeader =
-        changes.changed <- {current = current_global; old = old_global; unchangedHeader; diff} :: changes.changed
-      in
-      match change_status with
-      | Changed ->
-        append_to_changed ~unchangedHeader:true
-      | Unchanged -> changes.unchanged <- {current = current_global; old = old_global} :: changes.unchanged
-      | ChangedFunHeader f
-      | ForceReanalyze f ->
-        changes.exclude_from_rel_destab <- VarinfoSet.add f.svar changes.exclude_from_rel_destab;
-        append_to_changed ~unchangedHeader:false;
-    with Not_found -> changes.added <- current_global::changes.added (* Global could not be found in old map -> added *)
-  in
+      let gc_old = GlobalMap.find name oldMap in
+      eq ~matchVars ~matchFuns ~renameDetection oldMap newMap cfgs gc_old gc_new (change_info, final_matches)
+    with Not_found ->
+      if not renameDetection then
+        change_info.added <- gc_new::change_info.added; (* Global could not be found in old map -> added *)
+      change_info, final_matches in
 
-  (*  For each function in the new file, check whether a function with the same name
-      already existed in the old version, and whether it is the same function. *)
-  GlobalMap.iter (fun name glob_col -> findChanges oldMap name glob_col global_rename_mapping) newMap;
+  if GobConfig.get_bool "incremental.detect-renames" then (
+    let _ =
+      (changes, (VarinfoMap.empty, VarinfoMap.empty)) (* change_info and final_matches (bi-directional) is propagated *)
+      |> GlobalMap.fold (findChanges ~matchVars:true ~matchFuns:false ~renameDetection:true oldMap newMap cfgs) newMap
+      |> GlobalMap.fold (findChanges ~matchVars:false ~matchFuns:true ~renameDetection:true oldMap newMap cfgs) newMap
+      |> GlobalMap.fold addNewGlobals newMap
+      |> GlobalMap.fold addOldGlobals oldMap in
 
-  (* We check whether functions have been added or removed *)
-  GlobalMap.iter (fun name glob -> if not (GlobalMap.mem name newMap) then changes.removed <- (glob::changes.removed)) oldMap;
+    ()
+  ) else (
+    let _ =
+      (changes, (VarinfoMap.empty, VarinfoMap.empty)) (* change_info and final_matches (bi-directional) is propagated *)
+      |> GlobalMap.fold (findChanges oldMap newMap cfgs) newMap
+      |> GlobalMap.fold addOldGlobals oldMap in
+    ()
+  );
   changes
 
 (** Given an (optional) equality function between [Cil.global]s, an old and a new [Cil.file], this function computes a [change_info],
diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml
index 2f9628b4c1..474254872d 100644
--- a/src/incremental/updateCil.ml
+++ b/src/incremental/updateCil.ml
@@ -32,6 +32,7 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
     target.svar <- src.svar;
   in
   let reset_fun (f: fundec) (old_f: fundec) =
+    old_f.svar.vname <- f.svar.vname;
     f.svar.vid <- old_f.svar.vid;
     List.iter2 (fun l o_l -> l.vid <- o_l.vid; o_l.vname <- l.vname) f.slocals old_f.slocals;
     List.iter2 (fun lo o_f -> lo.vid <- o_f.vid; o_f.vname <- lo.vname) f.sformals old_f.sformals;
@@ -48,6 +49,7 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
   in
   let reset_var (v: varinfo) (old_v: varinfo)=
     v.vid <- old_v.vid;
+    old_v.vname <- v.vname;
     update_vid_max v.vid;
   in
   let reset_globals (glob: unchanged_global) =
diff --git a/src/util/cilMaps.ml b/src/util/cilMaps.ml
index 9b3b91f5c6..2706d8252b 100644
--- a/src/util/cilMaps.ml
+++ b/src/util/cilMaps.ml
@@ -1,5 +1,14 @@
 open GoblintCil
 
+module FundecForMap = struct
+  type t = Cil.fundec
+
+  (*x.svar.uid cannot be used, as they may overlap between old and now AST*)
+  let compare x y = String.compare x.svar.vname y.svar.vname
+end
+
+module FundecMap = Map.Make(FundecForMap)
+
 module VarinfoOrdered = struct
   type t = varinfo
 
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 2ff2e8bf58..c5e255aa02 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1138,6 +1138,12 @@
           "enum": ["ast", "cfg"],
           "default": "ast"
         },
+        "detect-renames": {
+          "title": "incremental.detect-renames",
+          "description": "If Goblint should try to detect renamed local variables, function parameters, functions and global variables",
+          "type":"boolean",
+          "default": true
+        },
         "force-reanalyze": {
           "title": "incremental.force-reanalyze",
           "type": "object",
diff --git a/src/util/server.ml b/src/util/server.ml
index ba58fbd032..97691bb1c3 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -207,9 +207,11 @@ let reparse (s: t) =
 
 (* Only called when the file has not been reparsed, so we can skip the expensive CFG comparison. *)
 let virtual_changes file =
-  let eq (glob: CompareCIL.global_col) _ _ _ = match glob.def with
-    | Some (Fun fdec) when CompareCIL.should_reanalyze fdec -> CompareCIL.ForceReanalyze fdec, None
-    | _ -> Unchanged, None
+  let eq ?(matchVars=true) ?(matchFuns=true) ?(renameDetection=false) _ _ _ gc_old (gc_new: CompareCIL.global_col) ((change_info : CompareCIL.change_info), final_matches) = (match gc_new.def with
+      | Some (Fun fdec) when CompareCIL.should_reanalyze fdec ->
+        change_info.exclude_from_rel_destab <- CompareCIL.VarinfoSet.add fdec.svar change_info.exclude_from_rel_destab
+      | _ -> change_info.unchanged <- {old = gc_old; current= gc_new} :: change_info.unchanged);
+    change_info, final_matches
   in
   CompareCIL.compareCilFiles ~eq file file
 
diff --git a/tests/incremental/04-var-rename/02-rename_and_shuffle.c b/tests/incremental/04-var-rename/01-rename_and_shuffle.c
similarity index 58%
rename from tests/incremental/04-var-rename/02-rename_and_shuffle.c
rename to tests/incremental/04-var-rename/01-rename_and_shuffle.c
index 9917738055..7d6ea81e6f 100644
--- a/tests/incremental/04-var-rename/02-rename_and_shuffle.c
+++ b/tests/incremental/04-var-rename/01-rename_and_shuffle.c
@@ -1,6 +1,6 @@
 #include<stdio.h>
 
-//a is renamed to c, but the usage of a is replaced by b
+// a is renamed to c, but the usage of a is replaced by b (semantic changes)
 int main() {
     int a = 0;
     int b = 1;
diff --git a/tests/incremental/04-var-rename/01-unused_rename.json b/tests/incremental/04-var-rename/01-rename_and_shuffle.json
similarity index 100%
rename from tests/incremental/04-var-rename/01-unused_rename.json
rename to tests/incremental/04-var-rename/01-rename_and_shuffle.json
diff --git a/tests/incremental/04-var-rename/01-rename_and_shuffle.patch b/tests/incremental/04-var-rename/01-rename_and_shuffle.patch
new file mode 100644
index 0000000000..94e27d9a80
--- /dev/null
+++ b/tests/incremental/04-var-rename/01-rename_and_shuffle.patch
@@ -0,0 +1,15 @@
+--- tests/incremental/04-var-rename/01-rename_and_shuffle.c
++++ tests/incremental/04-var-rename/01-rename_and_shuffle.c
+@@ -2,10 +2,10 @@
+
+ // a is renamed to c, but the usage of a is replaced by b (semantic changes)
+ int main() {
+-    int a = 0;
++    int c = 0;
+     int b = 1;
+
+-    printf("Print %d", a);
++    printf("Print %d", b);
+
+     return 0;
+ }
diff --git a/tests/incremental/04-var-rename/01-rename_and_shuffle.t b/tests/incremental/04-var-rename/01-rename_and_shuffle.t
new file mode 100644
index 0000000000..8f3b57f797
--- /dev/null
+++ b/tests/incremental/04-var-rename/01-rename_and_shuffle.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 01-rename_and_shuffle.json --enable incremental.save 01-rename_and_shuffle.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 01-rename_and_shuffle.c
+  $ patch -b <01-rename_and_shuffle.patch
+  patching file 01-rename_and_shuffle.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 01-rename_and_shuffle.json --enable incremental.load 01-rename_and_shuffle.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 1 (with unchangedHeader = 1); added = 0; removed = 0
diff --git a/tests/incremental/04-var-rename/01-unused_rename.c b/tests/incremental/04-var-rename/01-unused_rename.c
deleted file mode 100644
index 31eacd5bf9..0000000000
--- a/tests/incremental/04-var-rename/01-unused_rename.c
+++ /dev/null
@@ -1,4 +0,0 @@
-int main() {
-    int a = 0;
-    return 0;
-}
diff --git a/tests/incremental/04-var-rename/01-unused_rename.patch b/tests/incremental/04-var-rename/01-unused_rename.patch
deleted file mode 100644
index 977470ad53..0000000000
--- a/tests/incremental/04-var-rename/01-unused_rename.patch
+++ /dev/null
@@ -1,8 +0,0 @@
---- tests/incremental/04-var-rename/01-unused_rename.c
-+++ tests/incremental/04-var-rename/01-unused_rename.c
-@@ -1,4 +1,4 @@
- int main() {
--    int a = 0;
-+    int b = 0;
-     return 0;
- }
diff --git a/tests/incremental/04-var-rename/01-unused_rename.txt b/tests/incremental/04-var-rename/01-unused_rename.txt
deleted file mode 100644
index a317916ad1..0000000000
--- a/tests/incremental/04-var-rename/01-unused_rename.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-local variable a is renamed to b.
-a/b is not used.
-No semantic changes.
diff --git a/tests/incremental/04-var-rename/02-rename_and_shuffle.patch b/tests/incremental/04-var-rename/02-rename_and_shuffle.patch
deleted file mode 100644
index 5c1dc4785e..0000000000
--- a/tests/incremental/04-var-rename/02-rename_and_shuffle.patch
+++ /dev/null
@@ -1,15 +0,0 @@
---- tests/incremental/04-var-rename/02-rename_and_shuffle.c
-+++ tests/incremental/04-var-rename/02-rename_and_shuffle.c
-@@ -2,10 +2,10 @@
- 
- //a is renamed to c, but the usage of a is replaced by b
- int main() {
--    int a = 0;
-+    int c = 0;
-     int b = 1;
- 
--    printf("Print %d", a);
-+    printf("Print %d", b);
- 
-     return 0;
- }
diff --git a/tests/incremental/04-var-rename/02-rename_and_shuffle.txt b/tests/incremental/04-var-rename/02-rename_and_shuffle.txt
deleted file mode 100644
index 8c0ab5ac05..0000000000
--- a/tests/incremental/04-var-rename/02-rename_and_shuffle.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-a is renamed to c, but the usage of a is replaced by b.
-Semantic changes.
diff --git a/tests/incremental/04-var-rename/03-rename_with_usage.c b/tests/incremental/04-var-rename/02-rename_with_usage.c
similarity index 100%
rename from tests/incremental/04-var-rename/03-rename_with_usage.c
rename to tests/incremental/04-var-rename/02-rename_with_usage.c
diff --git a/tests/incremental/04-var-rename/02-rename_and_shuffle.json b/tests/incremental/04-var-rename/02-rename_with_usage.json
similarity index 100%
rename from tests/incremental/04-var-rename/02-rename_and_shuffle.json
rename to tests/incremental/04-var-rename/02-rename_with_usage.json
diff --git a/tests/incremental/04-var-rename/03-rename_with_usage.patch b/tests/incremental/04-var-rename/02-rename_with_usage.patch
similarity index 62%
rename from tests/incremental/04-var-rename/03-rename_with_usage.patch
rename to tests/incremental/04-var-rename/02-rename_with_usage.patch
index 26fb98b340..6cfe41bbb1 100644
--- a/tests/incremental/04-var-rename/03-rename_with_usage.patch
+++ b/tests/incremental/04-var-rename/02-rename_with_usage.patch
@@ -1,15 +1,15 @@
---- tests/incremental/04-var-rename/03-rename_with_usage.c
-+++ tests/incremental/04-var-rename/03-rename_with_usage.c
+--- tests/incremental/04-var-rename/02-rename_with_usage.c
++++ tests/incremental/04-var-rename/02-rename_with_usage.c
 @@ -2,10 +2,10 @@
- 
+
  //a is renamed to c, but its usages stay the same
  int main() {
 -    int a = 0;
 +    int c = 0;
      int b = 1;
- 
+
 -    printf("Print %d", a);
 +    printf("Print %d", c);
- 
+
      return 0;
  }
diff --git a/tests/incremental/04-var-rename/02-rename_with_usage.t b/tests/incremental/04-var-rename/02-rename_with_usage.t
new file mode 100644
index 0000000000..1e2818ed4d
--- /dev/null
+++ b/tests/incremental/04-var-rename/02-rename_with_usage.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 02-rename_with_usage.json --enable incremental.save 02-rename_with_usage.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 02-rename_with_usage.c
+  $ patch -b <02-rename_with_usage.patch
+  patching file 02-rename_with_usage.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 02-rename_with_usage.json --enable incremental.load 02-rename_with_usage.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 0 (with unchangedHeader = 0); added = 0; removed = 0
diff --git a/tests/incremental/04-var-rename/03-rename_with_usage.txt b/tests/incremental/04-var-rename/03-rename_with_usage.txt
deleted file mode 100644
index 18ff7e94d4..0000000000
--- a/tests/incremental/04-var-rename/03-rename_with_usage.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-a is renamed to c, but the usage stays the same.
-No semantic changes.
diff --git a/tests/incremental/04-var-rename/04-renamed_assert.c b/tests/incremental/04-var-rename/03-renamed_assert.c
similarity index 62%
rename from tests/incremental/04-var-rename/04-renamed_assert.c
rename to tests/incremental/04-var-rename/03-renamed_assert.c
index 665e44251c..b9f484ba01 100644
--- a/tests/incremental/04-var-rename/04-renamed_assert.c
+++ b/tests/incremental/04-var-rename/03-renamed_assert.c
@@ -1,9 +1,10 @@
 #include <goblint.h>
 
+// local var used in assert is renamed (no semantic changes)
 int main() {
     int myVar = 0;
 
     __goblint_check(myVar < 11);
 
     return 0;
-}
\ No newline at end of file
+}
diff --git a/tests/incremental/04-var-rename/03-rename_with_usage.json b/tests/incremental/04-var-rename/03-renamed_assert.json
similarity index 100%
rename from tests/incremental/04-var-rename/03-rename_with_usage.json
rename to tests/incremental/04-var-rename/03-renamed_assert.json
diff --git a/tests/incremental/04-var-rename/04-renamed_assert.patch b/tests/incremental/04-var-rename/03-renamed_assert.patch
similarity index 64%
rename from tests/incremental/04-var-rename/04-renamed_assert.patch
rename to tests/incremental/04-var-rename/03-renamed_assert.patch
index d7dfe6ae8e..c672e68044 100644
--- a/tests/incremental/04-var-rename/04-renamed_assert.patch
+++ b/tests/incremental/04-var-rename/03-renamed_assert.patch
@@ -1,5 +1,5 @@
---- tests/incremental/04-var-rename/04-renamed_assert.c
-+++ tests/incremental/04-var-rename/04-renamed_assert.c
+--- tests/incremental/04-var-rename/03-renamed_assert.c
++++ tests/incremental/04-var-rename/03-renamed_assert.c
 @@ -1,7 +1,7 @@
  int main() {
 -    int myVar = 0;
diff --git a/tests/incremental/04-var-rename/04-renamed_assert.txt b/tests/incremental/04-var-rename/04-renamed_assert.txt
deleted file mode 100644
index 1afc289347..0000000000
--- a/tests/incremental/04-var-rename/04-renamed_assert.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-local var used in assert is renamed.
-No semantic changes.
diff --git a/tests/incremental/04-var-rename/05-renamed_param.c b/tests/incremental/04-var-rename/04-renamed_param.c
similarity index 60%
rename from tests/incremental/04-var-rename/05-renamed_param.c
rename to tests/incremental/04-var-rename/04-renamed_param.c
index 72fdfaf0e9..770af2683c 100644
--- a/tests/incremental/04-var-rename/05-renamed_param.c
+++ b/tests/incremental/04-var-rename/04-renamed_param.c
@@ -1,3 +1,4 @@
+// function param is renamed (no semantic changes)
 void method(int a) {
     int c = a;
 }
@@ -5,4 +6,4 @@ void method(int a) {
 int main() {
     method(0);
     return 0;
-}
\ No newline at end of file
+}
diff --git a/tests/incremental/04-var-rename/04-renamed_assert.json b/tests/incremental/04-var-rename/04-renamed_param.json
similarity index 100%
rename from tests/incremental/04-var-rename/04-renamed_assert.json
rename to tests/incremental/04-var-rename/04-renamed_param.json
diff --git a/tests/incremental/04-var-rename/04-renamed_param.patch b/tests/incremental/04-var-rename/04-renamed_param.patch
new file mode 100644
index 0000000000..50a9b69f6a
--- /dev/null
+++ b/tests/incremental/04-var-rename/04-renamed_param.patch
@@ -0,0 +1,10 @@
+--- tests/incremental/04-var-rename/04-renamed_param.c
++++ tests/incremental/04-var-rename/04-renamed_param.c
+@@ -2,5 +2,5 @@
+-void method(int a) {
+-    int c = a;
++void method(int b) {
++    int c = b;
+ }
+
+ int main() {
diff --git a/tests/incremental/04-var-rename/04-renamed_param.t b/tests/incremental/04-var-rename/04-renamed_param.t
new file mode 100644
index 0000000000..9da6d5e888
--- /dev/null
+++ b/tests/incremental/04-var-rename/04-renamed_param.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 04-renamed_param.json --enable incremental.save 04-renamed_param.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 04-renamed_param.c
+  $ patch -b <04-renamed_param.patch
+  patching file 04-renamed_param.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 04-renamed_param.json --enable incremental.load 04-renamed_param.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 0 (with unchangedHeader = 0); added = 0; removed = 0
diff --git a/tests/incremental/04-var-rename/05-renamed_param.patch b/tests/incremental/04-var-rename/05-renamed_param.patch
deleted file mode 100644
index 944566b05c..0000000000
--- a/tests/incremental/04-var-rename/05-renamed_param.patch
+++ /dev/null
@@ -1,10 +0,0 @@
---- tests/incremental/04-var-rename/05-renamed_param.c
-+++ tests/incremental/04-var-rename/05-renamed_param.c
-@@ -1,5 +1,5 @@
--void method(int a) {
--    int c = a;
-+void method(int b) {
-+    int c = b;
- }
- 
- int main() {
diff --git a/tests/incremental/04-var-rename/05-renamed_param.txt b/tests/incremental/04-var-rename/05-renamed_param.txt
deleted file mode 100644
index 09bca47979..0000000000
--- a/tests/incremental/04-var-rename/05-renamed_param.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-Function param is renamed.
-No semantic changes.
diff --git a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.c b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.c
similarity index 100%
rename from tests/incremental/04-var-rename/06-renamed_param_usage_changed.c
rename to tests/incremental/04-var-rename/05-renamed_param_usage_changed.c
diff --git a/tests/incremental/04-var-rename/05-renamed_param.json b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.json
similarity index 100%
rename from tests/incremental/04-var-rename/05-renamed_param.json
rename to tests/incremental/04-var-rename/05-renamed_param_usage_changed.json
diff --git a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.patch b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.patch
similarity index 55%
rename from tests/incremental/04-var-rename/06-renamed_param_usage_changed.patch
rename to tests/incremental/04-var-rename/05-renamed_param_usage_changed.patch
index a93e45c4c5..9ffc2c1cea 100644
--- a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.patch
+++ b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.patch
@@ -1,8 +1,8 @@
---- tests/incremental/04-var-rename/06-renamed_param_usage_changed.c
-+++ tests/incremental/04-var-rename/06-renamed_param_usage_changed.c
+--- tests/incremental/04-var-rename/05-renamed_param_usage_changed.c
++++ tests/incremental/04-var-rename/05-renamed_param_usage_changed.c
 @@ -1,6 +1,6 @@
  //This test should mark foo and main as changed
- 
+
 -void foo(int a, int b) {
 +void foo(int b, int a) {
      int x = a;
diff --git a/tests/incremental/04-var-rename/05-renamed_param_usage_changed.t b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.t
new file mode 100644
index 0000000000..a465b2b6f2
--- /dev/null
+++ b/tests/incremental/04-var-rename/05-renamed_param_usage_changed.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 05-renamed_param_usage_changed.json --enable incremental.save 05-renamed_param_usage_changed.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 05-renamed_param_usage_changed.c
+  $ patch -b <05-renamed_param_usage_changed.patch
+  patching file 05-renamed_param_usage_changed.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 05-renamed_param_usage_changed.json --enable incremental.load 05-renamed_param_usage_changed.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 1 (with unchangedHeader = 1); added = 0; removed = 0
diff --git a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.json b/tests/incremental/04-var-rename/06-renamed_param_usage_changed.json
deleted file mode 100644
index 544b7b4ddd..0000000000
--- a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.json
+++ /dev/null
@@ -1,3 +0,0 @@
-{
-    
-}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.txt b/tests/incremental/04-var-rename/06-renamed_param_usage_changed.txt
deleted file mode 100644
index 0dc90594c7..0000000000
--- a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-function parameters a and b and swapped in the function header. But the function body stays the same.
-Semantic changes.
diff --git a/tests/incremental/04-var-rename/dune b/tests/incremental/04-var-rename/dune
new file mode 100644
index 0000000000..1b37756f98
--- /dev/null
+++ b/tests/incremental/04-var-rename/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.{c,json,patch}) (sandbox preserve_file_kind)))
diff --git a/tests/incremental/05-method-rename/00-simple_rename.c b/tests/incremental/05-method-rename/00-simple_rename.c
new file mode 100644
index 0000000000..5d1e6fe872
--- /dev/null
+++ b/tests/incremental/05-method-rename/00-simple_rename.c
@@ -0,0 +1,10 @@
+#include<stdio.h>
+
+void foo() {
+    printf("foo");
+}
+
+int main() {
+    foo();
+    return 0;
+}
diff --git a/tests/incremental/05-method-rename/00-simple_rename.json b/tests/incremental/05-method-rename/00-simple_rename.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/05-method-rename/00-simple_rename.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/05-method-rename/00-simple_rename.patch b/tests/incremental/05-method-rename/00-simple_rename.patch
new file mode 100644
index 0000000000..ed7b40014c
--- /dev/null
+++ b/tests/incremental/05-method-rename/00-simple_rename.patch
@@ -0,0 +1,15 @@
+--- tests/incremental/05-method-rename/00-simple_rename.c
++++ tests/incremental/05-method-rename/00-simple_rename.c
+@@ -1,10 +1,10 @@
+ #include<stdio.h>
+
+-void foo() {
++void bar() {
+     printf("foo");
+ }
+
+ int main() {
+-    foo();
++    bar();
+     return 0;
+ }
diff --git a/tests/incremental/05-method-rename/00-simple_rename.t b/tests/incremental/05-method-rename/00-simple_rename.t
new file mode 100644
index 0000000000..1855b903eb
--- /dev/null
+++ b/tests/incremental/05-method-rename/00-simple_rename.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 00-simple_rename.json --enable incremental.save 00-simple_rename.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 00-simple_rename.c
+  $ patch -b <00-simple_rename.patch
+  patching file 00-simple_rename.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 00-simple_rename.json --enable incremental.load 00-simple_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 0 (with unchangedHeader = 0); added = 0; removed = 0
diff --git a/tests/incremental/05-method-rename/01-dependent_rename.c b/tests/incremental/05-method-rename/01-dependent_rename.c
new file mode 100644
index 0000000000..66c1a5a634
--- /dev/null
+++ b/tests/incremental/05-method-rename/01-dependent_rename.c
@@ -0,0 +1,14 @@
+#include<stdio.h>
+
+void fun1() {
+    printf("fun1");
+}
+
+void fun2() {
+    fun1();
+}
+
+int main() {
+    fun2();
+    return 0;
+}
diff --git a/tests/incremental/05-method-rename/01-dependent_rename.json b/tests/incremental/05-method-rename/01-dependent_rename.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/05-method-rename/01-dependent_rename.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/05-method-rename/01-dependent_rename.patch b/tests/incremental/05-method-rename/01-dependent_rename.patch
new file mode 100644
index 0000000000..f3a4a9a3f8
--- /dev/null
+++ b/tests/incremental/05-method-rename/01-dependent_rename.patch
@@ -0,0 +1,21 @@
+--- tests/incremental/05-method-rename/01-dependent_rename.c
++++ tests/incremental/05-method-rename/01-dependent_rename.c
+@@ -1,14 +1,14 @@
+ #include<stdio.h>
+
+-void fun1() {
++void bar1() {
+     printf("fun1");
+ }
+
+-void fun2() {
+-    fun1();
++void bar2() {
++    bar1();
+ }
+
+ int main() {
+-    fun2();
++    bar2();
+     return 0;
+ }
diff --git a/tests/incremental/05-method-rename/01-dependent_rename.t b/tests/incremental/05-method-rename/01-dependent_rename.t
new file mode 100644
index 0000000000..bb0628447b
--- /dev/null
+++ b/tests/incremental/05-method-rename/01-dependent_rename.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 01-dependent_rename.json --enable incremental.save 01-dependent_rename.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 01-dependent_rename.c
+  $ patch -b <01-dependent_rename.patch
+  patching file 01-dependent_rename.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 01-dependent_rename.json --enable incremental.load 01-dependent_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 1 (with unchangedHeader = 1); added = 2; removed = 2
diff --git a/tests/incremental/05-method-rename/02-cyclic_rename_dependency.c b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.c
new file mode 100644
index 0000000000..331a5e25cb
--- /dev/null
+++ b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.c
@@ -0,0 +1,15 @@
+#include<stdio.h>
+
+void foo1(int c) {
+    if (c < 10) foo2(c + 1);
+}
+
+void foo2(int c) {
+    if (c < 10) foo1(c + 1);
+}
+
+int main() {
+    foo1(0);
+    foo2(0);
+    return 0;
+}
diff --git a/tests/incremental/05-method-rename/02-cyclic_rename_dependency.json b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/05-method-rename/02-cyclic_rename_dependency.patch b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.patch
new file mode 100644
index 0000000000..7f15d88c3a
--- /dev/null
+++ b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.patch
@@ -0,0 +1,23 @@
+--- tests/incremental/05-method-rename/02-cyclic_rename_dependency.c
++++ tests/incremental/05-method-rename/02-cyclic_rename_dependency.c
+@@ -2,14 +2,14 @@
+
+-void foo1(int c) {
+-    if (c < 10) foo2(c + 1);
++void bar1(int c) {
++    if (c < 10) bar2(c + 1);
+ }
+
+-void foo2(int c) {
+-    if (c < 10) foo1(c + 1);
++void bar2(int c) {
++    if (c < 10) bar1(c + 1);
+ }
+
+ int main() {
+-    foo1(0);
+-    foo2(0);
++    bar1(0);
++    bar2(0);
+     return 0;
+ }
diff --git a/tests/incremental/05-method-rename/02-cyclic_rename_dependency.t b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.t
new file mode 100644
index 0000000000..de9aa48e6c
--- /dev/null
+++ b/tests/incremental/05-method-rename/02-cyclic_rename_dependency.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 02-cyclic_rename_dependency.json --enable incremental.save 02-cyclic_rename_dependency.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 02-cyclic_rename_dependency.c
+  $ patch -b <02-cyclic_rename_dependency.patch
+  patching file 02-cyclic_rename_dependency.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 02-cyclic_rename_dependency.json --enable incremental.load 02-cyclic_rename_dependency.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 1 (with unchangedHeader = 1); added = 2; removed = 2
diff --git a/tests/incremental/05-method-rename/03-cyclic_with_swap.c b/tests/incremental/05-method-rename/03-cyclic_with_swap.c
new file mode 100644
index 0000000000..34026afa92
--- /dev/null
+++ b/tests/incremental/05-method-rename/03-cyclic_with_swap.c
@@ -0,0 +1,14 @@
+#include<stdio.h>
+
+void foo1(int c) {
+    if (c < 10) foo2(c + 1);
+}
+
+void foo2(int c) {
+    if (c < 10) foo1(c + 1);
+}
+
+int main() {
+    foo1(0);
+    return 0;
+}
diff --git a/tests/incremental/05-method-rename/03-cyclic_with_swap.json b/tests/incremental/05-method-rename/03-cyclic_with_swap.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/05-method-rename/03-cyclic_with_swap.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/05-method-rename/03-cyclic_with_swap.patch b/tests/incremental/05-method-rename/03-cyclic_with_swap.patch
new file mode 100644
index 0000000000..0886106162
--- /dev/null
+++ b/tests/incremental/05-method-rename/03-cyclic_with_swap.patch
@@ -0,0 +1,25 @@
+--- tests/incremental/05-method-rename/03-cyclic_with_swap.c
++++ tests/incremental/05-method-rename/03-cyclic_with_swap.c
+@@ -2,13 +2,17 @@
+
+-void foo1(int c) {
+-    if (c < 10) foo2(c + 1);
++void newFun(int c) {
++    printf("newfun");
+ }
+
+-void foo2(int c) {
+-    if (c < 10) foo1(c + 1);
++void bar1(int c) {
++    if (c < 10) bar2(c + 1);
++}
++
++void bar2(int c) {
++    if (c < 10) newFun(c + 1);
+ }
+
+ int main() {
+-    foo1(0);
++    bar1(0);
+     return 0;
+ }
diff --git a/tests/incremental/05-method-rename/03-cyclic_with_swap.t b/tests/incremental/05-method-rename/03-cyclic_with_swap.t
new file mode 100644
index 0000000000..d2e8dd6d97
--- /dev/null
+++ b/tests/incremental/05-method-rename/03-cyclic_with_swap.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 03-cyclic_with_swap.json --enable incremental.save 03-cyclic_with_swap.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 03-cyclic_with_swap.c
+  $ patch -b <03-cyclic_with_swap.patch
+  patching file 03-cyclic_with_swap.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 03-cyclic_with_swap.json --enable incremental.load 03-cyclic_with_swap.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 1 (with unchangedHeader = 1); added = 3; removed = 2
diff --git a/tests/incremental/05-method-rename/04-deep_change.c b/tests/incremental/05-method-rename/04-deep_change.c
new file mode 100644
index 0000000000..80037f934d
--- /dev/null
+++ b/tests/incremental/05-method-rename/04-deep_change.c
@@ -0,0 +1,18 @@
+#include<stdio.h>
+
+void zap() {
+    printf("zap");
+}
+
+void bar() {
+    zap();
+}
+
+void foo() {
+    bar();
+}
+
+int main() {
+    foo();
+    return 0;
+}
diff --git a/tests/incremental/05-method-rename/04-deep_change.json b/tests/incremental/05-method-rename/04-deep_change.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/05-method-rename/04-deep_change.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/05-method-rename/04-deep_change.patch b/tests/incremental/05-method-rename/04-deep_change.patch
new file mode 100644
index 0000000000..687b8f74bc
--- /dev/null
+++ b/tests/incremental/05-method-rename/04-deep_change.patch
@@ -0,0 +1,11 @@
+--- tests/incremental/05-method-rename/04-deep_change.c
++++ tests/incremental/05-method-rename/04-deep_change.c
+@@ -1,7 +1,7 @@
+ #include<stdio.h>
+
+ void zap() {
+-    printf("zap");
++    printf("drap");
+ }
+
+ void bar() {
diff --git a/tests/incremental/05-method-rename/04-deep_change.t b/tests/incremental/05-method-rename/04-deep_change.t
new file mode 100644
index 0000000000..1adcb56276
--- /dev/null
+++ b/tests/incremental/05-method-rename/04-deep_change.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 04-deep_change.json --enable incremental.save 04-deep_change.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 04-deep_change.c
+  $ patch -b <04-deep_change.patch
+  patching file 04-deep_change.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 04-deep_change.json --enable incremental.load 04-deep_change.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 1 (with unchangedHeader = 1); added = 0; removed = 0
diff --git a/tests/incremental/05-method-rename/05-common_rename.c b/tests/incremental/05-method-rename/05-common_rename.c
new file mode 100644
index 0000000000..ce72a6dda1
--- /dev/null
+++ b/tests/incremental/05-method-rename/05-common_rename.c
@@ -0,0 +1,20 @@
+#include<stdio.h>
+
+void foo() {
+    printf("foo");
+}
+
+void fun1() {
+    foo();
+}
+
+void fun2() {
+    foo();
+}
+
+int main() {
+    fun1();
+    fun2();
+    foo();
+    return 0;
+}
diff --git a/tests/incremental/05-method-rename/05-common_rename.json b/tests/incremental/05-method-rename/05-common_rename.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/05-method-rename/05-common_rename.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/05-method-rename/05-common_rename.patch b/tests/incremental/05-method-rename/05-common_rename.patch
new file mode 100644
index 0000000000..93904d5780
--- /dev/null
+++ b/tests/incremental/05-method-rename/05-common_rename.patch
@@ -0,0 +1,27 @@
+--- tests/incremental/05-method-rename/05-common_rename.c
++++ tests/incremental/05-method-rename/05-common_rename.c
+@@ -1,20 +1,20 @@
+ #include<stdio.h>
+
+-void foo() {
++void bar() {
+     printf("foo");
+ }
+
+ void fun1() {
+-    foo();
++    bar();
+ }
+
+ void fun2() {
+-    foo();
++    bar();
+ }
+
+ int main() {
+     fun1();
+     fun2();
+-    foo();
++    bar();
+     return 0;
+ }
diff --git a/tests/incremental/05-method-rename/05-common_rename.t b/tests/incremental/05-method-rename/05-common_rename.t
new file mode 100644
index 0000000000..62e99c6c80
--- /dev/null
+++ b/tests/incremental/05-method-rename/05-common_rename.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 05-common_rename.json --enable incremental.save 05-common_rename.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 05-common_rename.c
+  $ patch -b <05-common_rename.patch
+  patching file 05-common_rename.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 05-common_rename.json --enable incremental.load 05-common_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 0 (with unchangedHeader = 0); added = 0; removed = 0
diff --git a/tests/incremental/05-method-rename/06-recursive_rename.c b/tests/incremental/05-method-rename/06-recursive_rename.c
new file mode 100644
index 0000000000..dc9ac72e94
--- /dev/null
+++ b/tests/incremental/05-method-rename/06-recursive_rename.c
@@ -0,0 +1,7 @@
+void foo(int x) {
+    if(x > 1) foo(x - 1);
+}
+
+int main() {
+    foo(10);
+}
diff --git a/tests/incremental/05-method-rename/06-recursive_rename.json b/tests/incremental/05-method-rename/06-recursive_rename.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/05-method-rename/06-recursive_rename.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/05-method-rename/06-recursive_rename.patch b/tests/incremental/05-method-rename/06-recursive_rename.patch
new file mode 100644
index 0000000000..356f959256
--- /dev/null
+++ b/tests/incremental/05-method-rename/06-recursive_rename.patch
@@ -0,0 +1,13 @@
+--- tests/incremental/05-method-rename/06-recursive_rename.c
++++ tests/incremental/05-method-rename/06-recursive_rename.c
+@@ -1,7 +1,7 @@
+-void foo(int x) {
+-    if(x > 1) foo(x - 1);
++void bar(int x) {
++    if(x > 1) bar(x - 1);
+ }
+
+ int main() {
+-    foo(10);
++    bar(10);
+ }
diff --git a/tests/incremental/05-method-rename/06-recursive_rename.t b/tests/incremental/05-method-rename/06-recursive_rename.t
new file mode 100644
index 0000000000..dce0894ff1
--- /dev/null
+++ b/tests/incremental/05-method-rename/06-recursive_rename.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 06-recursive_rename.json --enable incremental.save 06-recursive_rename.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 06-recursive_rename.c
+  $ patch -b <06-recursive_rename.patch
+  patching file 06-recursive_rename.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 06-recursive_rename.json --enable incremental.load 06-recursive_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 0 (with unchangedHeader = 0); added = 0; removed = 0
diff --git a/tests/incremental/05-method-rename/dune b/tests/incremental/05-method-rename/dune
new file mode 100644
index 0000000000..1b37756f98
--- /dev/null
+++ b/tests/incremental/05-method-rename/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.{c,json,patch}) (sandbox preserve_file_kind)))
diff --git a/tests/incremental/06-glob-var-rename/00-simple_rename.c b/tests/incremental/06-glob-var-rename/00-simple_rename.c
new file mode 100644
index 0000000000..56650e98ed
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/00-simple_rename.c
@@ -0,0 +1,9 @@
+#include<stdio.h>
+
+int foo = 1;
+
+int main() {
+    printf("%d", foo);
+
+    return 0;
+}
diff --git a/tests/incremental/06-glob-var-rename/00-simple_rename.json b/tests/incremental/06-glob-var-rename/00-simple_rename.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/00-simple_rename.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/06-glob-var-rename/00-simple_rename.patch b/tests/incremental/06-glob-var-rename/00-simple_rename.patch
new file mode 100644
index 0000000000..1e0f3b2565
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/00-simple_rename.patch
@@ -0,0 +1,14 @@
+--- tests/incremental/06-glob-var-rename/00-simple_rename.c
++++ tests/incremental/06-glob-var-rename/00-simple_rename.c
+@@ -1,9 +1,9 @@
+ #include<stdio.h>
+
+-int foo = 1;
++int bar = 1;
+
+ int main() {
+-    printf("%d", foo);
++    printf("%d", bar);
+
+     return 0;
+ }
diff --git a/tests/incremental/06-glob-var-rename/00-simple_rename.t b/tests/incremental/06-glob-var-rename/00-simple_rename.t
new file mode 100644
index 0000000000..1855b903eb
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/00-simple_rename.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 00-simple_rename.json --enable incremental.save 00-simple_rename.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 00-simple_rename.c
+  $ patch -b <00-simple_rename.patch
+  patching file 00-simple_rename.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 00-simple_rename.json --enable incremental.load 00-simple_rename.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 0 (with unchangedHeader = 0); added = 0; removed = 0
diff --git a/tests/incremental/06-glob-var-rename/01-duplicate_local_global.c b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.c
new file mode 100644
index 0000000000..9ad715e50d
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.c
@@ -0,0 +1,14 @@
+#include<stdio.h>
+
+int foo = 1;
+
+int main() {
+
+    printf("%d", foo);
+
+    int foo = 2;
+
+    printf("%d", foo);
+
+    return 0;
+}
diff --git a/tests/incremental/06-glob-var-rename/01-duplicate_local_global.json b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/06-glob-var-rename/01-duplicate_local_global.patch b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.patch
new file mode 100644
index 0000000000..1d65c5672a
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.patch
@@ -0,0 +1,21 @@
+--- tests/incremental/06-glob-var-rename/01-duplicate_local_global.c
++++ tests/incremental/06-glob-var-rename/01-duplicate_local_global.c
+@@ -1,14 +1,14 @@
+ #include<stdio.h>
+
+-int foo = 1;
++int bar = 1;
+
+ int main() {
+
+-    printf("%d", foo);
++    printf("%d", bar);
+
+-    int foo = 2;
++    int bar = 2;
+
+-    printf("%d", foo);
++    printf("%d", bar);
+
+     return 0;
+ }
diff --git a/tests/incremental/06-glob-var-rename/01-duplicate_local_global.t b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.t
new file mode 100644
index 0000000000..cd2c5c0fea
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/01-duplicate_local_global.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 01-duplicate_local_global.json --enable incremental.save 01-duplicate_local_global.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 01-duplicate_local_global.c
+  $ patch -b <01-duplicate_local_global.patch
+  patching file 01-duplicate_local_global.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 01-duplicate_local_global.json --enable incremental.load 01-duplicate_local_global.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 0 (with unchangedHeader = 0); added = 0; removed = 0
diff --git a/tests/incremental/06-glob-var-rename/02-add_new_gvar.c b/tests/incremental/06-glob-var-rename/02-add_new_gvar.c
new file mode 100644
index 0000000000..5efe319981
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/02-add_new_gvar.c
@@ -0,0 +1,8 @@
+#include<stdio.h>
+
+int myVar = 1;
+
+int main() {
+    printf("%d", myVar);
+    printf("%d", myVar);
+}
diff --git a/tests/incremental/06-glob-var-rename/02-add_new_gvar.json b/tests/incremental/06-glob-var-rename/02-add_new_gvar.json
new file mode 100644
index 0000000000..0db3279e44
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/02-add_new_gvar.json
@@ -0,0 +1,3 @@
+{
+
+}
diff --git a/tests/incremental/06-glob-var-rename/02-add_new_gvar.patch b/tests/incremental/06-glob-var-rename/02-add_new_gvar.patch
new file mode 100644
index 0000000000..f0c145107a
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/02-add_new_gvar.patch
@@ -0,0 +1,13 @@
+--- tests/incremental/06-glob-var-rename/02-add_new_gvar.c
++++ tests/incremental/06-glob-var-rename/02-add_new_gvar.c
+@@ -1,8 +1,9 @@
+ #include<stdio.h>
+
+ int myVar = 1;
++int foo = 1;
+
+ int main() {
+     printf("%d", myVar);
+-    printf("%d", myVar);
++    printf("%d", foo);
+ }
diff --git a/tests/incremental/06-glob-var-rename/02-add_new_gvar.t b/tests/incremental/06-glob-var-rename/02-add_new_gvar.t
new file mode 100644
index 0000000000..c71cd6808f
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/02-add_new_gvar.t
@@ -0,0 +1,14 @@
+Run Goblint on initial program version
+
+  $ goblint --conf 02-add_new_gvar.json --enable incremental.save 02-add_new_gvar.c > /dev/null 2>&1
+
+Apply patch
+
+  $ chmod +w 02-add_new_gvar.c
+  $ patch -b <02-add_new_gvar.patch
+  patching file 02-add_new_gvar.c
+
+Run Goblint incrementally on new program version and check the change detection result
+
+  $ goblint --conf 02-add_new_gvar.json --enable incremental.load 02-add_new_gvar.c | grep 'change_info' | sed -r 's/^change_info = \{ unchanged = [[:digit:]]+; (.*) \}$/\1/'
+  changed = 1 (with unchangedHeader = 1); added = 1; removed = 0
diff --git a/tests/incremental/06-glob-var-rename/dune b/tests/incremental/06-glob-var-rename/dune
new file mode 100644
index 0000000000..1b37756f98
--- /dev/null
+++ b/tests/incremental/06-glob-var-rename/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.{c,json,patch}) (sandbox preserve_file_kind)))
diff --git a/tests/incremental/dune b/tests/incremental/dune
new file mode 100644
index 0000000000..fdb1d941c2
--- /dev/null
+++ b/tests/incremental/dune
@@ -0,0 +1,3 @@
+(cram
+ (applies_to :whole_subtree)
+ (deps %{bin:goblint} (package goblint))) ; need entire package for includes/