diff --git a/scripts/test-incremental-multiple.sh b/scripts/test-incremental-multiple.sh
new file mode 100644
index 0000000000..0dee9c117d
--- /dev/null
+++ b/scripts/test-incremental-multiple.sh
@@ -0,0 +1,37 @@
+#This file runs 3 incremental tests in total. As such it is similar to test-incremental.sh but performs an additional incremental run on top of it.
+test=$1
+
+base=./tests/incremental
+source=$base/${test}_1.c
+conf=$base/$test.json
+patch1=$base/${test}_1.patch
+patch2=$base/${test}_2.patch
+
+args="--enable dbg.debug --enable printstats -v"
+
+cat $source
+
+./goblint --conf $conf $args --enable incremental.save $source &> $base/$test.before.log --html
+
+patch -p0 -b <$patch1
+
+cat $source
+
+./goblint --conf $conf $args --enable incremental.load --enable incremental.save $source &> $base/$test.after.incr1.log --html
+
+patch -p0 <$patch2
+
+cat $source
+
+./goblint --conf $conf $args --enable incremental.load --enable incremental.save --set save_run $base/$test-incrementalrun $source &> $base/$test.after.incr2.log --html
+
+
+#./goblint --conf $conf $args --enable incremental.only-rename --set save_run $base/$test-originalrun $source &> $base/$test.after.scratch.log --html
+#./goblint --conf $conf --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source --html
+
+patch -p0 -b -R <$patch2
+patch -p0 -b -R <$patch1
+# rm -r $base/$test-originalrun $base/$test-incrementalrun
+rm -r $base/$test-incrementalrun
+
+cat $source
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 0a57bf0f7d..88142cd45f 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -1,10 +1,44 @@
 open Cil
+open CilMaps
 
 (* global_type and global_t are implicitly used by GlobalMap to keep GVarDecl apart from GVar and GFun, so do not remove! *)
 type global_type = Fun | Decl | Var
 
 and global_identifier = {name: string ; global_t: global_type} [@@deriving ord]
 
+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
+
+(*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)
+
+(*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 ->
+    (*Printf.printf "Assumption is: %s -> %s\n" original now;*)
+    now = name2
+  | None ->
+    (*Printf.printf "No assumption when %s, %s, %b\n" name1 name2 (name1 = name2);*)
+    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 ^ "])"
+
 let identifier_of_global glob =
   match glob with
   | GFun (fundec, l) -> {name = fundec.svar.vname; global_t = Fun}
@@ -18,38 +52,42 @@ module GlobalMap = Map.Make(struct
 
 
 (* hack: CIL generates new type names for anonymous types - we want to ignore these *)
-let compare_name a b =
+let compare_name (a: string) (b: string) =
   let anon_struct = "__anonstruct_" in
   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 (a: constant) (b: constant) = match a, b with
+let rec eq_constant (rename_mapping: rename_mapping) (a: constant) (b: constant)  =
+  match a, b with
   | CInt (val1, kind1, str1), CInt (val2, kind2, str2) -> Cilint.compare_cilint val1 val2 = 0 && kind1 = kind2 (* Ignore string representation, i.e. 0x2 == 2 *)
-  | CEnum (exp1, str1, enuminfo1), CEnum (exp2, str2, enuminfo2) -> eq_exp exp1 exp2 (* Ignore name and enuminfo  *)
+  | CEnum (exp1, str1, enuminfo1), CEnum (exp2, str2, enuminfo2) -> eq_exp exp1 exp2 rename_mapping (* Ignore name and enuminfo  *)
   | a, b -> a = b
 
-and eq_exp (a: exp) (b: exp) = match a,b with
-  | Const c1, Const c2 -> eq_constant c1 c2
-  | Lval lv1, Lval lv2 -> eq_lval lv1 lv2
-  | SizeOf typ1, SizeOf typ2 -> eq_typ typ1 typ2
-  | SizeOfE exp1, SizeOfE exp2 -> eq_exp exp1 exp2
+and eq_exp2 (rename_mapping: rename_mapping) (a: exp) (b: exp) = eq_exp a b rename_mapping
+
+and eq_exp (a: exp) (b: exp) (rename_mapping: rename_mapping) =
+  match a, b with
+  | Const c1, Const c2 -> eq_constant rename_mapping c1 c2
+  | Lval lv1, Lval lv2 -> eq_lval lv1 lv2 rename_mapping
+  | SizeOf typ1, SizeOf typ2 -> eq_typ typ1 typ2 rename_mapping
+  | SizeOfE exp1, SizeOfE exp2 -> eq_exp exp1 exp2 rename_mapping
   | SizeOfStr str1, SizeOfStr str2 -> str1 = str2 (* possibly, having the same length would suffice *)
-  | AlignOf typ1, AlignOf typ2 -> eq_typ typ1 typ2
-  | AlignOfE exp1, AlignOfE exp2 -> eq_exp exp1 exp2
-  | UnOp (op1, exp1, typ1), UnOp (op2, exp2, typ2) -> op1 == op2 && eq_exp exp1 exp2 && eq_typ typ1 typ2
-  | BinOp (op1, left1, right1, typ1), BinOp (op2, left2, right2, typ2) ->  op1 = op2 && eq_exp left1 left2 && eq_exp right1 right2 && eq_typ typ1 typ2
-  | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ typ1 typ2 &&  eq_exp exp1 exp2
-  | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2
-  | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2
-  | Real exp1, Real exp2 -> eq_exp exp1 exp2
-  | Imag exp1, Imag exp2 -> eq_exp exp1 exp2
-  | Question (b1, t1, f1, typ1), Question (b2, t2, f2, typ2) -> eq_exp b1 b2 && eq_exp t1 t2 && eq_exp f1 f2 && eq_typ typ1 typ2
+  | AlignOf typ1, AlignOf typ2 -> eq_typ typ1 typ2 rename_mapping
+  | AlignOfE exp1, AlignOfE exp2 -> eq_exp exp1 exp2 rename_mapping
+  | UnOp (op1, exp1, typ1), UnOp (op2, exp2, typ2) -> op1 == op2 && eq_exp exp1 exp2 rename_mapping && eq_typ typ1 typ2 rename_mapping
+  | BinOp (op1, left1, right1, typ1), BinOp (op2, left2, right2, typ2) ->  op1 = op2 && eq_exp left1 left2 rename_mapping && eq_exp right1 right2 rename_mapping && eq_typ typ1 typ2 rename_mapping
+  | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ typ1 typ2 rename_mapping && eq_exp exp1 exp2 rename_mapping
+  | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2 rename_mapping
+  | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2 rename_mapping
+  | Real exp1, Real exp2 -> eq_exp exp1 exp2 rename_mapping
+  | Imag exp1, Imag exp2 -> eq_exp exp1 exp2 rename_mapping
+  | Question (b1, t1, f1, typ1), Question (b2, t2, f2, typ2) -> eq_exp b1 b2 rename_mapping && eq_exp t1 t2 rename_mapping && eq_exp f1 f2 rename_mapping && eq_typ typ1 typ2 rename_mapping
   | AddrOfLabel _, AddrOfLabel _ -> false (* TODO: what to do? *)
   | _, _ -> false
 
-and eq_lhost (a: lhost) (b: lhost) = match a, b with
-    Var v1, Var v2 -> eq_varinfo v1 v2
-  | Mem exp1, Mem exp2 -> eq_exp exp1 exp2
+and eq_lhost (a: lhost) (b: lhost) (rename_mapping: rename_mapping) = match a, b with
+    Var v1, Var v2 -> eq_varinfo v1 v2 rename_mapping
+  | Mem exp1, Mem exp2 -> eq_exp exp1 exp2 rename_mapping
   | _, _ -> false
 
 and global_typ_acc: (typ * typ) list ref = ref [] (* TODO: optimize with physical Hashtbl? *)
@@ -58,21 +96,21 @@ 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) =
+and eq_typ_acc (a: typ) (b: typ) (acc: (typ * typ) list) (rename_mapping: rename_mapping) =
   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 acc && GobList.equal eq_attribute attr1 attr2
-    | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 acc && eq_exp lenExp1 lenExp2 &&  GobList.equal eq_attribute attr1 attr2
-    | TArray (typ1, None, attr1), TArray (typ2, None, attr2) -> eq_typ_acc typ1 typ2 acc && GobList.equal eq_attribute attr1 attr2
+    | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 acc rename_mapping && GobList.equal (eq_attribute rename_mapping) attr1 attr2
+    | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 acc rename_mapping && eq_exp lenExp1 lenExp2 rename_mapping &&  GobList.equal (eq_attribute rename_mapping) attr1 attr2
+    | TArray (typ1, None, attr1), TArray (typ2, None, attr2) -> eq_typ_acc typ1 typ2 acc rename_mapping && GobList.equal (eq_attribute rename_mapping) attr1 attr2
     | TFun (typ1, (Some list1), varArg1, attr1), TFun (typ2, (Some list2), varArg2, attr2)
-      ->  eq_typ_acc typ1 typ2 acc && GobList.equal (eq_args acc) list1 list2 && varArg1 = varArg2 &&
-          GobList.equal eq_attribute attr1 attr2
+      -> eq_typ_acc typ1 typ2 acc rename_mapping && GobList.equal (eq_args rename_mapping acc) list1 list2 && varArg1 = varArg2 &&
+         GobList.equal (eq_attribute rename_mapping) attr1 attr2
     | TFun (typ1, None, varArg1, attr1), TFun (typ2, None, varArg2, attr2)
-      ->  eq_typ_acc typ1 typ2 acc && varArg1 = varArg2 &&
-          GobList.equal eq_attribute attr1 attr2
-    | TNamed (typinfo1, attr1), TNamed (typeinfo2, attr2) -> eq_typ_acc typinfo1.ttype typeinfo2.ttype acc && GobList.equal eq_attribute attr1 attr2 (* Ignore tname, treferenced *)
-    | TNamed (tinf, attr), b -> eq_typ_acc tinf.ttype b acc (* Ignore tname, treferenced. TODO: dismiss attributes, or not? *)
-    | a, TNamed (tinf, attr) -> eq_typ_acc a tinf.ttype acc (* Ignore tname, treferenced . TODO: dismiss attributes, or not? *)
+      ->  eq_typ_acc typ1 typ2 acc rename_mapping && varArg1 = varArg2 &&
+          GobList.equal (eq_attribute rename_mapping) attr1 attr2
+    | TNamed (typinfo1, attr1), TNamed (typeinfo2, attr2) -> eq_typ_acc typinfo1.ttype typeinfo2.ttype acc rename_mapping && GobList.equal (eq_attribute rename_mapping) attr1 attr2 (* Ignore tname, treferenced *)
+    | TNamed (tinf, attr), b -> eq_typ_acc tinf.ttype b acc rename_mapping (* Ignore tname, treferenced. TODO: dismiss attributes, or not? *)
+    | a, TNamed (tinf, attr) -> eq_typ_acc a tinf.ttype acc rename_mapping (* 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 (
@@ -81,91 +119,132 @@ and eq_typ_acc (a: typ) (b: typ) (acc: (typ * typ) list) =
       )
       else (
         let acc = (a, b) :: acc in
-        let res = eq_compinfo compinfo1 compinfo2 acc && GobList.equal eq_attribute attr1 attr2 in
+        let res = eq_compinfo compinfo1 compinfo2 acc rename_mapping && GobList.equal (eq_attribute rename_mapping) attr1 attr2 in
         if res && compinfo1.cname <> compinfo2.cname then
           compinfo2.cname <- compinfo1.cname;
         if res then
           global_typ_acc := (a, b) :: !global_typ_acc;
         res
       )
-    | TEnum (enuminfo1, attr1), TEnum (enuminfo2, attr2) -> let res = eq_enuminfo enuminfo1 enuminfo2 && GobList.equal eq_attribute 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 attr1 attr2
-    | TVoid attr1, TVoid attr2 -> GobList.equal eq_attribute attr1 attr2
-    | TInt (ik1, attr1), TInt (ik2, attr2) -> ik1 = ik2 && GobList.equal eq_attribute attr1 attr2
-    | TFloat (fk1, attr1), TFloat (fk2, attr2) -> fk1 = fk2 && GobList.equal eq_attribute attr1 attr2
+    | TEnum (enuminfo1, attr1), TEnum (enuminfo2, attr2) -> let res = eq_enuminfo enuminfo1 enuminfo2 rename_mapping && GobList.equal (eq_attribute rename_mapping) 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) attr1 attr2
+    | TVoid attr1, TVoid attr2 -> GobList.equal (eq_attribute rename_mapping) attr1 attr2
+    | TInt (ik1, attr1), TInt (ik2, attr2) -> ik1 = ik2 && GobList.equal (eq_attribute rename_mapping) attr1 attr2
+    | TFloat (fk1, attr1), TFloat (fk2, attr2) -> fk1 = fk2 && GobList.equal (eq_attribute rename_mapping) attr1 attr2
     | _, _ -> false
   in
   if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a\n" d_type a d_type b;
   r
 
-and eq_typ (a: typ) (b: typ) = eq_typ_acc a b []
+and eq_typ (a: typ) (b: typ) (rename_mapping: rename_mapping) = eq_typ_acc a b [] rename_mapping
 
-and eq_eitems (a: string * exp * location) (b: string * exp * location) = match a, b with
-    (name1, exp1, _l1), (name2, exp2, _l2) -> name1 = name2 && eq_exp exp1 exp2
+and eq_eitems (rename_mapping: rename_mapping) (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
 (* Ignore location *)
 
-and eq_enuminfo (a: enuminfo) (b: enuminfo) =
+and eq_enuminfo (a: enuminfo) (b: enuminfo) (rename_mapping: rename_mapping) =
   compare_name a.ename b.ename &&
-  GobList.equal eq_attribute a.eattr b.eattr &&
-  GobList.equal eq_eitems a.eitems b.eitems
+  GobList.equal (eq_attribute rename_mapping) a.eattr b.eattr &&
+  GobList.equal (eq_eitems rename_mapping) a.eitems b.eitems
 (* Ignore ereferenced *)
 
-and eq_args (acc: (typ * typ) list) (a: string * typ * attributes) (b: string * typ * attributes) = match a, b with
-    (name1, typ1, attr1), (name2, typ2, attr2) -> name1 = name2 && eq_typ_acc typ1 typ2 acc && GobList.equal eq_attribute attr1 attr2
+and eq_args (rename_mapping: rename_mapping) (acc: (typ * typ) list) (a: string * typ * attributes) (b: string * typ * attributes) = match a, b with
+    (name1, typ1, attr1), (name2, typ2, attr2) ->
+    rename_mapping_aware_name_comparison name1 name2 rename_mapping && eq_typ_acc typ1 typ2 acc rename_mapping && GobList.equal (eq_attribute rename_mapping) attr1 attr2
 
-and eq_attrparam (a: attrparam) (b: attrparam) = match a, b with
-  | ACons (str1, attrparams1), ACons (str2, attrparams2) -> str1 = str2 && GobList.equal eq_attrparam attrparams1 attrparams2
-  | ASizeOf typ1, ASizeOf typ2 -> eq_typ typ1 typ2
-  | ASizeOfE attrparam1, ASizeOfE attrparam2 -> eq_attrparam attrparam1 attrparam2
+and eq_attrparam (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) attrparams1 attrparams2
+  | ASizeOf typ1, ASizeOf typ2 -> eq_typ typ1 typ2 rename_mapping
+  | ASizeOfE attrparam1, ASizeOfE attrparam2 -> eq_attrparam rename_mapping attrparam1 attrparam2
   | ASizeOfS typsig1, ASizeOfS typsig2 -> typsig1 = typsig2
-  | AAlignOf typ1, AAlignOf typ2 -> eq_typ typ1 typ2
-  | AAlignOfE attrparam1, AAlignOfE attrparam2 -> eq_attrparam attrparam1 attrparam2
+  | AAlignOf typ1, AAlignOf typ2 -> eq_typ typ1 typ2 rename_mapping
+  | AAlignOfE attrparam1, AAlignOfE attrparam2 -> eq_attrparam rename_mapping attrparam1 attrparam2
   | AAlignOfS typsig1, AAlignOfS typsig2 -> typsig1 = typsig2
-  | AUnOp (op1, attrparam1), AUnOp (op2, attrparam2) -> op1 = op2 && eq_attrparam attrparam1 attrparam2
-  | ABinOp (op1, left1, right1), ABinOp (op2, left2, right2) -> op1 = op2 && eq_attrparam left1 left2 && eq_attrparam right1 right2
-  | ADot (attrparam1, str1), ADot (attrparam2, str2) -> eq_attrparam attrparam1 attrparam2 && str1 = str2
-  | AStar attrparam1, AStar attrparam2 -> eq_attrparam attrparam1 attrparam2
-  | AAddrOf attrparam1, AAddrOf attrparam2 -> eq_attrparam attrparam1 attrparam2
-  | AIndex (left1, right1), AIndex (left2, right2) -> eq_attrparam left1 left2 && eq_attrparam right1 right2
-  | AQuestion (left1, middle1, right1), AQuestion (left2, middle2, right2) -> eq_attrparam left1 left2 && eq_attrparam middle1 middle2 && eq_attrparam right1 right2
+  | AUnOp (op1, attrparam1), AUnOp (op2, attrparam2) -> op1 = op2 && eq_attrparam rename_mapping attrparam1 attrparam2
+  | ABinOp (op1, left1, right1), ABinOp (op2, left2, right2) -> op1 = op2 && eq_attrparam rename_mapping left1 left2 && eq_attrparam rename_mapping right1 right2
+  | ADot (attrparam1, str1), ADot (attrparam2, str2) -> eq_attrparam rename_mapping attrparam1 attrparam2 && str1 = str2
+  | AStar attrparam1, AStar attrparam2 -> eq_attrparam rename_mapping attrparam1 attrparam2
+  | AAddrOf attrparam1, AAddrOf attrparam2 -> eq_attrparam rename_mapping attrparam1 attrparam2
+  | AIndex (left1, right1), AIndex (left2, right2) -> eq_attrparam rename_mapping left1 left2  && eq_attrparam rename_mapping right1 right2
+  | AQuestion (left1, middle1, right1), AQuestion (left2, middle2, right2) -> eq_attrparam rename_mapping left1 left2 && eq_attrparam rename_mapping middle1 middle2 && eq_attrparam rename_mapping right1 right2
   | a, b -> a = b
 
-and eq_attribute (a: attribute) (b: attribute) = match a, b with
-    Attr (name1, params1), Attr (name2, params2) -> name1 = name2 && GobList.equal eq_attrparam params1 params2
+and eq_attribute (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) params1 params2
+
+and eq_varinfo2 (rename_mapping: rename_mapping) (a: varinfo) (b: varinfo) = eq_varinfo a b rename_mapping
 
-and eq_varinfo (a: varinfo) (b: varinfo) = a.vname = b.vname && eq_typ a.vtype b.vtype && GobList.equal eq_attribute a.vattr b.vattr &&
-                                           a.vstorage = b.vstorage && a.vglob = b.vglob && a.vaddrof = b.vaddrof
+and eq_varinfo (a: varinfo) (b: varinfo) (rename_mapping: rename_mapping) =
+  (*Printf.printf "Comp %s with %s\n" a.vname b.vname;*)
+
+  let (_, method_rename_mappings) = rename_mapping 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 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
+      )
+    | _ -> rename_mapping_aware_name_comparison a.vname b.vname rename_mapping
+  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
+  in
+
+  let typeCheck = eq_typ a.vtype b.vtype typ_rename_mapping in
+  let attrCheck = GobList.equal (eq_attribute rename_mapping) a.vattr b.vattr in
+
+  (*let _ = Printf.printf "Comparing vars: %s = %s\n" a.vname b.vname in *)
+  (*a.vname = b.vname*)
+  let result = isNamingOk && typeCheck && attrCheck &&
+               a.vstorage = b.vstorage && a.vglob = b.vglob && a.vaddrof = b.vaddrof in
+
+  result
 (* 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) =
+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 acc) a.cfields b.cfields &&
-  GobList.equal eq_attribute a.cattr b.cattr &&
+  GobList.equal (fun a b-> eq_fieldinfo a b acc rename_mapping) a.cfields b.cfields &&
+  GobList.equal (eq_attribute rename_mapping) a.cattr b.cattr &&
   a.cdefined = b.cdefined (* Ignore ckey, and ignore creferenced *)
 
-and eq_fieldinfo (a: fieldinfo) (b: fieldinfo) (acc: (typ * typ) list)=
+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 acc && a.fbitfield = b.fbitfield &&  GobList.equal eq_attribute a.fattr b.fattr in
+  let r = a.fname = b.fname && eq_typ_acc a.ftype b.ftype acc rename_mapping && a.fbitfield = b.fbitfield &&  GobList.equal (eq_attribute rename_mapping) a.fattr b.fattr in
   if Messages.tracing then Messages.traceu "compareast" "fieldinfo %s vs %s\n" a.fname b.fname;
   r
 
-and eq_offset (a: offset) (b: offset) = match a, b with
+and eq_offset (a: offset) (b: offset) (rename_mapping: rename_mapping) = match a, b with
     NoOffset, NoOffset -> true
-  | Field (info1, offset1), Field (info2, offset2) -> eq_fieldinfo info1 info2 [] && eq_offset offset1 offset2
-  | Index (exp1, offset1), Index (exp2, offset2) -> eq_exp exp1 exp2 && eq_offset offset1 offset2
+  | Field (info1, offset1), Field (info2, offset2) -> eq_fieldinfo info1 info2 [] rename_mapping && eq_offset offset1 offset2 rename_mapping
+  | Index (exp1, offset1), Index (exp2, offset2) -> eq_exp exp1 exp2 rename_mapping && eq_offset offset1 offset2 rename_mapping
   | _, _ -> false
 
-and eq_lval (a: lval) (b: lval) = match a, b with
-    (host1, off1), (host2, off2) -> eq_lhost host1 host2 && eq_offset off1 off2
+and eq_lval (a: lval) (b: lval) (rename_mapping: rename_mapping) = match a, b with
+    (host1, off1), (host2, off2) -> eq_lhost host1 host2 rename_mapping && eq_offset off1 off2 rename_mapping
 
-let eq_instr (a: instr) (b: instr) = match a, b with
-  | Set (lv1, exp1, _l1, _el1), Set (lv2, exp2, _l2, _el2) -> eq_lval lv1 lv2 && eq_exp exp1 exp2
-  | Call (Some lv1, f1, args1, _l1, _el1), Call (Some lv2, f2, args2, _l2, _el2) -> eq_lval lv1 lv2 && eq_exp f1 f2 && GobList.equal eq_exp args1 args2
-  | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) -> eq_exp f1 f2 && GobList.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 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_lval z1 z2) ci1 ci2 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && 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
+let eq_instr (rename_mapping: rename_mapping) (a: instr) (b: instr)  = 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
+  | 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_exp2 rename_mapping) args1 args2
+  | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) ->
+    eq_exp f1 f2 rename_mapping && GobList.equal (eq_exp2 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 *)
+  | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2 rename_mapping
   | _, _ -> false
 
 let eq_label (a: label) (b: label) = match a, b with
@@ -184,25 +263,35 @@ 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) =
-  let eq_block' = fun x y -> if cfg_comp then true else eq_block (x, af) (y, bf) in
+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
   match a, b with
-  | Instr is1, Instr is2 -> GobList.equal eq_instr is1 is2
-  | Return (Some exp1, _l1), Return (Some exp2, _l2) -> eq_exp exp1 exp2
+  | Instr is1, Instr is2 -> GobList.equal (eq_instr rename_mapping) is1 is2
+  | 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 && 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 && eq_block' block1 block2 && GobList.equal (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
+  | 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
 
-and eq_stmt ?cfg_comp ((a, af): stmt * fundec) ((b, bf): stmt * fundec) =
+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)
+  eq_stmtkind ?cfg_comp (a.skind, af) (b.skind, bf) rename_mapping
+
+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) =
-  a.battrs = b.battrs && GobList.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
+
+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
diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
index 3956597f4b..78a182a291 100644
--- a/src/incremental/compareCFG.ml
+++ b/src/incremental/compareCFG.ml
@@ -1,28 +1,32 @@
 open MyCFG
 open Queue
 open Cil
+open CilMaps
 include CompareAST
 
 let eq_node (x, fun1) (y, fun2) =
+  let empty_rename_mapping: rename_mapping = (StringMap.empty, VarinfoMap.empty) in
   match x,y with
-  | Statement s1, Statement s2 -> eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2)
-  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar
-  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar
+  | Statement s1, Statement s2 -> eq_stmt ~cfg_comp:true (s1, fun1) (s2, fun2) empty_rename_mapping
+  | Function f1, Function f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping
+  | FunctionEntry f1, FunctionEntry f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping
   | _ -> false
 
 (* TODO: compare ASMs properly instead of simply always assuming that they are not the same *)
-let eq_edge x y = match x, y with
-  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 && eq_exp rv1 rv2
-  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 && GobList.equal eq_exp ars1 ars2
+let eq_edge x y =
+  let empty_rename_mapping: rename_mapping = (StringMap.empty, VarinfoMap.empty) in
+  match x, y with
+  | Assign (lv1, rv1), Assign (lv2, rv2) -> eq_lval lv1 lv2 empty_rename_mapping && eq_exp rv1 rv2 empty_rename_mapping
+  | Proc (None,f1,ars1), Proc (None,f2,ars2) -> eq_exp f1 f2 empty_rename_mapping && GobList.equal (eq_exp2 empty_rename_mapping) ars1 ars2
   | Proc (Some r1,f1,ars1), Proc (Some r2,f2,ars2) ->
-    eq_lval r1 r2 && eq_exp f1 f2 && GobList.equal eq_exp ars1 ars2
-  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar
-  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar
-  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 && eq_varinfo fd1.svar fd2.svar
-  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 && b1 = b2
+    eq_lval r1 r2 empty_rename_mapping && eq_exp f1 f2 empty_rename_mapping && GobList.equal (eq_exp2 empty_rename_mapping) ars1 ars2
+  | Entry f1, Entry f2 -> eq_varinfo f1.svar f2.svar empty_rename_mapping
+  | Ret (None,fd1), Ret (None,fd2) -> eq_varinfo fd1.svar fd2.svar empty_rename_mapping
+  | Ret (Some r1,fd1), Ret (Some r2,fd2) -> eq_exp r1 r2 empty_rename_mapping && eq_varinfo fd1.svar fd2.svar empty_rename_mapping
+  | Test (p1,b1), Test (p2,b2) -> eq_exp p1 p2 empty_rename_mapping && b1 = b2
   | ASM _, ASM _ -> false
   | Skip, Skip -> true
-  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2
+  | VDecl v1, VDecl v2 -> eq_varinfo v1 v2 empty_rename_mapping
   | _ -> false
 
 (* The order of the edges in the list is relevant. Therefore compare them one to one without sorting first *)
diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 0456a942e9..a956cb6609 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -1,5 +1,6 @@
 open Cil
 open MyCFG
+open CilMaps
 include CompareAST
 include CompareCFG
 
@@ -36,18 +37,51 @@ let should_reanalyze (fdec: Cil.fundec) =
 (* 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 (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) =
-  let unchangedHeader = eq_varinfo a.svar b.svar && GobList.equal eq_varinfo a.sformals b.sformals in
+let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) =
+  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 a.sformals b.sformals (StringMap.empty) in
+        let actHeaderRenameMapping = (headerRenameMapping, global_rename_mapping) in
+        eq_varinfo a.svar b.svar actHeaderRenameMapping && GobList.equal (eq_varinfo2 actHeaderRenameMapping) a.sformals b.sformals, headerRenameMapping
+      )
+    | Some _ -> (
+        eq_varinfo a.svar b.svar emptyRenameMapping && GobList.equal (eq_varinfo2 emptyRenameMapping) a.sformals b.sformals, StringMap.empty
+      )
+  in
+
   let identical, diffOpt =
     if should_reanalyze a then
       false, None
     else
-      let sameDef = unchangedHeader && GobList.equal eq_varinfo a.slocals b.slocals in
+      (* 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 flag, local_rename =
+        match cfgs with
+        | None -> rename_mapping_aware_compare a.slocals b.slocals headerRenameMapping
+        | Some _ -> GobList.equal (eq_varinfo2 emptyRenameMapping) a.slocals b.slocals, StringMap.empty
+      in
+      let rename_mapping: rename_mapping = (local_rename, global_rename_mapping) in
+
+      let sameDef = unchangedHeader && flag in
       if not sameDef then
         (false, None)
       else
         match cfgs with
-        | None -> eq_block (a.sbody, a) (b.sbody, b), None
+        | None -> eq_block (a.sbody, a) (b.sbody, b) 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
@@ -57,10 +91,10 @@ let eqF (a: Cil.fundec) (b: Cil.fundec) (cfgs : (cfg * (cfg * cfg)) option) =
   in
   identical, unchangedHeader, diffOpt
 
-let eq_glob (a: global) (b: global) (cfgs : (cfg * (cfg * cfg)) option) = match a, b with
-  | GFun (f,_), GFun (g,_) -> eqF f g cfgs
-  | GVar (x, init_x, _), GVar (y, init_y, _) -> eq_varinfo x y, false, None (* ignore the init_info - a changed init of a global will lead to a different start state *)
-  | GVarDecl (x, _), GVarDecl (y, _) -> eq_varinfo x y, false, None
+let eq_glob (a: global) (b: global) (cfgs : (cfg * (cfg * cfg)) option) (global_rename_mapping: method_rename_assumptions) = match a, b with
+  | GFun (f,_), GFun (g,_) -> eqF f g cfgs global_rename_mapping
+  | GVar (x, init_x, _), GVar (y, init_y, _) -> eq_varinfo x y (StringMap.empty, VarinfoMap.empty), false, None (* ignore the init_info - a changed init of a global will lead to a different start state *)
+  | GVarDecl (x, _), GVarDecl (y, _) -> eq_varinfo x y (StringMap.empty, VarinfoMap.empty), false, None
   | _ -> ignore @@ Pretty.printf "Not comparable: %a and %a\n" Cil.d_global a Cil.d_global b; false, false, None
 
 let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
@@ -68,6 +102,30 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     then Some (CfgTools.getCFG oldAST |> fst, CfgTools.getCFG newAST)
     else None in
 
+  let generate_global_rename_mapping map global =
+    try
+      let ident = identifier_of_global global in
+      let old_global = GlobalMap.find ident map in
+
+      match old_global, global with
+      | GFun(f, _), GFun (g, _) ->
+        let renamed_params: string StringMap.t = if (List.length f.sformals) = (List.length g.sformals) then
+            let mappings = List.combine f.sformals g.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 (f.svar.vname = g.svar.vname) || (StringMap.cardinal renamed_params) > 0 then
+          Some (f.svar, {original_method_name=f.svar.vname; new_method_name=g.svar.vname; parameter_renames=renamed_params})
+        else None
+      | _, _ -> None
+    with Not_found -> None
+  in
+
   let addGlobal map global  =
     try
       let gid = identifier_of_global global in
@@ -79,14 +137,15 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     with
       Not_found -> map
   in
+
   let changes = empty_change_info () in
   global_typ_acc := [];
-  let checkUnchanged map global =
+  let findChanges map global global_rename_mapping =
     try
       let ident = identifier_of_global global in
       let old_global = GlobalMap.find ident map in
       (* Do a (recursive) equal comparison ignoring location information *)
-      let identical, unchangedHeader, diff = eq old_global global cfgs in
+      let identical, unchangedHeader, diff = eq old_global global cfgs global_rename_mapping in
       if identical
       then changes.unchanged <- {current = global; old = old_global} :: changes.unchanged
       else changes.changed <- {current = global; old = old_global; unchangedHeader; diff} :: changes.changed
@@ -100,10 +159,18 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
   (* Store a map from functionNames in the old file to the function definition*)
   let oldMap = Cil.foldGlobals oldAST addGlobal GlobalMap.empty in
   let newMap = Cil.foldGlobals newAST addGlobal GlobalMap.empty in
+
+  let global_rename_mapping: method_rename_assumptions = Cil.foldGlobals newAST (fun (current_global_rename_mapping: method_rename_assumption VarinfoMap.t) global ->
+      match generate_global_rename_mapping oldMap global with
+      | Some (funVar, rename_mapping) -> VarinfoMap.add funVar rename_mapping current_global_rename_mapping
+      | None -> current_global_rename_mapping
+    ) VarinfoMap.empty
+  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. *)
   Cil.iterGlobals newAST
-    (fun glob -> checkUnchanged oldMap glob);
+    (fun glob -> findChanges oldMap glob global_rename_mapping);
 
   (* We check whether functions have been added or removed *)
   Cil.iterGlobals newAST (fun glob -> if not (checkExists oldMap glob) then changes.added <- (glob::changes.added));
diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml
index b2655f9d54..a6823db4f0 100644
--- a/src/incremental/updateCil.ml
+++ b/src/incremental/updateCil.ml
@@ -43,8 +43,8 @@ let update_ids (old_file: file) (ids: max_ids) (new_file: file) (changes: change
   in
   let reset_fun (f: fundec) (old_f: fundec) =
     f.svar.vid <- old_f.svar.vid;
-    List.iter2 (fun l o_l -> l.vid <- o_l.vid) f.slocals old_f.slocals;
-    List.iter2 (fun lo o_f -> lo.vid <- o_f.vid) f.sformals old_f.sformals;
+    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;
     List.iter2 (fun s o_s -> s.sid <- o_s.sid) f.sallstmts old_f.sallstmts;
     List.iter (fun s -> store_node_location (Statement s) (Cilfacade.get_stmtLoc s)) f.sallstmts;
 
diff --git a/src/util/cilMaps.ml b/src/util/cilMaps.ml
new file mode 100644
index 0000000000..d776020fc2
--- /dev/null
+++ b/src/util/cilMaps.ml
@@ -0,0 +1,11 @@
+open Cil
+
+module VarinfoOrdered = struct
+  type t = varinfo
+
+  (*x.svar.uid cannot be used, as they may overlap between old and now AST*)
+  let compare (x: varinfo) (y: varinfo) = String.compare x.vname y.vname
+end
+
+
+module VarinfoMap = Map.Make(VarinfoOrdered)
diff --git a/src/util/server.ml b/src/util/server.ml
index 40fa77da9f..fa2f8a0453 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -117,7 +117,7 @@ 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: Cil.global) _ _ = match glob with
+  let eq (glob: Cil.global) _ _ _ = match glob with
     | GFun (fdec, _) -> not (CompareCIL.should_reanalyze fdec), false, None
     | _ -> true, false, None
   in
diff --git a/tests/incremental/04-var-rename/01-unused_rename.c b/tests/incremental/04-var-rename/01-unused_rename.c
new file mode 100644
index 0000000000..31eacd5bf9
--- /dev/null
+++ b/tests/incremental/04-var-rename/01-unused_rename.c
@@ -0,0 +1,4 @@
+int main() {
+    int a = 0;
+    return 0;
+}
diff --git a/tests/incremental/04-var-rename/01-unused_rename.json b/tests/incremental/04-var-rename/01-unused_rename.json
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/01-unused_rename.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/01-unused_rename.patch b/tests/incremental/04-var-rename/01-unused_rename.patch
new file mode 100644
index 0000000000..977470ad53
--- /dev/null
+++ b/tests/incremental/04-var-rename/01-unused_rename.patch
@@ -0,0 +1,8 @@
+--- 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
new file mode 100644
index 0000000000..a317916ad1
--- /dev/null
+++ b/tests/incremental/04-var-rename/01-unused_rename.txt
@@ -0,0 +1,3 @@
+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.c b/tests/incremental/04-var-rename/02-rename_and_shuffle.c
new file mode 100644
index 0000000000..9917738055
--- /dev/null
+++ b/tests/incremental/04-var-rename/02-rename_and_shuffle.c
@@ -0,0 +1,11 @@
+#include<stdio.h>
+
+//a is renamed to c, but the usage of a is replaced by b
+int main() {
+    int a = 0;
+    int b = 1;
+
+    printf("Print %d", a);
+
+    return 0;
+}
diff --git a/tests/incremental/04-var-rename/02-rename_and_shuffle.json b/tests/incremental/04-var-rename/02-rename_and_shuffle.json
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/02-rename_and_shuffle.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/02-rename_and_shuffle.patch b/tests/incremental/04-var-rename/02-rename_and_shuffle.patch
new file mode 100644
index 0000000000..5c1dc4785e
--- /dev/null
+++ b/tests/incremental/04-var-rename/02-rename_and_shuffle.patch
@@ -0,0 +1,15 @@
+--- 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
new file mode 100644
index 0000000000..8c0ab5ac05
--- /dev/null
+++ b/tests/incremental/04-var-rename/02-rename_and_shuffle.txt
@@ -0,0 +1,2 @@
+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/03-rename_with_usage.c
new file mode 100644
index 0000000000..2c93c487d8
--- /dev/null
+++ b/tests/incremental/04-var-rename/03-rename_with_usage.c
@@ -0,0 +1,11 @@
+#include<stdio.h>
+
+//a is renamed to c, but its usages stay the same
+int main() {
+    int a = 0;
+    int b = 1;
+
+    printf("Print %d", a);
+
+    return 0;
+}
diff --git a/tests/incremental/04-var-rename/03-rename_with_usage.json b/tests/incremental/04-var-rename/03-rename_with_usage.json
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/03-rename_with_usage.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/03-rename_with_usage.patch b/tests/incremental/04-var-rename/03-rename_with_usage.patch
new file mode 100644
index 0000000000..26fb98b340
--- /dev/null
+++ b/tests/incremental/04-var-rename/03-rename_with_usage.patch
@@ -0,0 +1,15 @@
+--- tests/incremental/04-var-rename/03-rename_with_usage.c
++++ tests/incremental/04-var-rename/03-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/03-rename_with_usage.txt b/tests/incremental/04-var-rename/03-rename_with_usage.txt
new file mode 100644
index 0000000000..18ff7e94d4
--- /dev/null
+++ b/tests/incremental/04-var-rename/03-rename_with_usage.txt
@@ -0,0 +1,2 @@
+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/04-renamed_assert.c
new file mode 100644
index 0000000000..4a4a9e7f21
--- /dev/null
+++ b/tests/incremental/04-var-rename/04-renamed_assert.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main() {
+    int myVar = 0;
+    
+    assert(myVar < 11);
+
+    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_assert.json
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/04-renamed_assert.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/04-renamed_assert.patch b/tests/incremental/04-var-rename/04-renamed_assert.patch
new file mode 100644
index 0000000000..9644dcf6a1
--- /dev/null
+++ b/tests/incremental/04-var-rename/04-renamed_assert.patch
@@ -0,0 +1,13 @@
+--- tests/incremental/04-var-rename/04-renamed_assert.c
++++ tests/incremental/04-var-rename/04-renamed_assert.c
+@@ -1,7 +1,7 @@
+ int main() {
+-    int myVar = 0;
++    int myRenamedVar = 0;
+     
+-    assert(myVar < 11);
++    assert(myRenamedVar < 11);
+ 
+     return 0;
+ }
+\ Kein Zeilenumbruch am Dateiende.
diff --git a/tests/incremental/04-var-rename/04-renamed_assert.txt b/tests/incremental/04-var-rename/04-renamed_assert.txt
new file mode 100644
index 0000000000..1afc289347
--- /dev/null
+++ b/tests/incremental/04-var-rename/04-renamed_assert.txt
@@ -0,0 +1,2 @@
+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/05-renamed_param.c
new file mode 100644
index 0000000000..72fdfaf0e9
--- /dev/null
+++ b/tests/incremental/04-var-rename/05-renamed_param.c
@@ -0,0 +1,8 @@
+void method(int a) {
+    int c = a;
+}
+
+int main() {
+    method(0);
+    return 0;
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/05-renamed_param.json b/tests/incremental/04-var-rename/05-renamed_param.json
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/05-renamed_param.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/05-renamed_param.patch b/tests/incremental/04-var-rename/05-renamed_param.patch
new file mode 100644
index 0000000000..944566b05c
--- /dev/null
+++ b/tests/incremental/04-var-rename/05-renamed_param.patch
@@ -0,0 +1,10 @@
+--- 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
new file mode 100644
index 0000000000..09bca47979
--- /dev/null
+++ b/tests/incremental/04-var-rename/05-renamed_param.txt
@@ -0,0 +1,2 @@
+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/06-renamed_param_usage_changed.c
new file mode 100644
index 0000000000..aed642566c
--- /dev/null
+++ b/tests/incremental/04-var-rename/06-renamed_param_usage_changed.c
@@ -0,0 +1,11 @@
+//This test should mark foo and main as changed
+
+void foo(int a, int b) {
+    int x = a;
+    int y = b;
+}
+
+int main() {
+    foo(3, 4);
+    return 0;
+}
\ No newline at end of file
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
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/06-renamed_param_usage_changed.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/06-renamed_param_usage_changed.patch b/tests/incremental/04-var-rename/06-renamed_param_usage_changed.patch
new file mode 100644
index 0000000000..a93e45c4c5
--- /dev/null
+++ b/tests/incremental/04-var-rename/06-renamed_param_usage_changed.patch
@@ -0,0 +1,10 @@
+--- tests/incremental/04-var-rename/06-renamed_param_usage_changed.c
++++ tests/incremental/04-var-rename/06-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;
+     int y = b;
+ }
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
new file mode 100644
index 0000000000..0dc90594c7
--- /dev/null
+++ b/tests/incremental/04-var-rename/06-renamed_param_usage_changed.txt
@@ -0,0 +1,2 @@
+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/multiple_incremental_runs/08-2_incremental_runs.json b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs.json
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.c b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.c
new file mode 100644
index 0000000000..e522ad239a
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main() {
+    int varFirstIteration = 0;
+    
+    varFirstIteration++;
+    
+    assert(varFirstIteration < 10);
+    return 0;
+}
diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.patch b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.patch
new file mode 100644
index 0000000000..191b335f3c
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.patch
@@ -0,0 +1,14 @@
+--- tests/incremental/04-var-rename/08-2_incremental_runs_1.c
++++ tests/incremental/04-var-rename/08-2_incremental_runs_1.c
+@@ -1,8 +1,8 @@
+ int main() {
+-    int varFirstIteration = 0;
++    int varSecondIteration = 0;
+     
+-    varFirstIteration++;
++    varSecondIteration++;
+     
+-    assert(varFirstIteration < 10);
++    assert(varSecondIteration < 10);
+     return 0;
+ }
diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_2.patch b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_2.patch
new file mode 100644
index 0000000000..0952f3a4bf
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_2.patch
@@ -0,0 +1,14 @@
+--- tests/incremental/04-var-rename/08-2_incremental_runs_1.c
++++ tests/incremental/04-var-rename/08-2_incremental_runs_1.c
+@@ -1,8 +1,8 @@
+ int main() {
+-    int varSecondIteration = 0;
++    int varThirdIteration = 0;
+     
+-    varSecondIteration++;
++    varThirdIteration++;
+     
+-    assert(varSecondIteration < 10);
++    assert(varThirdIteration < 10);
+     return 0;
+ }
diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes.json b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes.json
new file mode 100644
index 0000000000..544b7b4ddd
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes.json
@@ -0,0 +1,3 @@
+{
+    
+}
\ No newline at end of file
diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.c b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.c
new file mode 100644
index 0000000000..e50f6d9beb
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+void foo() {
+    int fooOne = 1;
+    fooOne++;
+    assert(fooOne == 2);
+}
+
+void bar() {
+    int barOne = 10;
+    if (barOne < 11) barOne = 20;
+    assert(barOne == 20);
+}
+
+int main() {
+    foo();
+    bar();
+    return 0;
+}
diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.patch b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.patch
new file mode 100644
index 0000000000..c640034ea4
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.patch
@@ -0,0 +1,23 @@
+--- tests/incremental/04-var-rename/09-2_ir_with_changes_1.c
++++ tests/incremental/04-var-rename/09-2_ir_with_changes_1.c
+@@ -1,13 +1,14 @@
+ void foo() {
+-    int fooOne = 1;
+-    fooOne++;
+-    assert(fooOne == 2);
++    int fooTwo = 1;
++    fooTwo++;
++    assert(fooTwo == 2);
+ }
+ 
+ void bar() {
+-    int barOne = 10;
+-    if (barOne < 11) barOne = 20;
+-    assert(barOne == 20);
++    int barTwo = 10;
++    int x = 3;
++    if (x < 11) barTwo = 13;
++    assert(x > 1);
+ }
+ 
+ int main() {
diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_2.patch b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_2.patch
new file mode 100644
index 0000000000..ad44fd2303
--- /dev/null
+++ b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_2.patch
@@ -0,0 +1,13 @@
+--- tests/incremental/04-var-rename/09-2_ir_with_changes_1.c
++++ tests/incremental/04-var-rename/09-2_ir_with_changes_1.c
+@@ -1,7 +1,7 @@
+ void foo() {
+-    int fooTwo = 1;
+-    fooTwo++;
+-    assert(fooTwo == 2);
++    int fooThree = 1;
++    fooThree++;
++    assert(fooThree == 2);
+ }
+ 
+ void bar() {