diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 1e8de2aed5..bdc137591f 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -487,6 +487,15 @@ type increment_data = {
   restarting: VarQuery.t list;
 }
 
+(** Abstract incremental change to constraint system.
+    @param 'v constrain system variable type *)
+type 'v sys_change_info = {
+  obsolete: 'v list; (** Variables to destabilize. *)
+  delete: 'v list; (** Variables to delete. *)
+  reluctant: 'v list; (** Variables to solve reluctantly. *)
+  restart: 'v list; (** Variables to restart. *)
+}
+
 (** A side-effecting system. *)
 module type MonSystem =
 sig
@@ -506,10 +515,8 @@ sig
   (** The system in functional form. *)
   val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m
 
-  (** Data used for incremental analysis *)
-  val increment : increment_data option
-
-  val iter_vars: (v -> d) -> VarQuery.t -> v VarQuery.f -> unit
+  val sys_change: (v -> d) -> v sys_change_info
+  (** Compute incremental constraint system change from old solution. *)
 end
 
 (** Any system of side-effecting equations over lattices. *)
@@ -523,9 +530,8 @@ sig
 
   module D : Lattice.S
   module G : Lattice.S
-  val increment : increment_data option
   val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option
-  val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
+  val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info
 end
 
 (** A solver is something that can translate a system into a solution (hash-table).
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 9fbc432d7f..a944df5375 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -437,6 +437,39 @@ sig
   val increment: increment_data option
 end
 
+(** Combined variables so that we can also use the more common [EqConstrSys]
+    that uses only one kind of a variable. *)
+module Var2 (LV:VarType) (GV:VarType)
+  : VarType
+    with type t = [ `L of LV.t  | `G of GV.t ]
+=
+struct
+  type t = [ `L of LV.t  | `G of GV.t ] [@@deriving eq, ord, hash]
+  let relift = function
+    | `L x -> `L (LV.relift x)
+    | `G x -> `G (GV.relift x)
+
+  let pretty_trace () = function
+    | `L a -> LV.pretty_trace () a
+    | `G a -> GV.pretty_trace () a
+
+  let printXml f = function
+    | `L a -> LV.printXml f a
+    | `G a -> GV.printXml f a
+
+  let var_id = function
+    | `L a -> LV.var_id a
+    | `G a -> GV.var_id a
+
+  let node = function
+    | `L a -> LV.node a
+    | `G a -> GV.node a
+
+  let is_write_only = function
+    | `L a -> LV.is_write_only a
+    | `G a -> GV.is_write_only a
+end
+
 (** The main point of this file---generating a [GlobConstrSys] from a [Spec]. *)
 module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment)
   : sig
@@ -460,9 +493,6 @@ struct
      1. S.V -> S.G  --  used for Spec
      2. fundec -> set of S.C  --  used for IterSysVars Node *)
 
-  (* Dummy module. No incremental analysis supported here*)
-  let increment = I.increment
-
   let sync ctx =
     match Cfg.prev ctx.prev_node with
     | _ :: _ :: _ -> S.sync ctx `Join
@@ -783,6 +813,135 @@ struct
         ) cs
     | _ ->
       ()
+
+  let sys_change getl getg =
+    let open CompareCIL in
+
+    let c = match I.increment with
+      | 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));
+
+    let changed_funs = List.filter_map (function
+        | {old = {def = Some (Fun f); _}; diff = None; _} ->
+          print_endline ("Completely changed function: " ^ f.svar.vname);
+          Some f
+        | _ -> None
+      ) c.changed
+    in
+    let part_changed_funs = List.filter_map (function
+        | {old = {def = Some (Fun f); _}; diff = Some nd; _} ->
+          print_endline ("Partially changed function: " ^ f.svar.vname);
+          Some (f, nd.primObsoleteNodes, nd.unchangedNodes)
+        | _ -> None
+      ) c.changed
+    in
+    let removed_funs = List.filter_map (function
+        | {def = Some (Fun f); _} ->
+          print_endline ("Removed function: " ^ f.svar.vname);
+          Some f
+        | _ -> None
+      ) c.removed
+    in
+
+    let module HM = Hashtbl.Make (Var2 (LVar) (GVar)) in
+
+    let mark_node hm f node =
+      iter_vars getl getg (Node {node; fundec = Some f}) (fun v ->
+          HM.replace hm (`L v) ()
+        ) (fun v ->
+          HM.replace hm (`G v) ()
+        )
+    in
+
+    let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in
+    let reanalyze_entry f =
+      (* destabilize the entry points of a changed function when reluctant is off,
+         or the function is to be force-reanalyzed  *)
+      (not reluctant) || CompareCIL.VarinfoSet.mem f.svar c.exclude_from_rel_destab
+    in
+    let obsolete_ret = HM.create 103 in
+    let obsolete_entry = HM.create 103 in
+    let obsolete_prim = HM.create 103 in
+
+    (* When reluctant is on:
+       Only add function entry nodes to obsolete_entry if they are in force-reanalyze *)
+    List.iter (fun f ->
+        if reanalyze_entry f then
+          (* collect function entry for eager destabilization *)
+          mark_node obsolete_entry f (FunctionEntry f)
+        else
+          (* collect function return for reluctant analysis *)
+          mark_node obsolete_ret f (Function f)
+      ) changed_funs;
+    (* Primary changed unknowns from partially changed functions need only to be collected for eager destabilization when reluctant is off *)
+    (* The return nodes of partially changed functions are collected in obsolete_ret for reluctant analysis *)
+    (* We utilize that force-reanalyzed functions are always considered as completely changed (and not partially changed) *)
+    List.iter (fun (f, pn, _) ->
+        if not reluctant then (
+          List.iter (fun n ->
+              mark_node obsolete_prim f n
+            ) pn
+        )
+        else
+          mark_node obsolete_ret f (Function f)
+      ) part_changed_funs;
+
+    let obsolete = Enum.append (HM.keys obsolete_entry) (HM.keys obsolete_prim) |> List.of_enum in
+    let reluctant = HM.keys obsolete_ret |> List.of_enum in
+
+    let marked_for_deletion = HM.create 103 in
+
+    let dummy_pseudo_return_node f =
+      (* not the same as in CFG, but compares equal because of sid *)
+      Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f})
+    in
+    let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) =
+      let add_stmts (f: fundec) =
+        List.iter (fun s ->
+            mark_node marked_for_deletion f (Statement s)
+          ) f.sallstmts
+      in
+      List.iter (fun f ->
+          if withEntry f then
+            mark_node marked_for_deletion f (FunctionEntry f);
+          mark_node marked_for_deletion f (Function f);
+          add_stmts f;
+          mark_node marked_for_deletion f (dummy_pseudo_return_node f)
+        ) functions;
+    in
+
+    add_nodes_of_fun changed_funs reanalyze_entry;
+    add_nodes_of_fun removed_funs (fun _ -> true);
+    (* it is necessary to remove all unknowns for changed pseudo-returns because they have static ids *)
+    let add_pseudo_return f un =
+      let pseudo = dummy_pseudo_return_node f in
+      if not (List.exists (Node.equal pseudo % fst) un) then
+        mark_node marked_for_deletion f (dummy_pseudo_return_node f)
+    in
+    List.iter (fun (f,_,un) ->
+        mark_node marked_for_deletion f (Function f);
+        add_pseudo_return f un
+      ) part_changed_funs;
+
+    let delete = HM.keys marked_for_deletion |> List.of_enum in
+
+    let restart = match I.increment with
+      | Some data ->
+        let restart = ref [] in
+        List.iter (fun g ->
+            iter_vars getl getg g (fun v ->
+                restart := `L v :: !restart
+              ) (fun v ->
+                restart := `G v :: !restart
+              )
+          ) data.restarting;
+        !restart
+      | None -> []
+    in
+
+    {obsolete; delete; reluctant; restart}
 end
 
 (** Convert a non-incremental solver into an "incremental" solver.
@@ -803,38 +962,6 @@ module EqIncrSolverFromEqSolver (Sol: GenericEqBoxSolver): GenericEqBoxIncrSolve
       (vh, ())
   end
 
-(** Combined variables so that we can also use the more common [EqConstrSys]
-    that uses only one kind of a variable. *)
-module Var2 (LV:VarType) (GV:VarType)
-  : VarType
-    with type t = [ `L of LV.t  | `G of GV.t ]
-=
-struct
-  type t = [ `L of LV.t  | `G of GV.t ] [@@deriving eq, ord, hash]
-  let relift = function
-    | `L x -> `L (LV.relift x)
-    | `G x -> `G (GV.relift x)
-
-  let pretty_trace () = function
-    | `L a -> LV.pretty_trace () a
-    | `G a -> GV.pretty_trace () a
-
-  let printXml f = function
-    | `L a -> LV.printXml f a
-    | `G a -> GV.printXml f a
-
-  let var_id = function
-    | `L a -> LV.var_id a
-    | `G a -> GV.var_id a
-
-  let node = function
-    | `L a -> LV.node a
-    | `G a -> GV.node a
-
-  let is_write_only = function
-    | `L a -> LV.is_write_only a
-    | `G a -> GV.is_write_only a
-end
 
 (** Translate a [GlobConstrSys] into a [EqConstrSys] *)
 module EqConstrSysFromGlobConstrSys (S:GlobConstrSys)
@@ -853,7 +980,6 @@ struct
       | `Lifted2 a -> S.D.printXml f a
       | (`Bot | `Top) as x -> printXml f x
   end
-  let increment = S.increment
   type v = Var.t
   type d = Dom.t
 
@@ -883,8 +1009,8 @@ struct
     | `G _ -> None
     | `L x -> Option.map conv (S.system x)
 
-  let iter_vars get vq f =
-    S.iter_vars (getL % get % l) (getG % get % g) vq (f % l) (f % g)
+  let sys_change get =
+    S.sys_change (getL % get % l) (getG % get % g)
 end
 
 (** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index d1cebebe43..caf2cd2bab 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -11,10 +11,7 @@
 
 open Prelude
 open Analyses
-open Constraints
 open Messages
-open CompareCIL
-open GoblintCil
 
 module WP =
   functor (Arg: IncrSolverArg) ->
@@ -212,6 +209,8 @@ module WP =
          These don't have to be re-verified and warnings can be reused. *)
       let superstable = HM.copy stable in
 
+      let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in
+
       let var_messages = data.var_messages in
       let rho_write = data.rho_write in
       let dep = data.dep in
@@ -467,11 +466,6 @@ module WP =
       let restart_write_only = GobConfig.get_bool "incremental.restart.write-only" in
 
       if GobConfig.get_bool "incremental.load" then (
-        let c = match S.increment with
-          | 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));
 
         let restart_leaf x =
           if tracing then trace "sol2" "Restarting to bot %a\n" S.Var.pretty_trace x;
@@ -510,7 +504,7 @@ module WP =
             | _, is_write_only ->
               match restart_vars with
               | "all" -> true
-              | "global" -> Node.equal (S.Var.node x) (Function Cil.dummyFunDec) (* non-function entry node *)
+              | "global" -> Node.equal (S.Var.node x) (Function GoblintCil.dummyFunDec) (* non-function entry node *)
               | "write-only" -> is_write_only
               | _ -> assert false
           in
@@ -542,7 +536,7 @@ module WP =
           (* destabilize side infl *)
           if side_fuel <> Some 0 then ( (* non-0 or infinite fuel is fine *)
             let side_fuel' =
-              if not restart_fuel_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec) then
+              if not restart_fuel_only_globals || Node.equal (S.Var.node x) (Function GoblintCil.dummyFunDec) then
                 Option.map Int.pred side_fuel
               else
                 side_fuel (* don't decrease fuel for function entry side effect *)
@@ -570,128 +564,30 @@ module WP =
           else
             destabilize_normal;
 
-        let changed_funs = List.filter_map (function
-            | {old = {def = Some (Fun f); _}; diff = None; _} ->
-              print_endline ("Completely changed function: " ^ f.svar.vname);
-              Some f
-            | _ -> None
-          ) c.changed
-        in
-        let part_changed_funs = List.filter_map (function
-            | {old = {def = Some (Fun f); _}; diff = Some nd; _} ->
-              print_endline ("Partially changed function: " ^ f.svar.vname);
-              Some (f, nd.primObsoleteNodes, nd.unchangedNodes)
-            | _ -> None
-          ) c.changed
-        in
-        let removed_funs = List.filter_map (function
-            | {def = Some (Fun f); _} ->
-              print_endline ("Removed function: " ^ f.svar.vname);
-              Some f
-            | _ -> None
-          ) c.removed
-        in
-
-        let mark_node hm f node =
-          let get x = try HM.find rho x with Not_found -> S.Dom.bot () in
-          S.iter_vars get (Node {node; fundec = Some f}) (fun v ->
-              HM.replace hm v ()
-            )
-        in
-
-        let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in
-        let reanalyze_entry f =
-          (* destabilize the entry points of a changed function when reluctant is off,
-             or the function is to be force-reanalyzed  *)
-          (not reluctant) || CompareCIL.VarinfoSet.mem f.svar c.exclude_from_rel_destab
-        in
-        let obsolete_ret = HM.create 103 in
-        let obsolete_entry = HM.create 103 in
-        let obsolete_prim = HM.create 103 in
-
-        (* When reluctant is on:
-           Only add function entry nodes to obsolete_entry if they are in force-reanalyze *)
-        List.iter (fun f ->
-            if reanalyze_entry f then
-              (* collect function entry for eager destabilization *)
-              mark_node obsolete_entry f (FunctionEntry f)
-            else
-              (* collect function return for reluctant analysis *)
-              mark_node obsolete_ret f (Function f)
-          ) changed_funs;
-        (* Primary changed unknowns from partially changed functions need only to be collected for eager destabilization when reluctant is off *)
-        (* The return nodes of partially changed functions are collected in obsolete_ret for reluctant analysis *)
-        (* We utilize that force-reanalyzed functions are always considered as completely changed (and not partially changed) *)
-        List.iter (fun (f, pn, _) ->
-            if not reluctant then (
-              List.iter (fun n ->
-                  mark_node obsolete_prim f n
-                ) pn;
-            ) else (
-              mark_node obsolete_ret f (Function f);
-            )
-          ) part_changed_funs;
+        let sys_change = S.sys_change (fun v -> try HM.find rho v with Not_found -> S.Dom.bot ()) in
 
         let old_ret = HM.create 103 in
         if reluctant then (
           (* save entries of changed functions in rho for the comparison whether the result has changed after a function specific solve *)
-          HM.iter (fun k v ->
+          List.iter (fun k ->
               if HM.mem rho k then (
                 let old_rho = HM.find rho k in
                 let old_infl = HM.find_default infl k VS.empty in
                 HM.replace old_ret k (old_rho, old_infl)
               )
-            ) obsolete_ret;
+            ) sys_change.reluctant;
         );
 
-        if not (HM.is_empty obsolete_entry) || not (HM.is_empty obsolete_prim) then
+        if sys_change.obsolete <> [] then
           print_endline "Destabilizing changed functions and primary old nodes ...";
-        HM.iter (fun k _ ->
+        List.iter (fun k ->
             if HM.mem stable k then
               destabilize k
-          ) obsolete_entry;
-        HM.iter (fun k _ ->
-            if HM.mem stable k then
-              destabilize k
-          ) obsolete_prim;
+          ) sys_change.obsolete;
 
         (* We remove all unknowns for program points in changed or removed functions from rho, stable, infl and wpoint *)
-        let marked_for_deletion = HM.create 103 in
-
-        let dummy_pseudo_return_node f =
-          (* not the same as in CFG, but compares equal because of sid *)
-          Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f})
-        in
-        let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) =
-          let add_stmts (f: fundec) =
-            List.iter (fun s ->
-                mark_node marked_for_deletion f (Statement s)
-              ) f.sallstmts
-          in
-          List.iter (fun f ->
-              if withEntry f then
-                mark_node marked_for_deletion f (FunctionEntry f);
-              mark_node marked_for_deletion f (Function f);
-              add_stmts f;
-              mark_node marked_for_deletion f (dummy_pseudo_return_node f)
-            ) functions;
-        in
-
-        add_nodes_of_fun changed_funs reanalyze_entry;
-        add_nodes_of_fun removed_funs (fun _ -> true);
-        (* it is necessary to remove all unknowns for changed pseudo-returns because they have static ids *)
-        let add_pseudo_return f un =
-          let pseudo = dummy_pseudo_return_node f in
-          if not (List.exists (Node.equal pseudo % fst) un) then
-            mark_node marked_for_deletion f (dummy_pseudo_return_node f)
-        in
-        List.iter (fun (f,_,un) ->
-            mark_node marked_for_deletion f (Function f);
-            add_pseudo_return f un
-          ) part_changed_funs;
-
         print_endline "Removing data for changed and removed functions...";
-        let delete_marked s = HM.iter (fun k _ -> HM.remove s k) marked_for_deletion in
+        let delete_marked s = List.iter (fun k -> HM.remove s k) sys_change.delete in
         delete_marked rho;
         delete_marked infl; (* TODO: delete from inner sets? *)
         delete_marked wpoint;
@@ -701,12 +597,12 @@ module WP =
         if restart_sided then (
           (* restarts old copies of functions and their (removed) side effects *)
           print_endline "Destabilizing sides of changed functions, primary old nodes and removed functions ...";
-          HM.iter (fun k _ ->
+          List.iter (fun k ->
               if HM.mem stable k then (
                 ignore (Pretty.printf "marked %a\n" S.Var.pretty_trace k);
                 destabilize k
               )
-            ) marked_for_deletion
+            ) sys_change.delete
         );
 
         (* [destabilize_leaf] is meant for restarting of globals selected by the user. *)
@@ -731,22 +627,13 @@ module WP =
           destabilize_normal x
 
         in
-        let globals_to_restart = match S.increment with
-          | Some {restarting; _} -> restarting
-          | None -> []
-        in
-        let get x = try HM.find rho x with Not_found -> S.Dom.bot () in
-
-        List.iter
-          (fun g ->
-             S.iter_vars get g
-               (fun v ->
-                  if S.system v <> None then
-                    ignore @@ Pretty.printf "Trying to restart non-leaf unknown %a. This has no effect.\n" S.Var.pretty_trace v
-                  else if HM.mem stable v then
-                    destabilize_leaf v)
-          )
-          globals_to_restart;
+
+        List.iter (fun v ->
+            if S.system v <> None then
+              ignore @@ Pretty.printf "Trying to restart non-leaf unknown %a. This has no effect.\n" S.Var.pretty_trace v
+            else if HM.mem stable v then
+              destabilize_leaf v
+          ) sys_change.restart;
 
         let restart_and_destabilize x = (* destabilize_with_side doesn't restart x itself *)
           restart_leaf x;
diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml
index 38316eeae9..47ec5443ca 100644
--- a/unittest/solver/solverTest.ml
+++ b/unittest/solver/solverTest.ml
@@ -29,8 +29,6 @@ module ConstrSys = struct
   module D = Int
   module G = IntR
 
-  let increment = None
-
   (*
     1. x := g
     2. y := 8
@@ -45,6 +43,7 @@ module ConstrSys = struct
     | _   -> None
 
   let iter_vars _ _ _ _ _ = ()
+  let sys_change _ _ = {Analyses.obsolete = []; delete = []; reluctant = []; restart = []}
 end
 
 module LH = BatHashtbl.Make (ConstrSys.LVar)