diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index ad05295de2..edd251b66f 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -62,7 +62,7 @@ jobs:
         if: always()
         with:
           name: suite_result-${{ matrix.os }}
-          path: tests/suite_result/
+          path: _build/default/tests/suite_result/
 
   extraction:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
diff --git a/goblint.opam b/goblint.opam
index fa0e4f3c19..c8c4ce4e59 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -78,7 +78,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 8c9e914575..f8de683948 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -134,7 +134,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5"
+    "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f"
   ]
   [
     "ppx_deriving.5.2.1"
diff --git a/goblint.opam.template b/goblint.opam.template
index 1364586310..2d5ef10bc9 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -3,7 +3,7 @@
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]
diff --git a/gobview b/gobview
index 74e2958708..b33fd0b389 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 74e295870848c66885fa446970b0c59617a242a7
+Subproject commit b33fd0b3894d455a0a65791f4cfdf50f4426f863
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index a56400a712..4cf4f11be2 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -115,7 +115,7 @@ struct
   let invariant_fallback ctx st exp tv =
     (* We use a recursive helper function so that x != 0 is false can be handled
      * as x == 0 is true etc *)
-    let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): (lval * VD.t) option =
+    let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): [> `Refine of lval * VD.t | `NotUnderstood] =
       match (op, lval, value, tv) with
       (* The true-branch where x == value: *)
       | Eq, x, value, true ->
@@ -123,8 +123,8 @@ struct
         (match value with
          | Int n ->
            let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-           Some (x, Int (ID.cast_to ikind n))
-         | _ -> Some(x, value))
+           `Refine (x, Int (ID.cast_to ikind n))
+         | _ -> `Refine (x, value))
       (* The false-branch for x == value: *)
       | Eq, x, value, false -> begin
           match value with
@@ -134,26 +134,26 @@ struct
                 (* When x != n, we can return a singleton exclusion set *)
                 if M.tracing then M.tracec "invariant" "Yes, %a is not %a" d_lval x GobZ.pretty n;
                 let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-                Some (x, Int (ID.of_excl_list ikind [n]))
-              | None -> None
+                `Refine (x, Int (ID.of_excl_list ikind [n]))
+              | None -> `NotUnderstood
             end
           | Address n -> begin
               if M.tracing then M.tracec "invariant" "Yes, %a is not %a" d_lval x AD.pretty n;
               match eval_rv_address ~ctx st (Lval x) with
               | Address a when AD.is_definite n ->
-                Some (x, Address (AD.diff a n))
+                `Refine (x, Address (AD.diff a n))
               | Top when AD.is_null n ->
-                Some (x, Address AD.not_null)
+                `Refine (x, Address AD.not_null)
               | v ->
                 if M.tracing then M.tracec "invariant" "No address invariant for: %a != %a" VD.pretty v AD.pretty n;
-                None
+                `NotUnderstood
             end
-          (* | Address a -> Some (x, value) *)
+          (* | Address a -> `Refine (x, value) *)
           | _ ->
             (* We can't say anything else, exclusion sets are finite, so not
              * being in one means an infinite number of values *)
             if M.tracing then M.tracec "invariant" "Failed! (not a definite value)";
-            None
+            `NotUnderstood
         end
       | Ne, x, value, _ -> helper Eq x value (not tv)
       | Lt, x, value, _ -> begin
@@ -166,10 +166,10 @@ struct
               match limit_from n with
               | Some n ->
                 if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" d_lval x GobZ.pretty n;
-                Some (x, Int (range_from n))
-              | None -> None
+                `Refine (x, Int (range_from n))
+              | None -> `NotUnderstood
             end
-          | _ -> None
+          | _ -> `NotUnderstood
         end
       | Le, x, value, _ -> begin
           match value with
@@ -181,16 +181,16 @@ struct
               match limit_from n with
               | Some n ->
                 if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" d_lval x GobZ.pretty n;
-                Some (x, Int (range_from n))
-              | None -> None
+                `Refine (x, Int (range_from n))
+              | None -> `NotUnderstood
             end
-          | _ -> None
+          | _ -> `NotUnderstood
         end
       | Gt, x, value, _ -> helper Le x value (not tv)
       | Ge, x, value, _ -> helper Lt x value (not tv)
       | _ ->
         if M.tracing then M.trace "invariant" "Failed! (operation not supported)";
-        None
+        `NotUnderstood
     in
     if M.tracing then M.traceli "invariant" "assume expression %a is %B" d_exp exp tv;
     let null_val (typ:typ):VD.t =
@@ -199,7 +199,7 @@ struct
       | TEnum({ekind=_;_},_)
       | _                         -> Int (ID.of_int (Cilfacade.get_ikind typ) Z.zero)
     in
-    let rec derived_invariant exp tv =
+    let rec derived_invariant exp tv: [`Refine of lval * VD.t | `NothingToRefine | `NotUnderstood] =
       let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *)
       match exp with
       (* Since we handle not only equalities, the order is important *)
@@ -208,18 +208,22 @@ struct
       | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
       | BinOp(op, CastE (TInt (ik, _) as t1, Lval x), rval, typ) ->
-        (match eval_rv ~ctx st (Lval x) with
-         | Int v ->
-           (* This is tricky: It it is not sufficient to check that ID.cast_to_ik v = v
-             * If there is one domain that knows this to be true and the other does not, we
-             * should still impose the invariant. E.g. i -> ([1,5]; Not {0}[byte]) *)
-           if VD.is_safe_cast t1 (Cilfacade.typeOfLval x) then
-             derived_invariant (BinOp (op, Lval x, rval, typ)) tv
-           else
-             None
-         | _ -> None)
+        begin match eval_rv ~ctx st (Lval x) with
+          | Int v ->
+            (* This is tricky: It it is not sufficient to check that ID.cast_to_ik v = v
+               If there is one domain that knows this to be true and the other does not, we
+               should still impose the invariant. E.g. i -> ([1,5]; Not {0}[byte]) *)
+            if VD.is_safe_cast t1 (Cilfacade.typeOfLval x) then
+              derived_invariant (BinOp (op, Lval x, rval, typ)) tv
+            else
+              `NotUnderstood
+          | _ -> `NotUnderstood
+        end
       | BinOp(op, rval, CastE (TInt (_, _) as ti, Lval x), typ) ->
         derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv
+      | BinOp(op, (Const _ | AddrOf _), rval, typ) ->
+        (* This is last such that we never reach here with rval being Lval (it is swapped around). *)
+        `NothingToRefine
       (* Cases like if (x) are treated like if (x != 0) *)
       | Lval x ->
         (* There are two correct ways of doing it: "if ((int)x != 0)" or "if (x != (typeof(x))0))"
@@ -228,12 +232,15 @@ struct
       | UnOp (LNot,uexp,typ) -> derived_invariant uexp (not tv)
       | _ ->
         if M.tracing then M.tracec "invariant" "Failed! (expression %a not understood)" d_plainexp exp;
-        None
+        `NotUnderstood
     in
     match derived_invariant exp tv with
-    | Some (lval, value) ->
+    | `Refine (lval, value) ->
       refine_lv_fallback ctx st lval value tv
-    | None ->
+    | `NothingToRefine ->
+      if M.tracing then M.traceu "invariant" "Nothing to refine.";
+      st
+    | `NotUnderstood ->
       if M.tracing then M.traceu "invariant" "Doing nothing.";
       M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp;
       st
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index b4544812aa..527d11b1de 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -64,6 +64,43 @@ let old_threadenter (type d) ask (st: d BaseDomain.basecomponents_t) =
 let startstate_threadenter (type d) (startstate: unit -> d) ask (st: d BaseDomain.basecomponents_t) =
   {st with cpa = CPA.bot (); priv = startstate ()}
 
+
+(** Wrappers. *)
+module type PrivatizationWrapper = functor(GBase:Lattice.S) ->
+sig
+  module G: Lattice.S
+
+  val getg: Q.ask -> ('a -> G.t) -> 'a -> GBase.t
+  val sideg: Q.ask -> ('a -> G.t -> unit) -> 'a -> GBase.t -> unit
+end
+
+
+module NoWrapper:PrivatizationWrapper = functor (GBase:Lattice.S) ->
+  (struct
+    module G = GBase
+
+    let getg _ getg = getg
+    let sideg _ sideg = sideg
+  end)
+
+module DigestWrapper(Digest: Digest):PrivatizationWrapper =  functor (GBase:Lattice.S) ->
+  (struct
+    module G = MapDomain.MapBot_LiftTop (Digest) (GBase)
+
+    let getg ask getg x =
+      let vs = getg x in
+      G.fold (fun d v acc ->
+          if not (Digest.accounted_for ask ~current:(Digest.current ask) ~other:d) then
+            GBase.join v acc
+          else
+            acc) vs (GBase.bot ())
+
+    let sideg ask sideg x v =
+      let sidev = G.singleton (Digest.current ask) v in
+      sideg x sidev
+  end)
+
+
 (* No Privatization *)
 module NonePriv: S =
 struct
@@ -659,40 +696,7 @@ module ProtectionBasedV = struct
 end
 
 (** Protection-Based Reading. *)
-module type ProtectionBasedWrapper =
-sig
-  module G: Lattice.S
-
-  val getg: Q.ask -> (ProtectionBasedV.V.t -> G.t) -> ProtectionBasedV.V.t -> VD.t
-  val sideg: Q.ask -> (ProtectionBasedV.V.t -> G.t -> unit) -> ProtectionBasedV.V.t -> VD.t -> unit
-end
-
-
-module NoWrapper: ProtectionBasedWrapper =
-struct
-  module G = VD
-
-  let getg _ getg = getg
-  let sideg _ sideg = sideg
-end
-
-module DigestWrapper(Digest: Digest): ProtectionBasedWrapper = struct
-  module G = MapDomain.MapBot_LiftTop (Digest) (VD)
-
-  let getg ask getg x =
-    let vs = getg x in
-    G.fold (fun d v acc ->
-        if not (Digest.accounted_for ask ~current:(Digest.current ask) ~other:d) then
-          VD.join v acc
-        else
-          acc) vs (VD.bot ())
-
-  let sideg ask sideg x v =
-    let sidev = G.singleton (Digest.current ask) v in
-    sideg x sidev
-end
-
-module ProtectionBasedPrivWrapper (Param: PerGlobalPrivParam)(Wrapper:ProtectionBasedWrapper): S =
+module ProtectionBasedPriv (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
 struct
   include NoFinalize
   include ConfCheck.RequireMutexActivatedInit
@@ -707,6 +711,7 @@ struct
   (* W is implicitly represented by CPA domain *)
   module D = P
 
+  module Wrapper = Wrapper (VD)
   module G = Wrapper.G
   module V = ProtectionBasedV.V
 
@@ -1196,7 +1201,7 @@ struct
 end
 
 (** Lock-Centered Reading. *)
-module LockCenteredPriv: S =
+module LockCenteredPriv(Wrapper:PrivatizationWrapper): S =
 struct
   include MinePrivBase
   include LockCenteredBase
@@ -1205,24 +1210,32 @@ struct
   open LockCenteredD
   module D = Lattice.Prod (DV) (L)
 
+  module Wrapper = Wrapper (G)
+  module UnwrappedG = G
+  module G = Wrapper.G
+
+  let invariant_global ask getg = invariant_global ask (Wrapper.getg ask getg)
+  let invariant_vars ask getg = invariant_vars ask (Wrapper.getg ask getg)
+
   let startstate () = (DV.bot (), L.bot ())
 
   let lockset_init = Lockset.top ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
-      let v_init = GWeak.find lockset_init (G.weak (getg (V.global x))) in
+      let v_init = GWeak.find lockset_init (UnwrappedG.weak (getg (V.global x))) in
       VD.join v v_init
     else
       v
 
   let read_global ask getg (st: BaseComponents (D).t) x =
+    let getg = Wrapper.getg ask getg in
     let s = current_lockset ask in
     let (vv, l) = st.priv in
     let d_cpa = CPA.find x st.cpa in
     let d_sync = L.fold (fun m bs acc ->
         if not (MustVars.mem x (DV.find m vv)) then
-          let syncs = G.sync (getg (V.mutex m)) in
+          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           MinLocksets.fold (fun b acc ->
               GSync.fold (fun s' cpa' acc ->
                   if Lockset.disjoint b s' then
@@ -1236,7 +1249,7 @@ struct
           acc
       ) l (VD.bot ())
     in
-    let weaks = G.weak (getg (V.global x)) in
+    let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_weak = GWeak.fold (fun s' v acc ->
         if Lockset.disjoint s s' then
           VD.join v acc
@@ -1259,6 +1272,8 @@ struct
     d
 
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
+    let sideg = Wrapper.sideg ask sideg in
+    let getg = Wrapper.getg ask getg in
     let s = current_lockset ask in
     let (vv, l) = st.priv in
     let v' = L.fold (fun m _ acc ->
@@ -1268,7 +1283,7 @@ struct
     let cpa' = CPA.add x v st.cpa in
     if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then (
       let v = distr_init getg x v in
-      sideg (V.global x) (G.create_weak (GWeak.singleton s v))
+      sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton s v))
       (* Unlock after invariant will still side effect refined value from CPA, because cannot distinguish from non-invariant write. *)
     );
     {st with cpa = cpa'; priv = (v', l)}
@@ -1281,6 +1296,8 @@ struct
     {st with priv = (v', l')}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    let sideg = Wrapper.sideg ask sideg in
+    let getg = Wrapper.getg ask getg in
     let s = Lockset.remove m (current_lockset ask) in
     let is_in_G x _ = is_global ask x in
     let side_cpa = CPA.filter is_in_G st.cpa in
@@ -1289,7 +1306,7 @@ struct
         v
       ) side_cpa
     in
-    sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
+    sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_cpa));
     (* m stays in v, l *)
     st
 
@@ -1303,9 +1320,10 @@ struct
       st
 
   let escape ask getg sideg (st: BaseComponents (D).t) escaped =
+    let sideg = Wrapper.sideg ask sideg in
     let cpa' = CPA.fold (fun x v acc ->
         if EscapeDomain.EscapedVars.mem x escaped then (
-          sideg (V.global x) (G.create_weak (GWeak.singleton lockset_init v));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton lockset_init v));
           CPA.remove x acc
         )
         else
@@ -1315,9 +1333,10 @@ struct
     {st with cpa = cpa'}
 
   let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
+    let sideg = Wrapper.sideg ask sideg in
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_global ask x then (
-          sideg (V.global x) (G.create_weak (GWeak.singleton lockset_init v));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton lockset_init v));
           {st with cpa = CPA.remove x st.cpa}
         )
         else
@@ -1353,7 +1372,7 @@ struct
 end
 
 (** Write-Centered Reading. *)
-module WriteCenteredPriv: S =
+module WriteCenteredPriv(Wrapper:PrivatizationWrapper): S =
 struct
   include MinePrivBase
   include WriteCenteredBase
@@ -1362,25 +1381,33 @@ struct
   open WriteCenteredD
   module D = Lattice.Prod (W) (P)
 
+  module Wrapper = Wrapper(G)
+  module UnwrappedG = G
+  module G = Wrapper.G
+
+  let invariant_global ask getg = invariant_global ask (Wrapper.getg ask getg)
+  let invariant_vars ask getg = invariant_vars ask (Wrapper.getg ask getg)
+
   let startstate () = (W.bot (), P.top ())
 
   let lockset_init = Lockset.top ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
-      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (G.weak (getg (V.global x)))) in
+      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
       VD.join v v_init
     else
       v
 
   let read_global ask getg (st: BaseComponents (D).t) x =
+    let getg = Wrapper.getg ask getg in
     let s = current_lockset ask in
     let (w, p) = st.priv in
     let p_x = P.find x p in
     let d_cpa = CPA.find x st.cpa in
     let d_sync = Lockset.fold (fun m acc ->
         if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then
-          let syncs = G.sync (getg (V.mutex m)) in
+          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           GSync.fold (fun s' gsyncw' acc ->
               if Lockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
@@ -1397,7 +1424,7 @@ struct
           acc
       ) s (VD.bot ())
     in
-    let weaks = G.weak (getg (V.global x)) in
+    let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_weak = GWeak.fold (fun s' gweakw' acc ->
         if Lockset.disjoint s s' then
           GWeakW.fold (fun w' v acc ->
@@ -1417,6 +1444,8 @@ struct
     d
 
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
+    let getg = Wrapper.getg ask getg in
+    let sideg = Wrapper.sideg ask sideg in
     let s = current_lockset ask in
     let (w, p) = st.priv in
     let w' = if not invariant then
@@ -1429,7 +1458,7 @@ struct
     let cpa' = CPA.add x v st.cpa in
     if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then (
       let v = distr_init getg x v in
-      sideg (V.global x) (G.create_weak (GWeak.singleton s (GWeakW.singleton s v)))
+      sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton s (GWeakW.singleton s v)))
     );
     (* TODO: publish all g under M_g? *)
     {st with cpa = cpa'; priv = (w', p')}
@@ -1437,6 +1466,8 @@ struct
   let lock ask getg (st: BaseComponents (D).t) m = st
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    let getg = Wrapper.getg ask getg in
+    let sideg = Wrapper.sideg ask sideg in
     let s = Lockset.remove m (current_lockset ask) in
     let (w, p) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
@@ -1454,7 +1485,7 @@ struct
       ) st.cpa (GSyncW.bot ())
     in
     if M.tracing then M.traceu "priv" "unlock %a %a" Lock.pretty m GSyncW.pretty side_gsyncw;
-    sideg (V.mutex m) (G.create_sync (GSync.singleton s side_gsyncw));
+    sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_gsyncw));
     {st with priv = (w, p')}
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
@@ -1467,12 +1498,13 @@ struct
       st
 
   let escape ask getg sideg (st: BaseComponents (D).t) escaped =
+    let sideg = Wrapper.sideg ask sideg in
     let s = current_lockset ask in
     CPA.fold (fun x v acc ->
         if EscapeDomain.EscapedVars.mem x escaped then (
           let (w, p) = st.priv in
           let p' = P.add x (MinLocksets.singleton s) p in
-          sideg (V.global x) (G.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa; priv = (w, p')}
         )
         else
@@ -1480,9 +1512,10 @@ struct
       ) st.cpa st
 
   let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
+    let sideg = Wrapper.sideg ask sideg in
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_global ask x then (
-          sideg (V.global x) (G.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa}
         )
         else
@@ -1493,7 +1526,7 @@ struct
 end
 
 (** Write-Centered Reading and Lock-Centered Reading combined. *)
-module WriteAndLockCenteredPriv: S =
+module WriteAndLockCenteredPriv(Wrapper:PrivatizationWrapper): S =
 struct
   include MinePrivBase
   include WriteCenteredBase
@@ -1503,25 +1536,33 @@ struct
   open WriteCenteredD
   module D = Lattice.Prod (Lattice.Prod (W) (P)) (Lattice.Prod (DV) (L))
 
+  module Wrapper = Wrapper(G)
+  module UnwrappedG = G
+  module G = Wrapper.G
+
+  let invariant_global ask getg = invariant_global ask (Wrapper.getg ask getg)
+  let invariant_vars ask getg = invariant_vars ask (Wrapper.getg ask getg)
+
   let startstate () = ((W.bot (), P.top ()), (DV.bot (), L.bot ()))
 
   let lockset_init = Lockset.top ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
-      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (G.weak (getg (V.global x)))) in
+      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
       VD.join v v_init
     else
       v
 
   let read_global ask getg (st: BaseComponents (D).t) x =
+    let getg = Wrapper.getg ask getg in
     let s = current_lockset ask in
     let ((w, p), (vv, l)) = st.priv in
     let p_x = P.find x p in
     let d_cpa = CPA.find x st.cpa in
     let d_m_sync = L.fold (fun m bs acc ->
         if not (MustVars.mem x (DV.find m vv)) then
-          let syncs = G.sync (getg (V.mutex m)) in
+          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           MinLocksets.fold (fun b acc ->
               GSync.fold (fun s' gsyncw' acc ->
                   if Lockset.disjoint b s' then
@@ -1540,7 +1581,7 @@ struct
           acc
       ) l (VD.bot ())
     in
-    let weaks = G.weak (getg (V.global x)) in
+    let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_m_weak = GWeak.fold (fun s' gweakw' acc ->
         if Lockset.disjoint s s' then
           GWeakW.fold (fun w' v acc ->
@@ -1556,7 +1597,7 @@ struct
     let d_m = VD.join d_m_sync d_m_weak in
     let d_g_sync = Lockset.fold (fun m acc ->
         if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then
-          let syncs = G.sync (getg (V.mutex m)) in
+          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           GSync.fold (fun s' gsyncw' acc ->
               if Lockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
@@ -1579,6 +1620,8 @@ struct
     d
 
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
+    let getg = Wrapper.getg ask getg in
+    let sideg = Wrapper.sideg ask sideg in
     let s = current_lockset ask in
     let ((w, p), (vv, l)) = st.priv in
     let w' = if not invariant then
@@ -1595,7 +1638,7 @@ struct
     let cpa' = CPA.add x v st.cpa in
     if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then (
       let v = distr_init getg x v in
-      sideg (V.global x) (G.create_weak (GWeak.singleton s (GWeakW.singleton s v)))
+      sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton s (GWeakW.singleton s v)))
     );
     (* TODO: publish all g under M_g? *)
     {st with cpa = cpa'; priv = ((w', p'), (v', l))}
@@ -1608,6 +1651,8 @@ struct
     {st with priv = (wp, (v', l'))}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    let getg = Wrapper.getg ask getg in
+    let sideg = Wrapper.sideg ask sideg in
     let s = Lockset.remove m (current_lockset ask) in
     let ((w, p), vl) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
@@ -1621,7 +1666,7 @@ struct
           acc
       ) st.cpa (GSyncW.bot ())
     in
-    sideg (V.mutex m) (G.create_sync (GSync.singleton s side_gsyncw));
+    sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_gsyncw));
     (* m stays in v, l *)
     {st with priv = ((w, p'), vl)}
 
@@ -1635,12 +1680,13 @@ struct
       st
 
   let escape ask getg sideg (st: BaseComponents (D).t) escaped =
+    let sideg = Wrapper.sideg ask sideg in
     let s = current_lockset ask in
     CPA.fold (fun x v acc ->
         if EscapeDomain.EscapedVars.mem x escaped then (
           let ((w, p), (vv, l)) = st.priv in
           let p' = P.add x (MinLocksets.singleton s) p in
-          sideg (V.global x) (G.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa; priv = ((w, p'), (vv, l))}
         )
         else
@@ -1648,9 +1694,10 @@ struct
       ) st.cpa st
 
   let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
+    let sideg = Wrapper.sideg ask sideg in
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_global ask x then (
-          sideg (V.global x) (G.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa}
         )
         else
@@ -1835,19 +1882,22 @@ let priv_module: (module S) Lazy.t =
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
-        | "protection" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper))
-        | "protection-tid" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
-        | "protection-atomic" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *)
-        | "protection-read" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper))
-        | "protection-read-tid" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
-        | "protection-read-atomic" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *)
+        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper))
+        | "protection-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
+        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *)
+        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper))
+        | "protection-read-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
+        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *)
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))
         | "mine-W-noinit" -> (module MineWPriv (struct let side_effect_global_init = false end))
-        | "lock" -> (module LockCenteredPriv)
-        | "write" -> (module WriteCenteredPriv)
-        | "write+lock" -> (module WriteAndLockCenteredPriv)
+        | "lock" -> (module LockCenteredPriv (NoWrapper))
+        | "lock-tid" -> (module LockCenteredPriv (DigestWrapper(ThreadNotStartedDigest)))
+        | "write" -> (module WriteCenteredPriv (NoWrapper))
+        | "write-tid" -> (module WriteCenteredPriv (DigestWrapper(ThreadNotStartedDigest)))
+        | "write+lock" -> (module WriteAndLockCenteredPriv (NoWrapper))
+        | "write+lock-tid" -> (module WriteAndLockCenteredPriv (DigestWrapper(ThreadNotStartedDigest)))
         | _ -> failwith "ana.base.privatization: illegal value"
       )
     in
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 88a2c5a5b1..40d4390eab 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -24,7 +24,7 @@ struct
 
   module Locator = WitnessUtil.Locator (Node)
 
-  let locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
+  let location_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
   let loop_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
 
   type inv = {
@@ -38,26 +38,26 @@ struct
   let pre_invs: inv EH.t NH.t = NH.create 100
 
   let init _ =
-    Locator.clear locator;
+    Locator.clear location_locator;
     Locator.clear loop_locator;
     let module FileCfg =
     struct
       let file = !Cilfacade.current_file
       module Cfg = (val !MyCFG.current_cfg)
     end  in
-    let module WitnessInvariant = WitnessUtil.Invariant (FileCfg) in
+    let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in
 
     (* DFS, copied from CfgTools.find_backwards_reachable *)
     let reachable = NH.create 100 in
     let rec iter_node node =
       if not (NH.mem reachable node) then begin
         NH.replace reachable node ();
-        (* TODO: filter synthetic?
-           See YamlWitness. *)
-        if WitnessInvariant.is_invariant_node node then
-          Locator.add locator (Node.location node) node;
-        if WitnessUtil.NH.mem WitnessInvariant.loop_heads node then
-          Locator.add loop_locator (Node.location node) node;
+        Option.iter (fun loc ->
+            Locator.add location_locator loc node
+          ) (WitnessInvariant.location_location node);
+        Option.iter (fun loc ->
+            Locator.add loop_locator loc node
+          ) (WitnessInvariant.loop_location node);
         List.iter (fun (_, prev_node) ->
             iter_node prev_node
           ) (FileCfg.Cfg.prev node)
@@ -127,7 +127,7 @@ struct
         let inv = location_invariant.location_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt location_locator loc with
         | Some nodes ->
           unassume_nodes_invariant ~loc ~nodes inv
         | None ->
@@ -190,7 +190,7 @@ struct
         let inv = precondition_loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt loop_locator loc with
         | Some nodes ->
           unassume_precondition_nodes_invariant ~loc ~nodes pre inv
         | None ->
@@ -204,7 +204,7 @@ struct
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
-          match Locator.find_opt locator loc with
+          match Locator.find_opt location_locator loc with
           | Some nodes ->
             unassume_nodes_invariant ~loc ~nodes inv
           | None ->
diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index ef0687d6eb..813ec25818 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -13,15 +13,24 @@ class exp_replace_original_name_visitor = object
   method! vvrbl (vi: varinfo) =
     ChangeTo (var_replace_original_name vi)
 end
-let exp_replace_original_name e =
+let exp_replace_original_name =
   let visitor = new exp_replace_original_name_visitor in
-  visitCilExpr visitor e
+  visitCilExpr visitor
+
+class exp_deep_unroll_types_visitor = object
+  inherit nopCilVisitor
+  method! vtype (t: typ) =
+    ChangeTo (unrollTypeDeep t)
+end
+let exp_deep_unroll_types =
+  let visitor = new exp_deep_unroll_types_visitor in
+  visitCilExpr visitor
 
 
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
   | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
-  | Some fd -> 
+  | Some fd ->
     if CilType.Fundec.equal fd scope then
       GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
     else
@@ -75,6 +84,23 @@ let exp_contains_tmp e =
   ignore (visitCilExpr visitor e);
   !acc
 
+class exp_contains_anon_type_visitor = object
+  inherit nopCilVisitor
+  method! vtype (t: typ) =
+    match t with
+    | TComp ({cname; _}, _) when BatString.starts_with_stdlib ~prefix:"__anon" cname ->
+      raise Stdlib.Exit
+    | _ ->
+      DoChildren
+end
+let exp_contains_anon_type =
+  let visitor = new exp_contains_anon_type_visitor in
+  fun e ->
+    match visitCilExpr visitor e with
+    | _ -> false
+    | exception Stdlib.Exit -> true
+
+
 (* TODO: synchronize magic constant with BaseDomain *)
 let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@"
 
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 107c1c0692..baee8a2ce6 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -39,28 +39,21 @@ struct
   include SetDomain.Reverse(SetDomain.ToppedSet (Lock) (struct let topname = "All mutexes" end))
   let name () = "lockset"
 
-  let may_be_same_offset of1 of2 =
-    (* Only reached with definite of2 and indefinite of1. *)
-    (* TODO: Currently useless, because MayPointTo query doesn't return index offset ranges, so not enough information to ever return false. *)
-    (* TODO: Use Addr.Offs.semantic_equal. *)
-    true
-
-  let add (addr,rw) set =
-    match (Addr.to_mval addr) with
-    | Some (_,x) when Offs.is_definite x -> add (addr,rw) set
-    | _ -> set
-
-  let remove (addr,rw) set =
-    let collect_diff_varinfo_with (vi,os) (addr,rw) =
-      match (Addr.to_mval addr) with
-      | Some (v,o) when CilType.Varinfo.equal vi v -> not (may_be_same_offset o os)
-      | Some (v,o) -> true
-      | None -> false
-    in
-    match (Addr.to_mval addr) with
-    | Some (_,x) when Offs.is_definite x -> remove (addr,rw) set
-    | Some x -> filter (collect_diff_varinfo_with x) set
-    | _   -> top ()
+  let add ((addr, _) as lock) set =
+    match addr with
+    | Addr.Addr mv when Addr.Mval.is_definite mv -> (* avoids NULL *)
+      add lock set
+    | _ ->
+      set
+
+  let remove ((addr, _) as lock) set =
+    match addr with
+    | Addr.Addr mv when Addr.Mval.is_definite mv -> (* avoids NULL *)
+      remove lock set
+    | _ ->
+      filter (fun (addr', _) ->
+          Addr.semantic_equal addr addr' = Some false
+        ) set
 
   let export_locks ls =
     let f (x,_) set = Mutexes.add x set in
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 35a4cce5d5..60a9a4dc84 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -132,13 +132,7 @@ let () = Printexc.register_printer (function
     | _ -> None (* for other exceptions *)
   )
 
-(** Type of CFG "edges": keyed by 'from' and 'to' nodes,
-    along with the list of connecting instructions. *)
-module CfgEdge = struct
-  type t = Node.t * MyCFG.edges * Node.t [@@deriving eq, hash]
-end
 
-module CfgEdgeH = BatHashtbl.Make (CfgEdge)
 
 let createCFG (file: file) =
   let cfgF = H.create 113 in
@@ -254,7 +248,7 @@ let createCFG (file: file) =
         let pseudo_return = lazy (
           if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s." fd.svar.vname;
           let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in
-          let newst = mkStmt (Return (None, fd_end_loc)) in
+          let newst = mkStmt (Return (None, fd_end_loc, locUnknown)) in
           newst.sid <- Cilfacade.get_pseudo_return_id fd;
           Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd;
           Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst;
@@ -340,8 +334,8 @@ let createCFG (file: file) =
             (* CIL's xform_switch_stmt (via prepareCFG) always adds both continue and break statements to all Loops. *)
             failwith "MyCFG.createCFG: unprepared Loop"
 
-          | Return (exp, loc) ->
-            addEdge (Statement stmt) (loc, Ret (exp, fd)) (Function fd)
+          | Return (exp, loc, eloc) ->
+            addEdge (Statement stmt) (Cilfacade.eloc_fallback ~eloc ~loc, Ret (exp, fd)) (Function fd)
 
           | Goto (_, loc) ->
             (* Gotos are generally unnecessary and unwanted because find_real_stmt skips over these. *)
@@ -617,7 +611,7 @@ let fprint_hash_dot cfg  =
   close_out out
 
 
-let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
+let getCFG (file: file) : cfg * cfg * _ =
   let cfgF, cfgB, skippedByEdge = createCFG file in
   let cfgF, cfgB, skippedByEdge =
     if get_bool "exp.mincfg" then
@@ -626,13 +620,11 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
       (cfgF, cfgB, skippedByEdge)
   in
   if get_bool "justcfg" then fprint_hash_dot cfgB;
-  (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge
+  (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), (fun u e v -> CfgEdgeH.find skippedByEdge (u, e, v))
 
-let compute_cfg_skips file =
+let compute_cfg file =
   let cfgF, cfgB, skippedByEdge = getCFG file in
-  (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge
-
-let compute_cfg file = fst (compute_cfg_skips file)
+  (module struct let prev = cfgB let next = cfgF let skippedByEdge = skippedByEdge end : CfgBidirSkip)
 
 
 let iter_fd_edges (module Cfg : CfgBackward) fd =
diff --git a/src/common/framework/myCFG.ml b/src/common/framework/myCFG.ml
index 76675f3c88..71290a2ec0 100644
--- a/src/common/framework/myCFG.ml
+++ b/src/common/framework/myCFG.ml
@@ -42,19 +42,36 @@ sig
   include CfgForward
 end
 
+(** Type of CFG "edges": keyed by 'from' and 'to' nodes,
+    along with the list of connecting instructions. *)
+module CfgEdge = struct
+  type t = Node.t * edges * Node.t [@@deriving eq, hash]
+end
+
+module CfgEdgeH = BatHashtbl.Make (CfgEdge)
+
+module type CfgBidirSkip =
+sig
+  include CfgBidir
+  val skippedByEdge: node -> edges -> node -> stmt list
+  (** [skippedByEdge from edges to] returns the list of {{!GoblintCil.stmt} AST statements} skipped over by [find_real_stmt] in {!CfgTools.createCfg}.
+      This consists of statements which do not correspond to CFG nodes, but some surrounding AST constructions. *)
+end
+
 
 module NodeH = BatHashtbl.Make (Node)
 
 
 let current_node = Node.current_node
-let current_cfg : (module CfgBidir) ref =
+let current_cfg : (module CfgBidirSkip) ref =
   let module Cfg =
   struct
     let next _ = raise Not_found
     let prev _ = raise Not_found
+    let skippedByEdge _ _ _ = raise Not_found
   end
   in
-  ref (module Cfg: CfgBidir)
+  ref (module Cfg: CfgBidirSkip)
 
 let unknown_exp : exp = mkString "__unknown_value__"
 let dummy_func = emptyFunction "__goblint_dummy_init" (* TODO get rid of this? *)
@@ -64,5 +81,5 @@ let dummy_node = FunctionEntry Cil.dummyFunDec
 module type FileCfg =
 sig
   val file: Cil.file
-  module Cfg: CfgBidir
+  module Cfg: CfgBidirSkip
 end
diff --git a/src/common/util/cilLocation.ml b/src/common/util/cilLocation.ml
index 23c1b8df5b..5b8771d8d4 100644
--- a/src/common/util/cilLocation.ml
+++ b/src/common/util/cilLocation.ml
@@ -34,7 +34,7 @@ let rec get_stmtLoc stmt: locs =
     {loc = locUnknown; eloc = locUnknown}
 
   | Instr (hd :: _) -> get_instrLoc hd
-  | Return (_, loc) -> {loc; eloc = locUnknown}
+  | Return (_, loc, eloc) -> {loc; eloc}
   | Goto (_, loc) -> {loc; eloc = locUnknown}
   | ComputedGoto (_, loc) -> {loc; eloc = locUnknown}
   | Break loc -> {loc; eloc = locUnknown}
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index b5b217889f..2a4e73d588 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -494,7 +494,7 @@ class countFnVisitor = object
   inherit nopCilVisitor
   method! vstmt s =
     match s.skind with
-    | Return (_, loc)
+    | Return (_, loc, _)
     | Goto (_, loc)
     | ComputedGoto (_, loc)
     | Break loc
diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml
index 35fd5fb706..5748d9166c 100644
--- a/src/common/util/cilfacade0.ml
+++ b/src/common/util/cilfacade0.ml
@@ -42,7 +42,7 @@ let rec get_stmtLoc stmt =
     get_labelsLoc stmt.labels
 
   | Instr (hd :: _) -> get_instrLoc hd
-  | Return (_, loc) -> loc
+  | Return (_, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Goto (_, loc) -> loc
   | ComputedGoto (_, loc) -> loc
   | Break loc -> loc
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index bddf89fc1c..db93e74ff4 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -752,9 +752,9 @@
             "privatization": {
               "title": "ana.base.privatization",
               "description":
-                "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock",
+                "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid",
               "type": "string",
-              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
+              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"],
               "default": "protection-read"
             },
             "priv": {
@@ -2487,6 +2487,12 @@
               "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",
               "type": "boolean",
               "default": false
+            },
+            "typedefs": {
+              "title": "witness.invariant.typedefs",
+              "description": "Emit invariants with typedef-ed types (e.g. in casts). Our validator cannot parse these.",
+              "type": "boolean",
+              "default": true
             }
           },
           "additionalProperties": false
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 3f4bd5e320..c6f17041cb 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -20,26 +20,28 @@ let spec_module: (module Spec) Lazy.t = lazy (
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
-  let module S1 = (val
-            (module MCP.MCP2 : Spec)
-            |> lift true (module WidenContextLifterSide) (* option checked in functor *)
-            (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
-            |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
-            |> lift arg_enabled (module HashconsLifter)
-            |> lift arg_enabled (module WitnessConstraints.PathSensitive3)
-            |> lift (not arg_enabled) (module PathSensitive2)
-            |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
-            |> lift true (module DeadCodeLifter)
-            |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
-            |> lift (get_int "dbg.limit.widen" > 0) (module LimitLifter)
-            |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
-            |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
-            (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
-               Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
-            |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
-            |> lift true (module LongjmpLifter)
-            |> lift termination_enabled (module RecursionTermLifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
-          ) in
+  let module S1 =
+    (val
+      (module MCP.MCP2 : Spec)
+      |> lift true (module WidenContextLifterSide) (* option checked in functor *)
+      (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
+      |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
+      |> lift arg_enabled (module HashconsLifter)
+      |> lift arg_enabled (module WitnessConstraints.PathSensitive3)
+      |> lift (not arg_enabled) (module PathSensitive2)
+      |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
+      |> lift true (module DeadCodeLifter)
+      |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
+      |> lift (get_int "dbg.limit.widen" > 0) (module LimitLifter)
+      |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
+      |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
+      (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
+         Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
+      |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
+      |> lift true (module LongjmpLifter)
+      |> lift termination_enabled (module RecursionTermLifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
+    )
+  in
   GobConfig.building_spec := false;
   ControlSpecC.control_spec_c := (module S1.C);
   (module S1)
@@ -54,7 +56,7 @@ let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _
 let current_varquery_global_state_json: (VarQuery.t option -> Yojson.Safe.t) ref = ref (fun _ -> `Null)
 
 (** Given a [Cfg], a [Spec], and an [Inc], computes the solution to [MCP.Path] *)
-module AnalyzeCFG (Cfg:CfgBidir) (Spec:Spec) (Inc:Increment) =
+module AnalyzeCFG (Cfg:CfgBidirSkip) (Spec:Spec) (Inc:Increment) =
 struct
 
   module SpecSys: SpecSys with module Spec = Spec =
@@ -230,7 +232,7 @@ struct
     res
 
   (** The main function to preform the selected analyses. *)
-  let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) skippedByEdge =
+  let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) =
     let module FileCfg: FileCfg =
     struct
       let file = file
@@ -321,12 +323,12 @@ struct
           Spec.body {ctx with local = st} func
         | MyCFG.Assign (lval,exp) ->
           if M.tracing then M.trace "global_inits" "Assign %a = %a" d_lval lval d_exp exp;
-          (match lval, exp with
+          begin match lval, exp with
             | (Var v,o), (AddrOf (Var f,NoOffset))
               when v.vstorage <> Static && isFunctionType f.vtype ->
               (try funs := Cilfacade.find_varinfo_fundec f :: !funs with Not_found -> ())
             | _ -> ()
-          );
+          end;
           let res = Spec.assign {ctx with local = st} lval exp in
           (* Needed for privatizations (e.g. None) that do not side immediately *)
           let res' = Spec.sync {ctx with local = res} `Normal in
@@ -546,9 +548,9 @@ struct
             GobSys.mkdir_or_exists save_run;
             GobConfig.write_file config;
             let module Meta = struct
-                type t = { command : string; version: string; timestamp : float; localtime : string } [@@deriving to_yojson]
-                let json = to_yojson { command = GobSys.command_line; version = Goblint_build_info.version; timestamp = Unix.time (); localtime = GobUnix.localtime () }
-              end
+              type t = { command : string; version: string; timestamp : float; localtime : string } [@@deriving to_yojson]
+              let json = to_yojson { command = GobSys.command_line; version = Goblint_build_info.version; timestamp = Unix.time (); localtime = GobUnix.localtime () }
+            end
             in
             (* Yojson.Safe.to_file meta Meta.json; *)
             Yojson.Safe.pretty_to_channel (Stdlib.open_out (Fpath.to_string meta)) Meta.json; (* the above is compact, this is pretty-printed *)
@@ -598,10 +600,10 @@ struct
       in
       let print_and_calculate_uncalled = function
         | GFun (fn, loc) when is_bad_uncalled fn.svar loc->
-            let cnt = Cilfacade.countLoc fn in
-            uncalled_dead := !uncalled_dead + cnt;
-            if get_bool "ana.dead-code.functions" then
-              M.warn ~loc:(CilLocation loc) ~category:Deadcode "Function '%a' is uncalled: %d LLoC" CilType.Fundec.pretty fn cnt  (* CilLocation is fine because always printed from scratch *)
+          let cnt = Cilfacade.countLoc fn in
+          uncalled_dead := !uncalled_dead + cnt;
+          if get_bool "ana.dead-code.functions" then
+            M.warn ~loc:(CilLocation loc) ~category:Deadcode "Function '%a' is uncalled: %d LLoC" CilType.Fundec.pretty fn cnt  (* CilLocation is fine because always printed from scratch *)
         | _ -> ()
       in
       List.iter print_and_calculate_uncalled file.globals;
@@ -616,23 +618,26 @@ struct
 
       (* run activated transformations with the analysis result *)
       let active_transformations = get_string_list "trans.activated" in
-      (if active_transformations <> [] then
-
-         (* Most transformations use the locations of statements, since they run using Cil visitors.
-            Join abstract values once per location and once per node. *)
-         let joined_by_loc, joined_by_node =
-           let open Enum in
-           let node_values = LHT.enum lh |> map (Tuple2.map1 fst) in (* drop context from key *)
-           let hashtbl_size = if fast_count node_values then count node_values else 123 in
-           let by_loc, by_node = Hashtbl.create hashtbl_size, NodeH.create hashtbl_size in
-           node_values |> iter (fun (node, v) ->
-               let loc = Node.location node in
-               (* join values once for the same location and once for the same node *)
-               let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in
-               Hashtbl.modify_opt loc join by_loc;
-               NodeH.modify_opt node join by_node;
-             );
-           by_loc, by_node
+      if active_transformations <> [] then (
+
+        (* Most transformations use the locations of statements, since they run using Cil visitors.
+           Join abstract values once per location and once per node. *)
+        let joined_by_loc, joined_by_node =
+          let open Enum in
+          let node_values = LHT.enum lh |> map (Tuple2.map1 fst) in (* drop context from key *)
+          let hashtbl_size = if fast_count node_values then count node_values else 123 in
+          let by_loc, by_node = Hashtbl.create hashtbl_size, NodeH.create hashtbl_size in
+          iter (fun (node, v) ->
+              let loc = match node with
+                | Statement s -> Cil.get_stmtLoc s.skind (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
+                | FunctionEntry _ | Function _ -> Node.location node
+              in
+              (* join values once for the same location and once for the same node *)
+              let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in
+              Hashtbl.modify_opt loc join by_loc;
+              NodeH.modify_opt node join by_node;
+            ) node_values;
+          by_loc, by_node
         in
 
         let ask ?(node = MyCFG.dummy_node) loc =
@@ -656,7 +661,10 @@ struct
         let must_be_uncalled fd = not @@ BatSet.Int.mem fd.svar.vid calledFuns in
 
         let skipped_statements from_node edge to_node =
-          CfgTools.CfgEdgeH.find_default skippedByEdge (from_node, edge, to_node) []
+          try
+            Cfg.skippedByEdge from_node edge to_node
+          with Not_found ->
+            []
         in
 
         Transform.run_transformations file active_transformations
@@ -793,22 +801,22 @@ end
    [analyze_loop] cannot reside in it anymore since each invocation of
    [get_spec] in the loop might/should return a different module, and we
    cannot swap the functor parameter from inside [AnalyzeCFG]. *)
-let rec analyze_loop (module CFG : CfgBidir) file fs change_info skippedByEdge =
+let rec analyze_loop (module CFG : CfgBidirSkip) file fs change_info =
   try
     let (module Spec) = get_spec () in
     let module A = AnalyzeCFG (CFG) (Spec) (struct let increment = change_info end) in
-    GobConfig.with_immutable_conf (fun () -> A.analyze file fs skippedByEdge)
+    GobConfig.with_immutable_conf (fun () -> A.analyze file fs)
   with Refinement.RestartAnalysis ->
     (* Tail-recursively restart the analysis again, when requested.
         All solving starts from scratch.
         Whoever raised the exception should've modified some global state
         to do a more precise analysis next time. *)
     (* TODO: do some more incremental refinement and reuse parts of solution *)
-    analyze_loop (module CFG) file fs change_info skippedByEdge
+    analyze_loop (module CFG) file fs change_info
 
 (** The main function to perform the selected analyses. *)
 let analyze change_info (file: file) fs =
   Logs.debug "Generating the control flow graph.";
-  let (module CFG), skippedByEdge = CfgTools.compute_cfg_skips file in
+  let (module CFG) = CfgTools.compute_cfg file in
   MyCFG.current_cfg := (module CFG);
-  analyze_loop (module CFG) file fs change_info skippedByEdge
+  analyze_loop (module CFG) file fs change_info
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 85f7db43b5..f3de153658 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -339,8 +339,8 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s
   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 -> 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, rename_mapping
+  | Return (Some exp1, _l1, _el1), Return (Some exp2, _l2, _el2) -> eq_exp exp1 exp2 ~rename_mapping
+  | Return (None, _l1, _el1), Return (None, _l2, _el2) -> 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
diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml
index 0cf59f0c78..88b273ab6d 100644
--- a/src/transform/expressionEvaluation.ml
+++ b/src/transform/expressionEvaluation.ml
@@ -68,7 +68,7 @@ struct
         (* Take all statements *)
         |> List.concat_map (fun (f : Cil.fundec) -> f.sallstmts |> List.map (fun s -> f, s))
         (* Add locations *)
-        |> List.map (fun (f, (s : Cil.stmt)) -> (Cilfacade.get_stmtLoc s, f, s))
+        |> List.map (fun (f, (s : Cil.stmt)) -> (Cil.get_stmtLoc s.skind, f, s)) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
         (* Filter artificial ones by impossible location *)
         |> List.filter (fun ((l : Cil.location), _, _) -> l.line >= 0)
         (* Create hash table *)
@@ -109,7 +109,7 @@ struct
                         fun (s : Cil.stmt) ->
                           succeeding_statement := Some s;
                           (* Evaluate at (directly before) a succeeding location *)
-                          Some(self#try_ask (Cilfacade.get_stmtLoc s) expression)
+                          Some(self#try_ask (Cil.get_stmtLoc s.skind) expression) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
                       end
                       statement.succs
                 with Not_found -> None
diff --git a/src/util/server.ml b/src/util/server.ml
index 6f760e6856..1b67dbf8a3 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -121,6 +121,12 @@ let serve serv =
   |> Seq.map Packet.t_of_yojson
   |> Seq.iter (handle_packet serv)
 
+(** Is node valid for lookup by location?
+    Used for abstract debugging breakpoints. *)
+let is_server_node cfgnode =
+  let loc = UpdateCil.getLoc cfgnode in
+  not loc.synthetic
+
 let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
   ResettableLazy.from_fun (fun () ->
       let module Arg = (val (Option.get_exn !ArgTools.current_arg Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or arg disabled" ())))) in
@@ -133,7 +139,7 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
       Arg.iter_nodes (fun n ->
           let cfgnode = Arg.Node.cfgnode n in
           let loc = UpdateCil.getLoc cfgnode in
-          if not loc.synthetic then
+          if is_server_node cfgnode then
             Locator.add locator loc n;
           StringH.replace ids (Arg.Node.to_string n) n;
           StringH.add cfg_nodes (Node.show_id cfgnode) n (* add for find_all *)
@@ -248,7 +254,7 @@ let node_locator: Locator.t ResettableLazy.t =
         if not (NH.mem reachable node) then begin
           NH.replace reachable node ();
           let loc = UpdateCil.getLoc node in
-          if not loc.synthetic then
+          if is_server_node node then
             Locator.add locator loc node;
           List.iter (fun (_, prev_node) ->
               iter_node prev_node
@@ -486,7 +492,7 @@ let () =
     let process { fname } serv =
       let fundec = Cilfacade.find_name_fundec fname in
       let live _ = true in (* TODO: fix this *)
-      let cfg = CfgTools.sprint_fundec_html_dot !MyCFG.current_cfg live fundec in
+      let cfg = CfgTools.sprint_fundec_html_dot (module (val !MyCFG.current_cfg: MyCFG.CfgBidirSkip): MyCFG.CfgBidir) live fundec in
       { cfg }
   end);
 
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index 6d22a51166..bb887e6cb1 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -7,10 +7,8 @@ module Specification = SvcompSpec
 
 module type Task =
 sig
-  val file: Cil.file
+  include MyCFG.FileCfg
   val specification: Specification.multi
-
-  module Cfg: MyCFG.CfgBidir
 end
 
 let task: (module Task) option ref = ref None
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
index 12bc598be5..5d22fd1e83 100644
--- a/src/witness/witnessUtil.ml
+++ b/src/witness/witnessUtil.ml
@@ -79,8 +79,65 @@ struct
       emit_after_lock
     else
       emit_other
+
+  let find_syntactic_loop_head = function
+    | Statement s ->
+      let n' = Statement (LoopUnrolling.find_original s) in
+      let prevs = Cfg.prev n' in
+      List.find_map (fun (edges, prev) ->
+          let stmts = Cfg.skippedByEdge prev edges n' in
+          List.find_map (fun s' ->
+              match s'.GoblintCil.skind with
+              | Loop (_, loc, _, _, _) -> Some loc
+              | _ -> None
+            ) stmts
+        ) prevs
+    | FunctionEntry _ | Function _ -> None
+end
+
+module YamlInvariant (FileCfg: MyCFG.FileCfg) =
+struct
+  include Invariant (FileCfg)
+
+  let is_stub_node n =
+    let fundec = Node.find_fundec n in
+    Cil.hasAttribute "goblint_stub" fundec.svar.vattr
+
+  let location_location (n : Node.t) = (* great naming... *)
+    match n with
+    | Statement s ->
+      let {loc; _}: CilLocation.locs = CilLocation.get_stmtLoc s in
+      if not loc.synthetic && is_invariant_node n && not (is_stub_node n) then (* TODO: remove is_invariant_node? i.e. exclude witness.invariant.loop-head check *)
+        Some loc
+      else
+        None
+    | FunctionEntry _ | Function _ ->
+      (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *)
+      None
+
+  let is_invariant_node n = Option.is_some (location_location n)
+
+  let loop_location n =
+    find_syntactic_loop_head n
+    |> BatOption.filter (fun _loc -> not (is_stub_node n))
+
+  let is_loop_head_node n = Option.is_some (loop_location n)
 end
 
+module YamlInvariantValidate (FileCfg: MyCFG.FileCfg) =
+struct
+  include Invariant (FileCfg)
+
+  (* TODO: filter synthetic?
+
+     Almost all loops are transformed by CIL, so the loop constructs all get synthetic locations. Filtering them from the locator could give some odd behavior: if the location is right before the loop and all the synthetic loop head stuff is filtered, then the first non-synthetic node is already inside the loop, not outside where the location actually was.
+     Similarly, if synthetic locations are then filtered, witness.invariant.loop-head becomes essentially useless.
+     I guess at some point during testing and benchmarking I achieved better results with the filtering removed. *)
+
+  let is_loop_head_node = NH.mem loop_heads
+end
+[@@deprecated]
+
 module InvariantExp =
 struct
   module ES = SetDomain.Make (CilType.Exp)
@@ -106,9 +163,20 @@ struct
     | e -> to_conjunct_set e
 
   let process_exp inv =
-    let inv' = InvariantCil.exp_replace_original_name inv in
+    let exp_deep_unroll_types =
+      if GobConfig.get_bool "witness.invariant.typedefs" then
+        Fun.id
+      else
+        InvariantCil.exp_deep_unroll_types
+    in
+    let inv' =
+      inv
+      |> exp_deep_unroll_types
+      |> InvariantCil.exp_replace_original_name
+    in
     if GobConfig.get_bool "witness.invariant.split-conjunction" then
       ES.elements (pullOutCommonConjuncts inv')
+      |> List.filter (Fun.negate InvariantCil.exp_contains_anon_type)
     else
       [inv']
 end
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index d9d39ccee1..9273616740 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -165,17 +165,28 @@ struct
   open SpecSys
 
   module NH = BatHashtbl.Make (Node)
-  module WitnessInvariant = WitnessUtil.Invariant (FileCfg)
+  module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg)
   module FMap = BatHashtbl.Make (CilType.Fundec)
   module FCMap = BatHashtbl.Make (Printable.Prod (CilType.Fundec) (Spec.C))
   type con_inv = {node: Node.t; context: Spec.C.t; invariant: Invariant.t; state: Spec.D.t}
 
   (* TODO: fix location hack *)
   module LH = BatHashtbl.Make (CilType.Location)
-  let location2nodes: Node.t list LH.t Lazy.t = lazy (
+  let location_nodes: Node.t list LH.t Lazy.t = lazy (
     let lh = LH.create 113 in
     NH.iter (fun n _ ->
-        LH.modify_def [] (Node.location n) (List.cons n) lh
+        Option.iter (fun loc ->
+            LH.modify_def [] loc (List.cons n) lh
+          ) (WitnessInvariant.location_location n)
+      ) (Lazy.force nh);
+    lh
+  )
+  let loop_nodes: Node.t list LH.t Lazy.t = lazy (
+    let lh = LH.create 113 in
+    NH.iter (fun n _ ->
+        Option.iter (fun loc ->
+            LH.modify_def [] loc (List.cons n) lh
+          ) (WitnessInvariant.loop_location n)
       ) (Lazy.force nh);
     lh
   )
@@ -193,25 +204,6 @@ struct
     in
     let task = Entry.task ~input_files ~data_model ~specification in
 
-    let is_stub_node n =
-      let fundec = Node.find_fundec n in
-      Cil.hasAttribute "goblint_stub" fundec.svar.vattr
-    in
-
-    let is_invariant_node (n : Node.t) =
-      let loc = Node.location n in
-      match n with
-      | Statement _ ->
-        not loc.synthetic && WitnessInvariant.is_invariant_node n && not (is_stub_node n)
-      | FunctionEntry _ | Function _ ->
-        (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *)
-        false
-    in
-
-    let is_loop_head_node n =
-      WitnessUtil.NH.mem WitnessInvariant.loop_heads n && not (is_stub_node n)
-    in
-
     let local_lvals n local =
       if GobConfig.get_bool "witness.invariant.accessed" then (
         match R.ask_local_node n ~local MayAccessed with
@@ -254,30 +246,26 @@ struct
     let entries =
       if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then (
         LH.fold (fun loc ns acc ->
-            if List.exists is_invariant_node ns then (
-              let inv = List.fold_left (fun acc n ->
-                  let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
-                  let lvals = local_lvals n local in
-                  Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-                ) (Invariant.bot ()) ns
-              in
-              match inv with
-              | `Lifted inv ->
-                let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
-                let location_function = fundec.svar.vname in
-                let location = Entry.location ~location:loc ~location_function in
-                let invs = WitnessUtil.InvariantExp.process_exp inv in
-                List.fold_left (fun acc inv ->
-                    let invariant = Entry.invariant (CilType.Exp.show inv) in
-                    let entry = Entry.location_invariant ~task ~location ~invariant in
-                    entry :: acc
-                  ) acc invs
-              | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
-                acc
-            )
-            else
+            let inv = List.fold_left (fun acc n ->
+                let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
+                let lvals = local_lvals n local in
+                Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+              ) (Invariant.bot ()) ns
+            in
+            match inv with
+            | `Lifted inv ->
+              let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
+              let location_function = fundec.svar.vname in
+              let location = Entry.location ~location:loc ~location_function in
+              let invs = WitnessUtil.InvariantExp.process_exp inv in
+              List.fold_left (fun acc inv ->
+                  let invariant = Entry.invariant (CilType.Exp.show inv) in
+                  let entry = Entry.location_invariant ~task ~location ~invariant in
+                  entry :: acc
+                ) acc invs
+            | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
               acc
-          ) (Lazy.force location2nodes) entries
+          ) (Lazy.force location_nodes) entries
       )
       else
         entries
@@ -287,7 +275,7 @@ struct
     let entries =
       if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then (
         LH.fold (fun loc ns acc ->
-            if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then (
+            if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? needs both loop_invariant entry enabled and witness.invariant.loop-head option enabled *)
               let inv = List.fold_left (fun acc n ->
                   let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
                   Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
@@ -309,7 +297,7 @@ struct
             )
             else
               acc
-          ) (Lazy.force location2nodes) entries
+          ) (Lazy.force loop_nodes) entries
       )
       else
         entries
@@ -340,11 +328,11 @@ struct
         entries
     in
 
-    (* Generate precondition invariants.
+    (* Generate precondition loop invariants.
        We do this in three steps:
        1. Collect contexts for each function
        2. For each function context, find "matching"/"weaker" contexts that may satisfy its invariant
-       3. Generate precondition invariants. The postcondition is a disjunction over the invariants for matching states. *)
+       3. Generate precondition loop invariants. The postcondition is a disjunction over the invariants for matching states. *)
     let entries =
       if entry_type_enabled YamlWitnessType.PreconditionLoopInvariant.entry_type then (
         (* 1. Collect contexts for each function *)
@@ -392,47 +380,47 @@ struct
 
         (* 3. Generate precondition invariants *)
         LHT.fold (fun ((n, c) as lvar) local acc ->
-            if is_invariant_node n then (
+            match WitnessInvariant.loop_location n with
+            | Some loc ->
               let fundec = Node.find_fundec n in
               let pre_lvar = (Node.FunctionEntry fundec, c) in
               let query = Queries.Invariant Invariant.default_context in
-              match R.ask_local pre_lvar query with
-              | `Lifted c_inv ->
-                let loc = Node.location n in
-                (* Find unknowns for which the preceding start state satisfies the precondtion *)
-                let xs = find_matching_states lvar in
-
-                (* Generate invariants. Give up in case one invariant could not be generated. *)
-                let invs = GobList.fold_while_some (fun acc local ->
-                    let lvals = local_lvals n local in
-                    match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with
-                    | `Lifted c -> Some ((`Lifted c)::acc)
-                    | `Bot | `Top -> None
-                  ) [] xs
-                in
-                begin match invs with
-                  | None
-                  | Some [] -> acc
-                  | Some (x::xs) ->
-                    begin match List.fold_left (fun acc inv -> Invariant.(acc || inv) [@coverage off]) x xs with (* bisect_ppx cannot handle redefined (||) *)
-                      | `Lifted inv ->
-                        let invs = WitnessUtil.InvariantExp.process_exp inv in
-                        let c_inv = InvariantCil.exp_replace_original_name c_inv in (* cannot be split *)
-                        List.fold_left (fun acc inv ->
-                            let location_function = (Node.find_fundec n).svar.vname in
-                            let location = Entry.location ~location:loc ~location_function in
-                            let precondition = Entry.invariant (CilType.Exp.show c_inv) in
-                            let invariant = Entry.invariant (CilType.Exp.show inv) in
-                            let entry = Entry.precondition_loop_invariant ~task ~location ~precondition ~invariant in
-                            entry :: acc
-                          ) acc invs
-                      | `Bot | `Top -> acc
-                    end
-                end
-              | _ -> (* Do not construct precondition invariants if we cannot express precondition *)
-                acc
-            )
-            else
+              begin match R.ask_local pre_lvar query with
+                | `Lifted c_inv ->
+                  (* Find unknowns for which the preceding start state satisfies the precondtion *)
+                  let xs = find_matching_states lvar in
+
+                  (* Generate invariants. Give up in case one invariant could not be generated. *)
+                  let invs = GobList.fold_while_some (fun acc local ->
+                      let lvals = local_lvals n local in
+                      match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with
+                      | `Lifted c -> Some ((`Lifted c)::acc)
+                      | `Bot | `Top -> None
+                    ) [] xs
+                  in
+                  begin match invs with
+                    | None
+                    | Some [] -> acc
+                    | Some (x::xs) ->
+                      begin match List.fold_left (fun acc inv -> Invariant.(acc || inv) [@coverage off]) x xs with (* bisect_ppx cannot handle redefined (||) *)
+                        | `Lifted inv ->
+                          let invs = WitnessUtil.InvariantExp.process_exp inv in
+                          let c_inv = InvariantCil.exp_replace_original_name c_inv in (* cannot be split *)
+                          List.fold_left (fun acc inv ->
+                              let location_function = (Node.find_fundec n).svar.vname in
+                              let location = Entry.location ~location:loc ~location_function in
+                              let precondition = Entry.invariant (CilType.Exp.show c_inv) in
+                              let invariant = Entry.invariant (CilType.Exp.show inv) in
+                              let entry = Entry.precondition_loop_invariant ~task ~location ~precondition ~invariant in
+                              entry :: acc
+                            ) acc invs
+                        | `Bot | `Top -> acc
+                      end
+                  end
+                | _ -> (* Do not construct precondition invariants if we cannot express precondition *)
+                  acc
+              end
+            | None ->
               acc
           ) lh entries
       )
@@ -449,30 +437,26 @@ struct
         let invariants =
           if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then (
             LH.fold (fun loc ns acc ->
-                if List.exists is_invariant_node ns then (
-                  let inv = List.fold_left (fun acc n ->
-                      let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
-                      let lvals = local_lvals n local in
-                      Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-                    ) (Invariant.bot ()) ns
-                  in
-                  match inv with
-                  | `Lifted inv ->
-                    let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
-                    let location_function = fundec.svar.vname in
-                    let location = Entry.location ~location:loc ~location_function in
-                    let invs = WitnessUtil.InvariantExp.process_exp inv in
-                    List.fold_left (fun acc inv ->
-                        let invariant = CilType.Exp.show inv in
-                        let invariant = Entry.location_invariant' ~location ~invariant in
-                        invariant :: acc
-                      ) acc invs
-                  | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
-                    acc
-                )
-                else
+                let inv = List.fold_left (fun acc n ->
+                    let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
+                    let lvals = local_lvals n local in
+                    Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+                  ) (Invariant.bot ()) ns
+                in
+                match inv with
+                | `Lifted inv ->
+                  let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
+                  let location_function = fundec.svar.vname in
+                  let location = Entry.location ~location:loc ~location_function in
+                  let invs = WitnessUtil.InvariantExp.process_exp inv in
+                  List.fold_left (fun acc inv ->
+                      let invariant = CilType.Exp.show inv in
+                      let invariant = Entry.location_invariant' ~location ~invariant in
+                      invariant :: acc
+                    ) acc invs
+                | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
                   acc
-              ) (Lazy.force location2nodes) invariants
+              ) (Lazy.force location_nodes) invariants
           )
           else
             invariants
@@ -482,7 +466,7 @@ struct
         let invariants =
           if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
             LH.fold (fun loc ns acc ->
-                if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then (
+                if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? *)
                   let inv = List.fold_left (fun acc n ->
                       let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
                       Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
@@ -504,7 +488,7 @@ struct
                 )
                 else
                   acc
-              ) (Lazy.force location2nodes) invariants
+              ) (Lazy.force loop_nodes) invariants
           )
           else
             invariants
@@ -565,7 +549,7 @@ struct
 
   module Locator = WitnessUtil.Locator (EQSys.LVar)
   module LvarS = Locator.ES
-  module WitnessInvariant = WitnessUtil.Invariant (FileCfg)
+  module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg)
   module InvariantParser = WitnessUtil.InvariantParser
   module VR = ValidationResult
 
@@ -581,19 +565,16 @@ struct
   }
 
   let validate () =
-    let locator = Locator.create () in
+    let location_locator = Locator.create () in
     let loop_locator = Locator.create () in
+    (* TODO: add all CFG nodes, not just live ones from lh, like UnassumeAnalysis *)
     LHT.iter (fun ((n, _) as lvar) _ ->
-        let loc = Node.location n in
-        (* TODO: filter synthetic?
-
-           Almost all loops are transformed by CIL, so the loop constructs all get synthetic locations. Filtering them from the locator could give some odd behavior: if the location is right before the loop and all the synthetic loop head stuff is filtered, then the first non-synthetic node is already inside the loop, not outside where the location actually was.
-           Similarly, if synthetic locations are then filtered, witness.invariant.loop-head becomes essentially useless.
-           I guess at some point during testing and benchmarking I achieved better results with the filtering removed. *)
-        if WitnessInvariant.is_invariant_node n then
-          Locator.add locator loc lvar;
-        if WitnessUtil.NH.mem WitnessInvariant.loop_heads n then
-          Locator.add loop_locator loc lvar
+        Option.iter (fun loc ->
+            Locator.add location_locator loc lvar
+          ) (WitnessInvariant.location_location n);
+        Option.iter (fun loc ->
+            Locator.add loop_locator loc lvar
+          ) (WitnessInvariant.loop_location n)
       ) lh;
 
     let inv_parser = InvariantParser.create FileCfg.file in
@@ -687,7 +668,7 @@ struct
             None
         in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt location_locator loc with
         | Some lvars ->
           validate_lvars_invariant ~entry_certificate ~loc ~lvars inv
         | None ->
@@ -727,7 +708,7 @@ struct
         in
         let msgLoc: M.Location.t = CilLocation loc in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt loop_locator loc with
         | Some lvars ->
           begin match InvariantParser.parse_cabs pre with
             | Ok pre_cabs ->
@@ -778,7 +759,7 @@ struct
           let loc = loc_of_location location_invariant.location in
           let inv = location_invariant.value in
 
-          match Locator.find_opt locator loc with
+          match Locator.find_opt location_locator loc with
           | Some lvars ->
             ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv)
           | None ->
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
index de9fa151d8..1630e05b69 100644
--- a/src/witness/yamlWitnessType.ml
+++ b/src/witness/yamlWitnessType.ml
@@ -111,6 +111,7 @@ struct
     column: int;
     function_: string;
   }
+  [@@deriving ord]
 
   let to_yaml {file_name; file_hash; line; column; function_} =
     `O [
@@ -138,6 +139,7 @@ struct
     type_: string;
     format: string;
   }
+  [@@deriving ord]
 
   let to_yaml {string; type_; format} =
     `O [
@@ -160,6 +162,7 @@ struct
     location: Location.t;
     loop_invariant: Invariant.t;
   }
+  [@@deriving ord]
 
   let entry_type = "loop_invariant"
 
@@ -182,6 +185,7 @@ struct
     location: Location.t;
     location_invariant: Invariant.t;
   }
+  [@@deriving ord]
 
   let entry_type = "location_invariant"
 
@@ -203,6 +207,7 @@ struct
   type t = {
     flow_insensitive_invariant: Invariant.t;
   }
+  [@@deriving ord]
 
   let entry_type = "flow_insensitive_invariant"
 
@@ -224,6 +229,7 @@ struct
     loop_invariant: Invariant.t;
     precondition: Invariant.t;
   }
+  [@@deriving ord]
 
   let entry_type = "precondition_loop_invariant"
 
@@ -251,6 +257,7 @@ struct
       value: string;
       format: string;
     }
+    [@@deriving ord]
 
     let invariant_type = "loop_invariant"
 
@@ -282,6 +289,7 @@ struct
     type t =
       | LocationInvariant of LocationInvariant.t
       | LoopInvariant of LoopInvariant.t
+    [@@deriving ord]
 
     let invariant_type = function
       | LocationInvariant _ -> LocationInvariant.invariant_type
@@ -309,6 +317,7 @@ struct
     type t = {
       invariant_type: InvariantType.t;
     }
+    [@@deriving ord]
 
     let to_yaml {invariant_type} =
       `O [
@@ -327,6 +336,7 @@ struct
   type t = {
     content: Invariant.t list;
   }
+  [@@deriving ord]
 
   let entry_type = "invariant_set"
 
@@ -346,6 +356,7 @@ struct
     type_: string;
     file_hash: string;
   }
+  [@@deriving ord]
 
   let to_yaml {uuid; type_; file_hash} =
     `O [
@@ -369,6 +380,7 @@ struct
     type_: string;
     format: string;
   }
+  [@@deriving ord]
 
   let to_yaml {string; type_; format} =
     `O [
@@ -391,6 +403,7 @@ struct
     target: Target.t;
     certification: Certification.t;
   }
+  [@@deriving ord]
 
   let entry_type = "loop_invariant_certificate"
 
@@ -424,6 +437,7 @@ struct
     | LoopInvariantCertificate of LoopInvariantCertificate.t
     | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
     | InvariantSet of InvariantSet.t
+  [@@deriving ord]
 
   let entry_type = function
     | LocationInvariant _ -> LocationInvariant.entry_type
diff --git a/tests/regression/00-sanity/19-if-0.t b/tests/regression/00-sanity/19-if-0.t
index f847d75446..9f856c43fc 100644
--- a/tests/regression/00-sanity/19-if-0.t
+++ b/tests/regression/00-sanity/19-if-0.t
@@ -1,33 +1,39 @@
   $ cfgDot 19-if-0.c
 
   $ graph-easy --as=boxart main.dot
-                                                   ┌────────────────────────┐
-                                                   │ main()                 │
-                                                   └────────────────────────┘
-                                                     │
-                                                     │ (body)
-                                                     ▼
-  ┌────────────────────────┐                       ┌────────────────────────┐
-  │ 19-if-0.c:15:9-15:27   │  Neg(0)               │ 19-if-0.c:9:5-16:5     │
-  │ (19-if-0.c:15:9-15:27) │ ◀──────────────────── │ (19-if-0.c:9:9-9:10)   │
-  └────────────────────────┘                       └────────────────────────┘
-    │                                                │
-    │                                                │ Pos(0)
-    │                                                ▼
-    │                                              ┌────────────────────────┐
-    │                                              │ 19-if-0.c:11:9-11:16   │
-    │                                              │ (19-if-0.c:11:9-11:16) │
-    │                                              └────────────────────────┘
-    │                                                │
-    │                                                │ stuff()
-    │                                                ▼
-    │                                              ┌────────────────────────┐
-    │                        __goblint_check(1)    │ 19-if-0.c:17:5-17:13   │
-    └────────────────────────────────────────────▶ │ (unknown)              │
-                                                   └────────────────────────┘
-                                                     │
-                                                     │ return 0
-                                                     ▼
-                                                   ┌────────────────────────┐
-                                                   │ return of main()       │
-                                                   └────────────────────────┘
+                                                           ┌────────────────────────────────┐
+                                                           │ main()                         │
+                                                           └────────────────────────────────┘
+                                                             │
+                                                             │ (body)
+                                                             ▼
+  ┌────────────────────────────────┐                       ┌────────────────────────────────┐
+  │ 19-if-0.c:15:9-15:27           │                       │ 19-if-0.c:9:5-16:5             │
+  │ (19-if-0.c:15:9-15:27)         │                       │ (19-if-0.c:9:9-9:10)           │
+  │ YAML loc: 19-if-0.c:15:9-15:27 │  Neg(0)               │ YAML loc: 19-if-0.c:9:5-16:5   │
+  │ GraphML: true; server: true    │ ◀──────────────────── │ GraphML: true; server: true    │
+  └────────────────────────────────┘                       └────────────────────────────────┘
+    │                                                        │
+    │                                                        │ Pos(0)
+    │                                                        ▼
+    │                                                      ┌────────────────────────────────┐
+    │                                                      │ 19-if-0.c:11:9-11:16           │
+    │                                                      │ (19-if-0.c:11:9-11:16)         │
+    │                                                      │ YAML loc: 19-if-0.c:11:9-11:16 │
+    │                                                      │ GraphML: true; server: true    │
+    │                                                      └────────────────────────────────┘
+    │                                                        │
+    │                                                        │ stuff()
+    │                                                        ▼
+    │                                                      ┌────────────────────────────────┐
+    │                                                      │ 19-if-0.c:17:5-17:13           │
+    │                                                      │ (19-if-0.c:17:12-17:13)        │
+    │                                __goblint_check(1)    │ YAML loc: 19-if-0.c:17:5-17:13 │
+    └────────────────────────────────────────────────────▶ │ GraphML: true; server: true    │
+                                                           └────────────────────────────────┘
+                                                             │
+                                                             │ return 0
+                                                             ▼
+                                                           ┌────────────────────────────────┐
+                                                           │ return of main()               │
+                                                           └────────────────────────────────┘
diff --git a/tests/regression/00-sanity/20-if-0-realnode.t b/tests/regression/00-sanity/20-if-0-realnode.t
index 06a0bba865..32f06ecdd4 100644
--- a/tests/regression/00-sanity/20-if-0-realnode.t
+++ b/tests/regression/00-sanity/20-if-0-realnode.t
@@ -1,35 +1,41 @@
   $ cfgDot 20-if-0-realnode.c
 
   $ graph-easy --as=boxart main.dot
-  ┌─────────────────────────────────┐
-  │ main()                          │
-  └─────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ main()                                  │
+  └─────────────────────────────────────────┘
     │
     │ (body)
     ▼
-  ┌─────────────────────────────────┐
-  │ 20-if-0-realnode.c:8:5-14:5     │   Neg(0)
-  │ (20-if-0-realnode.c:8:9-8:10)   │ ─────────┐
-  │ [20-if-0-realnode.c:7:5-8:5     │          │
-  │ (unknown)]                      │ ◀────────┘
-  └─────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 20-if-0-realnode.c:8:5-14:5             │
+  │ (20-if-0-realnode.c:8:9-8:10)           │
+  │ [20-if-0-realnode.c:7:5-8:5             │   Neg(0)
+  │ (unknown)]                              │ ─────────┐
+  │ YAML loc: 20-if-0-realnode.c:8:5-14:5   │          │
+  │ GraphML: true; server: true             │ ◀────────┘
+  └─────────────────────────────────────────┘
     │
     │ Pos(0)
     ▼
-  ┌─────────────────────────────────┐
-  │ 20-if-0-realnode.c:10:9-10:16   │
-  │ (20-if-0-realnode.c:10:9-10:16) │
-  └─────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 20-if-0-realnode.c:10:9-10:16           │
+  │ (20-if-0-realnode.c:10:9-10:16)         │
+  │ YAML loc: 20-if-0-realnode.c:10:9-10:16 │
+  │ GraphML: true; server: true             │
+  └─────────────────────────────────────────┘
     │
     │ stuff()
     ▼
-  ┌─────────────────────────────────┐
-  │ 20-if-0-realnode.c:15:5-15:13   │
-  │ (unknown)                       │
-  └─────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 20-if-0-realnode.c:15:5-15:13           │
+  │ (20-if-0-realnode.c:15:12-15:13)        │
+  │ YAML loc: 20-if-0-realnode.c:15:5-15:13 │
+  │ GraphML: true; server: true             │
+  └─────────────────────────────────────────┘
     │
     │ return 0
     ▼
-  ┌─────────────────────────────────┐
-  │ return of main()                │
-  └─────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ return of main()                        │
+  └─────────────────────────────────────────┘
diff --git a/tests/regression/00-sanity/21-empty-loops.t b/tests/regression/00-sanity/21-empty-loops.t
index 202a4d1071..932a21f049 100644
--- a/tests/regression/00-sanity/21-empty-loops.t
+++ b/tests/regression/00-sanity/21-empty-loops.t
@@ -1,31 +1,35 @@
   $ cfgDot 21-empty-loops.c
 
   $ graph-easy --as=boxart f_empty_goto_loop.dot
-  ┌───────────────────────────────┐
-  │ f_empty_goto_loop()           │
-  └───────────────────────────────┘
+  ┌───────────────────────────────────────┐
+  │ f_empty_goto_loop()                   │
+  └───────────────────────────────────────┘
     │
     │ (body)
     ▼
-  ┌───────────────────────────────┐
-  │ 21-empty-loops.c:57:3-57:31   │   skip
-  │ (unknown)                     │ ───────┐
-  │ [21-empty-loops.c:56:1-57:3   │        │
-  │ (unknown)]                    │ ◀──────┘
-  └───────────────────────────────┘
+  ┌───────────────────────────────────────┐
+  │ 21-empty-loops.c:57:3-57:31           │
+  │ (unknown)                             │
+  │ [21-empty-loops.c:56:1-57:3           │   skip
+  │ (unknown)]                            │ ───────┐
+  │ YAML loc: 21-empty-loops.c:57:3-57:31 │        │
+  │ GraphML: true; server: true           │ ◀──────┘
+  └───────────────────────────────────────┘
     │
     │ Neg(1)
     ▼
-  ┌───────────────────────────────┐
-  │ 21-empty-loops.c:58:1-58:1    │
-  │ (unknown)                     │
-  └───────────────────────────────┘
+  ┌───────────────────────────────────────┐
+  │ 21-empty-loops.c:58:1-58:1            │
+  │ (unknown)                             │
+  │ YAML loc: 21-empty-loops.c:58:1-58:1  │
+  │ GraphML: true; server: true           │
+  └───────────────────────────────────────┘
     │
     │ return
     ▼
-  ┌───────────────────────────────┐
-  │ return of f_empty_goto_loop() │
-  └───────────────────────────────┘
+  ┌───────────────────────────────────────┐
+  │ return of f_empty_goto_loop()         │
+  └───────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_empty_while_loop.dot
   ┌────────────────────────────────────────────┐
@@ -34,10 +38,12 @@
     │
     │ (body)
     ▼
-  ┌────────────────────────────────────────────┐   Pos(1)
-  │ 21-empty-loops.c:62:3-62:14 (synthetic)    │ ─────────┐
-  │ (21-empty-loops.c:62:10-62:11 (synthetic)) │          │
-  │                                            │ ◀────────┘
+  ┌────────────────────────────────────────────┐
+  │ 21-empty-loops.c:62:3-62:14 (synthetic)    │
+  │ (21-empty-loops.c:62:10-62:11 (synthetic)) │   Pos(1)
+  │ YAML loop: 21-empty-loops.c:62:3-62:14     │ ─────────┐
+  │ GraphML: true; server: false               │          │
+  │ loop: 21-empty-loops.c:62:3-62:14          │ ◀────────┘
   └────────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -45,6 +51,8 @@
   ┌────────────────────────────────────────────┐
   │ 21-empty-loops.c:63:1-63:1                 │
   │ (unknown)                                  │
+  │ YAML loc: 21-empty-loops.c:63:1-63:1       │
+  │ GraphML: true; server: true                │
   └────────────────────────────────────────────┘
     │
     │ return
@@ -54,35 +62,41 @@
   └────────────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_empty_goto_loop_suffix.dot
-             ┌──────────────────────────────────────┐
-             │ 21-empty-loops.c:75:3-75:11          │
-             │ (21-empty-loops.c:75:3-75:11)        │
-             └──────────────────────────────────────┘
+             ┌───────────────────────────────────────┐
+             │ 21-empty-loops.c:75:3-75:11           │
+             │ (21-empty-loops.c:75:3-75:11)         │
+             │ YAML loc: 21-empty-loops.c:75:3-75:11 │
+             │ GraphML: true; server: true           │
+             └───────────────────────────────────────┘
                │
                │ suffix()
                ▼
-             ┌──────────────────────────────────────┐
-             │ 21-empty-loops.c:76:1-76:1           │
-             │ (unknown)                            │ ◀┐
-             └──────────────────────────────────────┘  │
-               │                                       │
-               │ return                                │
-               ▼                                       │
-             ┌──────────────────────────────────────┐  │
-             │ return of f_empty_goto_loop_suffix() │  │
-             └──────────────────────────────────────┘  │
-             ┌──────────────────────────────────────┐  │ Neg(1)
-             │ f_empty_goto_loop_suffix()           │  │
-             └──────────────────────────────────────┘  │
-               │                                       │
-               │ (body)                                │
-               ▼                                       │
-             ┌──────────────────────────────────────┐  │
-      skip   │ 21-empty-loops.c:73:3-73:38          │  │
-    ┌─────── │ (unknown)                            │  │
-    │        │ [21-empty-loops.c:72:1-73:3          │  │
-    └──────▶ │ (unknown)]                           │ ─┘
-             └──────────────────────────────────────┘
+             ┌───────────────────────────────────────┐
+             │ 21-empty-loops.c:76:1-76:1            │
+             │ (unknown)                             │
+             │ YAML loc: 21-empty-loops.c:76:1-76:1  │
+             │ GraphML: true; server: true           │ ◀┐
+             └───────────────────────────────────────┘  │
+               │                                        │
+               │ return                                 │
+               ▼                                        │
+             ┌───────────────────────────────────────┐  │
+             │ return of f_empty_goto_loop_suffix()  │  │
+             └───────────────────────────────────────┘  │
+             ┌───────────────────────────────────────┐  │ Neg(1)
+             │ f_empty_goto_loop_suffix()            │  │
+             └───────────────────────────────────────┘  │
+               │                                        │
+               │ (body)                                 │
+               ▼                                        │
+             ┌───────────────────────────────────────┐  │
+             │ 21-empty-loops.c:73:3-73:38           │  │
+             │ (unknown)                             │  │
+      skip   │ [21-empty-loops.c:72:1-73:3           │  │
+    ┌─────── │ (unknown)]                            │  │
+    │        │ YAML loc: 21-empty-loops.c:73:3-73:38 │  │
+    └──────▶ │ GraphML: true; server: true           │ ─┘
+             └───────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_empty_while_loop_suffix.dot
   ┌────────────────────────────────────────────┐
@@ -91,10 +105,12 @@
     │
     │ (body)
     ▼
-  ┌────────────────────────────────────────────┐   Pos(1)
-  │ 21-empty-loops.c:80:3-80:14 (synthetic)    │ ─────────┐
-  │ (21-empty-loops.c:80:10-80:11 (synthetic)) │          │
-  │                                            │ ◀────────┘
+  ┌────────────────────────────────────────────┐
+  │ 21-empty-loops.c:80:3-80:14 (synthetic)    │
+  │ (21-empty-loops.c:80:10-80:11 (synthetic)) │   Pos(1)
+  │ YAML loop: 21-empty-loops.c:80:3-80:14     │ ─────────┐
+  │ GraphML: true; server: false               │          │
+  │ loop: 21-empty-loops.c:80:3-80:14          │ ◀────────┘
   └────────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -102,6 +118,8 @@
   ┌────────────────────────────────────────────┐
   │ 21-empty-loops.c:82:3-82:11                │
   │ (21-empty-loops.c:82:3-82:11)              │
+  │ YAML loc: 21-empty-loops.c:82:3-82:11      │
+  │ GraphML: true; server: true                │
   └────────────────────────────────────────────┘
     │
     │ suffix()
@@ -109,6 +127,8 @@
   ┌────────────────────────────────────────────┐
   │ 21-empty-loops.c:83:1-83:1                 │
   │ (unknown)                                  │
+  │ YAML loc: 21-empty-loops.c:83:1-83:1       │
+  │ GraphML: true; server: true                │
   └────────────────────────────────────────────┘
     │
     │ return
@@ -118,93 +138,107 @@
   └────────────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_nonempty_goto_loop.dot
-  ┌──────────────────────────────────┐
-  │ f_nonempty_goto_loop()           │
-  └──────────────────────────────────┘
+  ┌──────────────────────────────────────┐
+  │ f_nonempty_goto_loop()               │
+  └──────────────────────────────────────┘
     │
     │ (body)
     ▼
-  ┌──────────────────────────────────┐   body()
-  │ 21-empty-loops.c:93:3-93:9       │ ─────────┐
-  │ (21-empty-loops.c:93:3-93:9)     │          │
-  │                                  │ ◀────────┘
-  └──────────────────────────────────┘
+  ┌──────────────────────────────────────┐
+  │ 21-empty-loops.c:93:3-93:9           │   body()
+  │ (21-empty-loops.c:93:3-93:9)         │ ─────────┐
+  │ YAML loc: 21-empty-loops.c:93:3-93:9 │          │
+  │ GraphML: true; server: true          │ ◀────────┘
+  └──────────────────────────────────────┘
     │
     │ Neg(1)
     ▼
-  ┌──────────────────────────────────┐
-  │ 21-empty-loops.c:95:1-95:1       │
-  │ (unknown)                        │
-  └──────────────────────────────────┘
+  ┌──────────────────────────────────────┐
+  │ 21-empty-loops.c:95:1-95:1           │
+  │ (unknown)                            │
+  │ YAML loc: 21-empty-loops.c:95:1-95:1 │
+  │ GraphML: true; server: true          │
+  └──────────────────────────────────────┘
     │
     │ return
     ▼
-  ┌──────────────────────────────────┐
-  │ return of f_nonempty_goto_loop() │
-  └──────────────────────────────────┘
+  ┌──────────────────────────────────────┐
+  │ return of f_nonempty_goto_loop()     │
+  └──────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_nonempty_while_loop.dot
   
-    ┌───────────────────────────────────────────────────────────────────────────────────────────┐
-    │                                                                                           │
-    │                                           ┌────────────────────────────────────────────┐  │
-    │                                           │ f_nonempty_while_loop()                    │  │
-    │                                           └────────────────────────────────────────────┘  │
-    │                                             │                                             │ body()
-    │                                             │ (body)                                      │
-    │                                             ▼                                             │
-  ┌─────────────────────────────────┐           ┌────────────────────────────────────────────┐  │
-  │ 21-empty-loops.c:101:5-101:11   │  Pos(1)   │ 21-empty-loops.c:99:3-102:3 (synthetic)    │  │
-  │ (21-empty-loops.c:101:5-101:11) │ ◀──────── │ (21-empty-loops.c:99:10-99:11 (synthetic)) │ ◀┘
-  └─────────────────────────────────┘           └────────────────────────────────────────────┘
-                                                  │
-                                                  │ Neg(1)
-                                                  ▼
-                                                ┌────────────────────────────────────────────┐
-                                                │ 21-empty-loops.c:103:1-103:1               │
-                                                │ (unknown)                                  │
-                                                └────────────────────────────────────────────┘
-                                                  │
-                                                  │ return
-                                                  ▼
-                                                ┌────────────────────────────────────────────┐
-                                                │ return of f_nonempty_while_loop()          │
-                                                └────────────────────────────────────────────┘
+    ┌───────────────────────────────────────────────────────────────────────────────────────────────────┐
+    │                                                                                                   │
+    │                                                   ┌────────────────────────────────────────────┐  │
+    │                                                   │ f_nonempty_while_loop()                    │  │
+    │                                                   └────────────────────────────────────────────┘  │
+    │                                                     │                                             │ body()
+    │                                                     │ (body)                                      │
+    │                                                     ▼                                             │
+  ┌─────────────────────────────────────────┐           ┌────────────────────────────────────────────┐  │
+  │ 21-empty-loops.c:101:5-101:11           │           │ 21-empty-loops.c:99:3-102:3 (synthetic)    │  │
+  │ (21-empty-loops.c:101:5-101:11)         │           │ (21-empty-loops.c:99:10-99:11 (synthetic)) │  │
+  │ YAML loc: 21-empty-loops.c:101:5-101:11 │           │ YAML loop: 21-empty-loops.c:99:3-102:3     │  │
+  │ GraphML: true; server: true             │  Pos(1)   │ GraphML: true; server: false               │  │
+  │                                         │ ◀──────── │ loop: 21-empty-loops.c:99:3-102:3          │ ◀┘
+  └─────────────────────────────────────────┘           └────────────────────────────────────────────┘
+                                                          │
+                                                          │ Neg(1)
+                                                          ▼
+                                                        ┌────────────────────────────────────────────┐
+                                                        │ 21-empty-loops.c:103:1-103:1               │
+                                                        │ (unknown)                                  │
+                                                        │ YAML loc: 21-empty-loops.c:103:1-103:1     │
+                                                        │ GraphML: true; server: true                │
+                                                        └────────────────────────────────────────────┘
+                                                          │
+                                                          │ return
+                                                          ▼
+                                                        ┌────────────────────────────────────────────┐
+                                                        │ return of f_nonempty_while_loop()          │
+                                                        └────────────────────────────────────────────┘
 
 
   $ graph-easy --as=boxart f_empty_goto_loop_prefix.dot
-  ┌──────────────────────────────────────┐
-  │ f_empty_goto_loop_prefix()           │
-  └──────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ f_empty_goto_loop_prefix()              │
+  └─────────────────────────────────────────┘
     │
     │ (body)
     ▼
-  ┌──────────────────────────────────────┐
-  │ 21-empty-loops.c:112:3-112:11        │
-  │ (21-empty-loops.c:112:3-112:11)      │
-  └──────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 21-empty-loops.c:112:3-112:11           │
+  │ (21-empty-loops.c:112:3-112:11)         │
+  │ YAML loc: 21-empty-loops.c:112:3-112:11 │
+  │ GraphML: true; server: true             │
+  └─────────────────────────────────────────┘
     │
     │ prefix()
     ▼
-  ┌──────────────────────────────────────┐
-  │ 21-empty-loops.c:115:3-115:38        │   skip
-  │ (unknown)                            │ ───────┐
-  │ [21-empty-loops.c:114:1-115:3        │        │
-  │ (unknown)]                           │ ◀──────┘
-  └──────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 21-empty-loops.c:115:3-115:38           │
+  │ (unknown)                               │
+  │ [21-empty-loops.c:114:1-115:3           │   skip
+  │ (unknown)]                              │ ───────┐
+  │ YAML loc: 21-empty-loops.c:115:3-115:38 │        │
+  │ GraphML: true; server: true             │ ◀──────┘
+  └─────────────────────────────────────────┘
     │
     │ Neg(1)
     ▼
-  ┌──────────────────────────────────────┐
-  │ 21-empty-loops.c:116:1-116:1         │
-  │ (unknown)                            │
-  └──────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 21-empty-loops.c:116:1-116:1            │
+  │ (unknown)                               │
+  │ YAML loc: 21-empty-loops.c:116:1-116:1  │
+  │ GraphML: true; server: true             │
+  └─────────────────────────────────────────┘
     │
     │ return
     ▼
-  ┌──────────────────────────────────────┐
-  │ return of f_empty_goto_loop_prefix() │
-  └──────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ return of f_empty_goto_loop_prefix()    │
+  └─────────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_empty_while_loop_prefix.dot
   ┌──────────────────────────────────────────────┐
@@ -216,14 +250,18 @@
   ┌──────────────────────────────────────────────┐
   │ 21-empty-loops.c:120:3-120:11                │
   │ (21-empty-loops.c:120:3-120:11)              │
+  │ YAML loc: 21-empty-loops.c:120:3-120:11      │
+  │ GraphML: true; server: true                  │
   └──────────────────────────────────────────────┘
     │
     │ prefix()
     ▼
-  ┌──────────────────────────────────────────────┐   Pos(1)
-  │ 21-empty-loops.c:122:3-122:14 (synthetic)    │ ─────────┐
-  │ (21-empty-loops.c:122:10-122:11 (synthetic)) │          │
-  │                                              │ ◀────────┘
+  ┌──────────────────────────────────────────────┐
+  │ 21-empty-loops.c:122:3-122:14 (synthetic)    │
+  │ (21-empty-loops.c:122:10-122:11 (synthetic)) │   Pos(1)
+  │ YAML loop: 21-empty-loops.c:122:3-122:14     │ ─────────┐
+  │ GraphML: true; server: false                 │          │
+  │ loop: 21-empty-loops.c:122:3-122:14          │ ◀────────┘
   └──────────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -231,6 +269,8 @@
   ┌──────────────────────────────────────────────┐
   │ 21-empty-loops.c:123:1-123:1                 │
   │ (unknown)                                    │
+  │ YAML loc: 21-empty-loops.c:123:1-123:1       │
+  │ GraphML: true; server: true                  │
   └──────────────────────────────────────────────┘
     │
     │ return
@@ -247,10 +287,11 @@
     │ (body)
     ▼
   ┌─────────────────────────────────────────┐
-  │ unknown                                 │   skip
-  │ (unknown)                               │ ───────┐
-  │ [21-empty-loops.c:127:1-128:3           │        │
-  │ (unknown)]                              │ ◀──────┘
+  │ unknown                                 │
+  │ (unknown)                               │   skip
+  │ [21-empty-loops.c:127:1-128:3           │ ───────┐
+  │ (unknown)]                              │        │
+  │ GraphML: true; server: true             │ ◀──────┘
   └─────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -258,6 +299,8 @@
   ┌─────────────────────────────────────────┐
   │ 21-empty-loops.c:131:1-131:1            │
   │ (unknown)                               │
+  │ YAML loc: 21-empty-loops.c:131:1-131:1  │
+  │ GraphML: true; server: true             │
   └─────────────────────────────────────────┘
     │
     │ return
@@ -273,10 +316,12 @@
     │
     │ (body)
     ▼
-  ┌──────────────────────────────────────────────┐   Pos(1)
-  │ 21-empty-loops.c:135:3-137:3 (synthetic)     │ ─────────┐
-  │ (21-empty-loops.c:135:10-135:11 (synthetic)) │          │
-  │                                              │ ◀────────┘
+  ┌──────────────────────────────────────────────┐
+  │ 21-empty-loops.c:135:3-137:3 (synthetic)     │
+  │ (21-empty-loops.c:135:10-135:11 (synthetic)) │   Pos(1)
+  │ YAML loop: 21-empty-loops.c:135:3-137:3      │ ─────────┐
+  │ GraphML: true; server: false                 │          │
+  │ loop: 21-empty-loops.c:135:3-137:3           │ ◀────────┘
   └──────────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -284,6 +329,8 @@
   ┌──────────────────────────────────────────────┐
   │ 21-empty-loops.c:138:1-138:1                 │
   │ (unknown)                                    │
+  │ YAML loc: 21-empty-loops.c:138:1-138:1       │
+  │ GraphML: true; server: true                  │
   └──────────────────────────────────────────────┘
     │
     │ return
@@ -293,31 +340,35 @@
   └──────────────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_empty_goto_loop_multiple.dot
-  ┌────────────────────────────────────────┐
-  │ f_empty_goto_loop_multiple()           │
-  └────────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ f_empty_goto_loop_multiple()            │
+  └─────────────────────────────────────────┘
     │
     │ (body)
     ▼
-  ┌────────────────────────────────────────┐
-  │ 21-empty-loops.c:143:3-143:42          │   skip
-  │ (unknown)                              │ ───────┐
-  │ [21-empty-loops.c:142:1-143:3          │        │
-  │ (unknown)]                             │ ◀──────┘
-  └────────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 21-empty-loops.c:143:3-143:42           │
+  │ (unknown)                               │
+  │ [21-empty-loops.c:142:1-143:3           │   skip
+  │ (unknown)]                              │ ───────┐
+  │ YAML loc: 21-empty-loops.c:143:3-143:42 │        │
+  │ GraphML: true; server: true             │ ◀──────┘
+  └─────────────────────────────────────────┘
     │
     │ Neg(1)
     ▼
-  ┌────────────────────────────────────────┐
-  │ 21-empty-loops.c:146:1-146:1           │
-  │ (unknown)                              │
-  └────────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ 21-empty-loops.c:146:1-146:1            │
+  │ (unknown)                               │
+  │ YAML loc: 21-empty-loops.c:146:1-146:1  │
+  │ GraphML: true; server: true             │
+  └─────────────────────────────────────────┘
     │
     │ return
     ▼
-  ┌────────────────────────────────────────┐
-  │ return of f_empty_goto_loop_multiple() │
-  └────────────────────────────────────────┘
+  ┌─────────────────────────────────────────┐
+  │ return of f_empty_goto_loop_multiple()  │
+  └─────────────────────────────────────────┘
 
   $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_first.dot
   ┌────────────────────────────────────────────────────────┐
@@ -327,10 +378,11 @@
     │ (body)
     ▼
   ┌────────────────────────────────────────────────────────┐
-  │ unknown                                                │   skip
-  │ (unknown)                                              │ ───────┐
-  │ [21-empty-loops.c:150:1-151:3                          │        │
-  │ (unknown)]                                             │ ◀──────┘
+  │ unknown                                                │
+  │ (unknown)                                              │   skip
+  │ [21-empty-loops.c:150:1-151:3                          │ ───────┐
+  │ (unknown)]                                             │        │
+  │ GraphML: true; server: true                            │ ◀──────┘
   └────────────────────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -338,6 +390,8 @@
   ┌────────────────────────────────────────────────────────┐
   │ 21-empty-loops.c:155:1-155:1                           │
   │ (unknown)                                              │
+  │ YAML loc: 21-empty-loops.c:155:1-155:1                 │
+  │ GraphML: true; server: true                            │
   └────────────────────────────────────────────────────────┘
     │
     │ return
@@ -354,10 +408,12 @@
     │ (body)
     ▼
   ┌─────────────────────────────────────────────────────────┐
-  │ 21-empty-loops.c:160:3-160:59                           │   skip
-  │ (unknown)                                               │ ───────┐
-  │ [21-empty-loops.c:159:1-160:3                           │        │
-  │ (unknown)]                                              │ ◀──────┘
+  │ 21-empty-loops.c:160:3-160:59                           │
+  │ (unknown)                                               │
+  │ [21-empty-loops.c:159:1-160:3                           │   skip
+  │ (unknown)]                                              │ ───────┐
+  │ YAML loc: 21-empty-loops.c:160:3-160:59                 │        │
+  │ GraphML: true; server: true                             │ ◀──────┘
   └─────────────────────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -365,6 +421,8 @@
   ┌─────────────────────────────────────────────────────────┐
   │ 21-empty-loops.c:164:1-164:1                            │
   │ (unknown)                                               │
+  │ YAML loc: 21-empty-loops.c:164:1-164:1                  │
+  │ GraphML: true; server: true                             │
   └─────────────────────────────────────────────────────────┘
     │
     │ return
@@ -381,10 +439,11 @@
     │ (body)
     ▼
   ┌───────────────────────────────────────────────────────┐
-  │ unknown                                               │   skip
-  │ (unknown)                                             │ ───────┐
-  │ [21-empty-loops.c:168:1-169:3                         │        │
-  │ (unknown)]                                            │ ◀──────┘
+  │ unknown                                               │
+  │ (unknown)                                             │   skip
+  │ [21-empty-loops.c:168:1-169:3                         │ ───────┐
+  │ (unknown)]                                            │        │
+  │ GraphML: true; server: true                           │ ◀──────┘
   └───────────────────────────────────────────────────────┘
     │
     │ Neg(1)
@@ -392,6 +451,8 @@
   ┌───────────────────────────────────────────────────────┐
   │ 21-empty-loops.c:174:1-174:1                          │
   │ (unknown)                                             │
+  │ YAML loc: 21-empty-loops.c:174:1-174:1                │
+  │ GraphML: true; server: true                           │
   └───────────────────────────────────────────────────────┘
     │
     │ return
diff --git a/tests/regression/05-lval_ls/19-idxunknown_unlock_precise.c b/tests/regression/05-lval_ls/19-idxunknown_unlock_precise.c
index 4b62b52cff..e5d0b1a022 100644
--- a/tests/regression/05-lval_ls/19-idxunknown_unlock_precise.c
+++ b/tests/regression/05-lval_ls/19-idxunknown_unlock_precise.c
@@ -1,5 +1,4 @@
-// PARAM: --enable ana.int.interval
-// TODO because queries don't pass lvalue index intervals
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 extern void abort(void);
 void assume_abort_if_not(int cond) {
@@ -15,7 +14,7 @@ pthread_mutex_t m[10];
 
 void *t_fun(void *arg) {
   pthread_mutex_lock(&m[4]);
-  data++; // TODO NORACE
+  data++; // NORACE
   pthread_mutex_unlock(&m[4]);
   return NULL;
 }
@@ -33,7 +32,7 @@ int main() {
   pthread_create(&id, NULL, t_fun, NULL);
   pthread_mutex_lock(&m[4]);
   pthread_mutex_unlock(&m[i]); // no UB because ERRORCHECK
-  data++; // TODO NORACE
+  data++; // NORACE
   pthread_mutex_unlock(&m[4]);
   return 0;
 }
diff --git a/tests/regression/13-privatized/18-first-reads.c b/tests/regression/13-privatized/18-first-reads.c
index 270307968a..e1b49f6a7f 100644
--- a/tests/regression/13-privatized/18-first-reads.c
+++ b/tests/regression/13-privatized/18-first-reads.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.int.interval true
+// PARAM: --set ana.int.interval true --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>
diff --git a/tests/regression/13-privatized/53-pfscan_widen_dependent_minimal.c b/tests/regression/13-privatized/53-pfscan_widen_dependent_minimal.c
index 5ad02c33a1..b34956dc7b 100644
--- a/tests/regression/13-privatized/53-pfscan_widen_dependent_minimal.c
+++ b/tests/regression/13-privatized/53-pfscan_widen_dependent_minimal.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval --enable exp.priv-distr-init --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/13-privatized/55-widen-dependent-local.c b/tests/regression/13-privatized/55-widen-dependent-local.c
index 24eb28332e..7d16c39372 100644
--- a/tests/regression/13-privatized/55-widen-dependent-local.c
+++ b/tests/regression/13-privatized/55-widen-dependent-local.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval --enable exp.priv-distr-init  --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/13-privatized/77-lock-tid.c b/tests/regression/13-privatized/77-lock-tid.c
new file mode 100644
index 0000000000..9da26595d6
--- /dev/null
+++ b/tests/regression/13-privatized/77-lock-tid.c
@@ -0,0 +1,48 @@
+// PARAM: --set ana.base.privatization lock-tid --enable ana.int.interval --set ana.path_sens[+] mutex
+// Based on the example {e:lock-centered-beats-write-centered} from the draft of Michael Schwarz's PhD thesis.
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t a;
+pthread_mutex_t d;
+
+
+void* other()
+{
+  pthread_mutex_lock(&d);
+  pthread_mutex_lock(&a);
+  g = 42;
+  pthread_mutex_unlock(&a);
+  g = 17;
+  pthread_mutex_unlock(&d);
+  return 0;
+}
+
+void* there_i_ruined_it()
+{
+  pthread_mutex_lock(&a);
+  g = 45;
+  pthread_mutex_unlock(&a);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  pthread_t tid1;
+  pthread_t tid2;
+  pthread_create(&tid1, 0, other, 0);
+
+  pthread_mutex_lock(&d);
+  pthread_mutex_lock(&a);
+  pthread_mutex_unlock(&d);
+
+  x = g;
+  // Succeeds with lock, fails with write
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(x <= 17);
+
+  pthread_create(&tid2, 0, there_i_ruined_it, 0);
+  return 0;
+}
diff --git a/tests/regression/13-privatized/78-write-tid.c b/tests/regression/13-privatized/78-write-tid.c
new file mode 100644
index 0000000000..ec93e3c969
--- /dev/null
+++ b/tests/regression/13-privatized/78-write-tid.c
@@ -0,0 +1,67 @@
+// PARAM: --set ana.base.privatization write-tid --enable ana.int.interval --set ana.path_sens[+] mutex
+// Based on the example {e:write-centered} from the draft of Michael Schwarz's PhD thesis.
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t a;
+pthread_mutex_t b;
+pthread_mutex_t c;
+
+
+void* t1()
+{
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+  g = 42;
+  pthread_mutex_unlock(&a);
+  g = 17;
+  pthread_mutex_unlock(&b);
+}
+
+void* t2()
+{
+  pthread_mutex_lock(&c);
+  g = 59;
+  pthread_mutex_unlock(&c);
+  return 0;
+}
+
+void* there_i_ruined_it()
+{
+  pthread_mutex_lock(&a);
+  g = 45;
+  pthread_mutex_unlock(&a);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  pthread_t tid1;
+  pthread_t tid2;
+  pthread_t tid3;
+
+  pthread_create(&tid1, 0, t1, 0);
+  pthread_create(&tid2, 0, t2, 0);
+
+  pthread_mutex_lock(&c);
+  g=31;
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+
+  x = g;
+
+  // Succeed with write & lock
+  __goblint_check(x >= 17);
+
+  // Succeeds with write-tid & lock-tid
+  __goblint_check(x <= 42);
+
+  // Succeeds with write, fails with lock
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(x <= 31);
+
+  pthread_create(&tid3, 0, there_i_ruined_it, 0);
+  return 0;
+}
diff --git a/tests/regression/13-privatized/79-write-lock-tid.c b/tests/regression/13-privatized/79-write-lock-tid.c
new file mode 100644
index 0000000000..ab9ef2a33c
--- /dev/null
+++ b/tests/regression/13-privatized/79-write-lock-tid.c
@@ -0,0 +1,91 @@
+// PARAM: --set ana.base.privatization write+lock-tid --enable ana.int.interval --set ana.path_sens[+] mutex
+// Based on combining the examples {e:lock-centered-beats-write-centered} and {e:write-centered} from the draft of Michael Schwarz's PhD thesis.
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t a;
+pthread_mutex_t b;
+pthread_mutex_t c;
+
+int xg;
+pthread_mutex_t xa;
+pthread_mutex_t xd;
+
+
+void* t1()
+{
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+  g = 42;
+  pthread_mutex_unlock(&a);
+  g = 17;
+  pthread_mutex_unlock(&b);
+
+  pthread_mutex_lock(&xd);
+  pthread_mutex_lock(&xa);
+  xg = 42;
+  pthread_mutex_unlock(&xa);
+  xg = 17;
+  pthread_mutex_unlock(&xd);
+}
+
+void* t2()
+{
+  pthread_mutex_lock(&c);
+  g = 59;
+  pthread_mutex_unlock(&c);
+  return 0;
+}
+
+void* there_i_ruined_it()
+{
+  pthread_mutex_lock(&a);
+  g = 45;
+  pthread_mutex_unlock(&a);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  int xx;
+  pthread_t tid1;
+  pthread_t tid2;
+  pthread_t tid3;
+
+  pthread_create(&tid1, 0, t1, 0);
+  pthread_create(&tid2, 0, t2, 0);
+
+  pthread_mutex_lock(&c);
+  g=31;
+  pthread_mutex_lock(&a);
+  pthread_mutex_lock(&b);
+
+  x = g;
+
+  // Succeed with write & lock
+  __goblint_check(x >= 17);
+
+  // Succeeds with write-tid & lock-tid
+  __goblint_check(x <= 42);
+
+  // Succeeds with write, fails with lock
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(x <= 31);
+
+
+  pthread_mutex_lock(&xd);
+  pthread_mutex_lock(&xa);
+  pthread_mutex_unlock(&xd);
+
+  xx = xg;
+  // Succeeds with lock, fails with write
+  // Needs the -tid variant to work here because of the there_i_ruined_it thread
+  __goblint_check(xx <= 17);
+
+
+
+  pthread_create(&tid3, 0, there_i_ruined_it, 0);
+  return 0;
+}
diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
index 81244d00f8..b3cdedcf49 100644
--- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
+++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
@@ -11,135 +11,178 @@
                                                      │ (body)
                                                      ▼
                                                    ┌──────────────────────────────────────────────────────┐
-                                                   │ 11-unrolled-loop-invariant.c:2:7-2:12                │
-                                                   │ (11-unrolled-loop-invariant.c:2:7-2:12)              │
+                                                   │ 11-unrolled-loop-invariant.c:2:3-2:12                │
+                                                   │ (11-unrolled-loop-invariant.c:2:7-2:12 (synthetic))  │
+                                                   │ YAML loc: 11-unrolled-loop-invariant.c:2:3-2:12      │
+                                                   │ GraphML: true; server: false                         │
                                                    └──────────────────────────────────────────────────────┘
                                                      │
                                                      │ i = 0
                                                      ▼
                                                    ┌──────────────────────────────────────────────────────┐
                                                    │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic)     │
-                                    ┌───────────── │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │ ·┐
+                                                   │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │
+                                                   │ YAML loop: 11-unrolled-loop-invariant.c:3:3-4:8      │
+                                                   │ GraphML: true; server: false                         │
+                                    ┌───────────── │ loop: 11-unrolled-loop-invariant.c:3:3-4:8           │ ·┐
                                     │              └──────────────────────────────────────────────────────┘  :
                                     │                │                                                       :
                                     │                │ Pos(i < 10)                                           :
                                     │                ▼                                                       :
                                     │              ┌──────────────────────────────────────────────────────┐  :
                                     │              │ 11-unrolled-loop-invariant.c:4:5-4:8                 │  :
-                                    │              │ (11-unrolled-loop-invariant.c:4:5-4:8)               │ ·┼··························································┐
-                                    │              └──────────────────────────────────────────────────────┘  :                                                          :
-                                    │                │                                                       :                                                          :
-                                    │ Neg(i < 10)    │ i = i + 1                                             :                                                          :
-                                    │                ▼                                                       ▼                                                          :
-                                    │              ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :
-                                    │              │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic)                                                                │  :
-                                    │              │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic))                                                            │  :
-                                    │              └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :
-                                    │                │                                                       │               ▲                                          :
-                                    │                │ Neg(i < 10)                                           │ Pos(i < 10)   │ i = i + 1                                :
-                                    │                ▼                                                       │               │                                          :
-                                    │              ┌──────────────────────────────────────────────────────┐  │             ┌─────────────────────────────────────────┐  :
-                                    │              │ 11-unrolled-loop-invariant.c:6:7-6:12                │  │             │ 11-unrolled-loop-invariant.c:4:5-4:8    │  :
-                                    └────────────▶ │ (11-unrolled-loop-invariant.c:6:7-6:12)              │  └───────────▶ │ (11-unrolled-loop-invariant.c:4:5-4:8)  │ ◀┘
-                                                   └──────────────────────────────────────────────────────┘                └─────────────────────────────────────────┘
+                                    │              │ (11-unrolled-loop-invariant.c:4:5-4:8)               │  :
+                                    │              │ YAML loc: 11-unrolled-loop-invariant.c:4:5-4:8       │  :
+                                    │              │ GraphML: true; server: true                          │ ·┼····································································┐
+                                    │              └──────────────────────────────────────────────────────┘  :                                                                    :
+                                    │                │                                                       :                                                                    :
+                                    │                │ i = i + 1                                             :                                                                    :
+                                    │ Neg(i < 10)    ▼                                                       ▼                                                                    :
+                                    │              ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :
+                                    │              │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic)                                                                          │  :
+                                    │              │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic))                                                                      │  :
+                                    │              │ YAML loop: 11-unrolled-loop-invariant.c:3:3-4:8                                                                           │  :
+                                    │              │ GraphML: true; server: false                                                                                              │  :
+                                    │              │ loop: 11-unrolled-loop-invariant.c:3:3-4:8                                                                                │  :
+                                    │              └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :
+                                    │                │                                                       │               ▲                                                    :
+                                    │                │ Neg(i < 10)                                           │ Pos(i < 10)   │ i = i + 1                                          :
+                                    │                ▼                                                       │               │                                                    :
+                                    │              ┌──────────────────────────────────────────────────────┐  │             ┌───────────────────────────────────────────────────┐  :
+                                    │              │ 11-unrolled-loop-invariant.c:6:3-6:19                │  │             │ 11-unrolled-loop-invariant.c:4:5-4:8              │  :
+                                    │              │ (11-unrolled-loop-invariant.c:6:7-6:12 (synthetic))  │  │             │ (11-unrolled-loop-invariant.c:4:5-4:8)            │  :
+                                    │              │ YAML loc: 11-unrolled-loop-invariant.c:6:3-6:19      │  │             │ YAML loc: 11-unrolled-loop-invariant.c:4:5-4:8    │  :
+                                    └────────────▶ │ GraphML: true; server: false                         │  └───────────▶ │ GraphML: true; server: true                       │ ◀┘
+                                                   └──────────────────────────────────────────────────────┘                └───────────────────────────────────────────────────┘
                                                      │
                                                      │ j = 0
                                                      ▼
                                                    ┌──────────────────────────────────────────────────────┐
-                                                   │ 11-unrolled-loop-invariant.c:6:14-6:19               │
-                                                   │ (11-unrolled-loop-invariant.c:6:14-6:19)             │
+                                                   │ 11-unrolled-loop-invariant.c:6:3-6:19 (synthetic)    │
+                                                   │ (11-unrolled-loop-invariant.c:6:14-6:19 (synthetic)) │
+                                                   │ GraphML: true; server: false                         │
                                                    └──────────────────────────────────────────────────────┘
                                                      │
                                                      │ k = 0
                                                      ▼
-                                                   ┌──────────────────────────────────────────────────────┐                ┌─────────────────────────────────────────┐             ┌──────────────────┐
-                                                   │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic)    │  Neg(j < 10)   │ 11-unrolled-loop-invariant.c:12:3-12:11 │  return 0   │ return of main() │
-                                    ┌············· │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │ ─────────────▶ │ (unknown)                               │ ──────────▶ │                  │
-                                    :              └──────────────────────────────────────────────────────┘                └─────────────────────────────────────────┘             └──────────────────┘
-                                    :                │                                                                       ▲                                         Neg(j < 10)
-                                    :                │ Pos(j < 10)                                                           └────────────────────────────────────────────────────────────────────────────────┐
-                                    :                ▼                                                                                                                                                        │
-                                    :              ┌──────────────────────────────────────────────────────┐                                                                                                   │
-                                    :              │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)    │                                                                                                   │
-         ┌──────────────────────────┼───────────── │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ ····························································┐                                     │
-         │                          :              └──────────────────────────────────────────────────────┘                                                             :                                     │
-         │                          :                │                                                                                                                  :                                     │
-         │                          :                │ Pos(k < 100)                                                                                                     :                                     │
-         │                          :                ▼                                                                                                                  :                                     │
-         │                          :              ┌──────────────────────────────────────────────────────┐                                                             :                                     │
-         │                          :              │ 11-unrolled-loop-invariant.c:9:7-9:10                │                                                             :                                     │
-         │                          :              │ (11-unrolled-loop-invariant.c:9:7-9:10)              │ ····························································┼············┐                        │
-         │                          :              └──────────────────────────────────────────────────────┘                                                             :            :                        │
-         │                          :                │                                                                                                                  :            :                        │
-         │                          :                │ k = k + 1                                                             ┌──────────────────────────────────────────┼────────────┼────────────────────────┼─────────────┐
-         │                          :                ▼                                                                       │                                          :            :                        │             │
-         │                          :              ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                        │             │
-         │                          :              │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)                                                               │  :            :                        │             │
-         │                          :              │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic))                                                            │  :            :                        │             │
-         │                          :              └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :            :                        │             │
-         │                          :                │                                                       :               ▲                                          :            :                        │             │
-         │                          :                │ Pos(k < 100)                                          :               │ k = k + 1                                :            :                        │             │
-         │                          :                ▼                                                       :               │                                          :            :                        │             │
-         │                          :              ┌──────────────────────────────────────────────────────┐  :               │                                          :            :                        │             │
-         │                          :              │ 11-unrolled-loop-invariant.c:9:7-9:10                │  :               │                                          :            :                        │             │
-         │                          :              │ (11-unrolled-loop-invariant.c:9:7-9:10)              │ ─┼───────────────┘                                          :            :                        │             │
-         │                          :              └──────────────────────────────────────────────────────┘  :                                                          :            :                        │             │
-         │                          :                :                                                       :                                                          :            :                        │             │
-    ┌────┘                          :                :                                                       :                                                          :            :                        │             │
-    │                               :                ▼                                                       :                                                          :            :                        │             │
-    │                               :              ┌──────────────────────────────────────────────────────┐  :                                                          :            :                        │             │
-    │                               :              │ 11-unrolled-loop-invariant.c:9:7-9:10                │  :                                                          :            :                        │             │
-    │    ┌··························┼············▶ │ (11-unrolled-loop-invariant.c:9:7-9:10)              │ ◀┼───────────────┐                                          :            :                        │             │
-    │    :                          :              └──────────────────────────────────────────────────────┘  :               │                                          :            :                        │             │
-    │    :                          :                │                                                       :               │                                          :            :                        │             │
-    │    :                          :                │ k = k + 1                                             :               │ Pos(k < 100)                             :            :                        │             │
-    │    :                          :                ▼                                                       ▼               │                                          :            :                        │             │
-    │    :                          :              ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                        │             │
-    │    :        k = k + 1         :              │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)                                                               │  :            :                        │             │
-    │    :    ┌─────────────────────┼────────────▶ │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic))                                                            │ ◀┼············┼···················┐    │             │
-    │    :    │                     :              └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :            :                   :    │             │
-    │    :    │                     :                │                                                                                                                  :            :                   :    │             │
-    │    :    │                     :                │ Neg(k < 100)                                                                                                     :            :                   :    │             │
-    │    :    │                     :                ▼                                                                                                                  :            :                   :    │             │
-    │    :    │                     :              ┌──────────────────────────────────────────────────────┐                                                             :            :                   :    │             │
-    │    :    │                     :              │ 11-unrolled-loop-invariant.c:10:5-10:8               │                                                             :            :                   :    │             │
-    │    :    │    ┌────────────────┼────────────▶ │ (11-unrolled-loop-invariant.c:10:5-10:8)             │ ◀···························································┼············┼···················┼····┼·············┼····┐
-    │    :    │    │                :              └──────────────────────────────────────────────────────┘                                                             :            :                   :    │             │    :
-    │    :    │    │                :                │                                                                                                                  :            :                   :    │             │    :
-    │    :    │    │                :                │ j = j + 1                                                             ┌──────────────────────────────────────────┼────────────┼───────────────────┼────┘             │    :
-    │    :    │    │                :                ▼                                                                       │                                          :            :                   :                  │    :
-    │    :    │    │                :              ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                   :                  │    :
-    │    :    │    │                :              │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic)                                                               │  :            :                   :                  │    :
-    │    :    │    │ Neg(k < 100)   └············▶ │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic))                                                            │ ◀┼────────────┼───────────────────┼────┐             │    :
-    │    :    │    │                               └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :            :                   :    │             │    :
-    │    :    │    │                                 │                                                                                                                  :            :                   :    │             │    :
-    │    :    │    │                                 │ Pos(j < 10)                                                                                                      :            :                   :    │             │    :
-    │    :    │    │                                 ▼                                                                                                                  :            :                   :    │             │    :
-    │    :    │    │                               ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                   :    │             │    :
-    │    :    │    │                               │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)                                                               │  :            :                   :    │             │    :
-    │    :    │    └────────────────────────────── │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic))                                                            │ ◀┘            :                   :    │ j = j + 1   │    :
-    │    :    │                                    └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘               :                   :    │             │    :
-    │    :    │                                      │                                                                       :                                                       :                   :    │             │    :
-    │    :    │                                      │ Pos(k < 100)                                                          └·······················································┼···················┘    │             │    :
-    │    :    │                                      ▼                                                                                                                               :                        │             │    :
-    │    :    │                                    ┌──────────────────────────────────────────────────────┐                                                                          :                        │             │    :
-    │    :    │                                    │ 11-unrolled-loop-invariant.c:9:7-9:10                │                                                                          :                        │             │    :
-    │    :    └─────────────────────────────────── │ (11-unrolled-loop-invariant.c:9:7-9:10)              │ ◀········································································┘                   ┌····┼·············┼····┘
-    │    :                                         └──────────────────────────────────────────────────────┘                                                                                              :    │             │
-    │    :                                           :                                                                                                                                                   :    │             │
-    │    └···········································┘                                                                                                                                                   :    │             │
-    │                                                                                                                                                                                                    :    │             │
-    │                                                                                                                                                                                                    :    │             │
-    │                                                ┌···················································································································································┘    │             │
-    │                                                :                                                                                                                                                        │             │
-    │                                              ┌──────────────────────────────────────────────────────┐                                                                                                   │             │
-    │                              Neg(k < 100)    │ 11-unrolled-loop-invariant.c:10:5-10:8               │                                                                                                   │             │
-    └────────────────────────────────────────────▶ │ (11-unrolled-loop-invariant.c:10:5-10:8)             │ ──────────────────────────────────────────────────────────────────────────────────────────────────┘             │
-                                                   └──────────────────────────────────────────────────────┘                                                                                                                 │
-                                                     ▲                                                      Neg(k < 100)                                                                                                    │
-                                                     └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+                                                   ┌──────────────────────────────────────────────────────┐                ┌───────────────────────────────────────────────────┐             ┌──────────────────┐
+                                                   │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic)    │                │ 11-unrolled-loop-invariant.c:12:3-12:11           │             │                  │
+                                                   │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │                │ (11-unrolled-loop-invariant.c:12:10-12:11)        │             │                  │
+                                                   │ YAML loop: 11-unrolled-loop-invariant.c:7:3-11:3     │                │ YAML loc: 11-unrolled-loop-invariant.c:12:3-12:11 │             │ return of main() │
+                                                   │ GraphML: true; server: false                         │  Neg(j < 10)   │ GraphML: true; server: true                       │  return 0   │                  │
+                                    ┌············· │ loop: 11-unrolled-loop-invariant.c:7:3-11:3          │ ─────────────▶ │                                                   │ ──────────▶ │                  │
+                                    :              └──────────────────────────────────────────────────────┘                └───────────────────────────────────────────────────┘             └──────────────────┘
+                                    :                │                                                                       ▲                                                   Neg(j < 10)
+                                    :                │ Pos(j < 10)                                                           └──────────────────────────────────────────────────────────────────────────────────────────┐
+                                    :                ▼                                                                                                                                                                  │
+                                    :              ┌──────────────────────────────────────────────────────┐                                                                                                             │
+                                    :              │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)    │                                                                                                             │
+                                    :              │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │                                                                                                             │
+                                    :              │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10     │                                                                                                             │
+                                    :              │ GraphML: true; server: false                         │                                                                                                             │
+         ┌──────────────────────────┼───────────── │ loop: 11-unrolled-loop-invariant.c:8:5-9:10          │ ······································································┐                                     │
+         │                          :              └──────────────────────────────────────────────────────┘                                                                       :                                     │
+         │                          :                │                                                                                                                            :                                     │
+         │                          :                │ Pos(k < 100)                                                                                                               :                                     │
+         │                          :                ▼                                                                                                                            :                                     │
+         │                          :              ┌──────────────────────────────────────────────────────┐                                                                       :                                     │
+         │                          :              │ 11-unrolled-loop-invariant.c:9:7-9:10                │                                                                       :                                     │
+         │                          :              │ (11-unrolled-loop-invariant.c:9:7-9:10)              │                                                                       :                                     │
+         │                          :              │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10      │                                                                       :                                     │
+         │                          :              │ GraphML: true; server: true                          │ ······································································┼············┐                        │
+         │                          :              └──────────────────────────────────────────────────────┘                                                                       :            :                        │
+         │                          :                │                                                                                                                            :            :                        │
+         │                          :                │ k = k + 1                                                             ┌────────────────────────────────────────────────────┼────────────┼────────────────────────┼─────────────┐
+         │                          :                ▼                                                                       │                                                    :            :                        │             │
+         │                          :              ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                        │             │
+         │                          :              │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)                                                                         │  :            :                        │             │
+         │                          :              │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic))                                                                      │  :            :                        │             │
+         │                          :              │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10                                                                          │  :            :                        │             │
+         │                          :              │ GraphML: true; server: false                                                                                              │  :            :                        │             │
+         │                          :              │ loop: 11-unrolled-loop-invariant.c:8:5-9:10                                                                               │  :            :                        │             │
+         │                          :              └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :            :                        │             │
+         │                          :                │                                                       :               ▲                                                    :            :                        │             │
+         │                          :                │ Pos(k < 100)                                          :               │ k = k + 1                                          :            :                        │             │
+         │                          :                ▼                                                       :               │                                                    :            :                        │             │
+         │                          :              ┌──────────────────────────────────────────────────────┐  :               │                                                    :            :                        │             │
+         │                          :              │ 11-unrolled-loop-invariant.c:9:7-9:10                │  :               │                                                    :            :                        │             │
+         │                          :              │ (11-unrolled-loop-invariant.c:9:7-9:10)              │  :               │                                                    :            :                        │             │
+         │                          :              │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10      │  :               │                                                    :            :                        │             │
+         │                          :              │ GraphML: true; server: true                          │ ─┼───────────────┘                                                    :            :                        │             │
+         │                          :              └──────────────────────────────────────────────────────┘  :                                                                    :            :                        │             │
+         │                          :                :                                                       :                                                                    :            :                        │             │
+    ┌────┘                          :                :                                                       :                                                                    :            :                        │             │
+    │                               :                ▼                                                       :                                                                    :            :                        │             │
+    │                               :              ┌──────────────────────────────────────────────────────┐  :                                                                    :            :                        │             │
+    │                               :              │ 11-unrolled-loop-invariant.c:9:7-9:10                │  :                                                                    :            :                        │             │
+    │                               :              │ (11-unrolled-loop-invariant.c:9:7-9:10)              │  :                                                                    :            :                        │             │
+    │                               :              │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10      │  :                                                                    :            :                        │             │
+    │    ┌··························┼············▶ │ GraphML: true; server: true                          │ ◀┼───────────────┐                                                    :            :                        │             │
+    │    :                          :              └──────────────────────────────────────────────────────┘  :               │                                                    :            :                        │             │
+    │    :                          :                │                                                       :               │                                                    :            :                        │             │
+    │    :                          :                │ k = k + 1                                             :               │ Pos(k < 100)                                       :            :                        │             │
+    │    :                          :                ▼                                                       ▼               │                                                    :            :                        │             │
+    │    :                          :              ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                        │             │
+    │    :                          :              │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)                                                                         │  :            :                        │             │
+    │    :                          :              │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic))                                                                      │  :            :                        │             │
+    │    :                          :              │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10                                                                          │  :            :                        │             │
+    │    :        k = k + 1         :              │ GraphML: true; server: false                                                                                              │  :            :                        │             │
+    │    :    ┌─────────────────────┼────────────▶ │ loop: 11-unrolled-loop-invariant.c:8:5-9:10                                                                               │ ◀┼············┼···················┐    │             │
+    │    :    │                     :              └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :            :                   :    │             │
+    │    :    │                     :                │                                                                                                                            :            :                   :    │             │
+    │    :    │                     :                │ Neg(k < 100)                                                                                                               :            :                   :    │             │
+    │    :    │                     :                ▼                                                                                                                            :            :                   :    │             │
+    │    :    │                     :              ┌──────────────────────────────────────────────────────┐                                                                       :            :                   :    │             │
+    │    :    │                     :              │ 11-unrolled-loop-invariant.c:10:5-10:8               │                                                                       :            :                   :    │             │
+    │    :    │                     :              │ (11-unrolled-loop-invariant.c:10:5-10:8)             │                                                                       :            :                   :    │             │
+    │    :    │                     :              │ YAML loc: 11-unrolled-loop-invariant.c:10:5-10:8     │                                                                       :            :                   :    │             │
+    │    :    │    ┌────────────────┼────────────▶ │ GraphML: true; server: true                          │ ◀·····································································┼············┼···················┼····┼·············┼····┐
+    │    :    │    │                :              └──────────────────────────────────────────────────────┘                                                                       :            :                   :    │             │    :
+    │    :    │    │                :                │                                                                                                                            :            :                   :    │             │    :
+    │    :    │    │                :                │ j = j + 1                                                             ┌────────────────────────────────────────────────────┼────────────┼───────────────────┼────┘             │    :
+    │    :    │    │                :                ▼                                                                       │                                                    :            :                   :                  │    :
+    │    :    │    │                :              ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                   :                  │    :
+    │    :    │    │                :              │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic)                                                                         │  :            :                   :                  │    :
+    │    :    │    │                :              │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic))                                                                      │  :            :                   :                  │    :
+    │    :    │    │ Neg(k < 100)   :              │ YAML loop: 11-unrolled-loop-invariant.c:7:3-11:3                                                                          │  :            :                   :                  │    :
+    │    :    │    │                :              │ GraphML: true; server: false                                                                                              │  :            :                   :                  │    :
+    │    :    │    │                └············▶ │ loop: 11-unrolled-loop-invariant.c:7:3-11:3                                                                               │ ◀┼────────────┼───────────────────┼────┐             │    :
+    │    :    │    │                               └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘  :            :                   :    │             │    :
+    │    :    │    │                                 │                                                                                                                            :            :                   :    │             │    :
+    │    :    │    │                                 │ Pos(j < 10)                                                                                                                :            :                   :    │             │    :
+    │    :    │    │                                 ▼                                                                                                                            :            :                   :    │             │    :
+    │    :    │    │                               ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐  :            :                   :    │             │    :
+    │    :    │    │                               │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic)                                                                         │  :            :                   :    │             │    :
+    │    :    │    │                               │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic))                                                                      │  :            :                   :    │             │    :
+    │    :    │    │                               │ YAML loop: 11-unrolled-loop-invariant.c:8:5-9:10                                                                          │  :            :                   :    │ j = j + 1   │    :
+    │    :    │    │                               │ GraphML: true; server: false                                                                                              │  :            :                   :    │             │    :
+    │    :    │    └────────────────────────────── │ loop: 11-unrolled-loop-invariant.c:8:5-9:10                                                                               │ ◀┘            :                   :    │             │    :
+    │    :    │                                    └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘               :                   :    │             │    :
+    │    :    │                                      │                                                                       :                                                                 :                   :    │             │    :
+    │    :    │                                      │ Pos(k < 100)                                                          └·································································┼···················┘    │             │    :
+    │    :    │                                      ▼                                                                                                                                         :                        │             │    :
+    │    :    │                                    ┌──────────────────────────────────────────────────────┐                                                                                    :                        │             │    :
+    │    :    │                                    │ 11-unrolled-loop-invariant.c:9:7-9:10                │                                                                                    :                        │             │    :
+    │    :    │                                    │ (11-unrolled-loop-invariant.c:9:7-9:10)              │                                                                                    :                        │             │    :
+    │    :    │                                    │ YAML loc: 11-unrolled-loop-invariant.c:9:7-9:10      │                                                                                    :                        │             │    :
+    │    :    └─────────────────────────────────── │ GraphML: true; server: true                          │ ◀··················································································┘                   ┌····┼·············┼····┘
+    │    :                                         └──────────────────────────────────────────────────────┘                                                                                                        :    │             │
+    │    :                                           :                                                                                                                                                             :    │             │
+    │    └···········································┘                                                                                                                                                             :    │             │
+    │                                                                                                                                                                                                              :    │             │
+    │                                                                                                                                                                                                              :    │             │
+    │                                                ┌·····························································································································································┘    │             │
+    │                                                :                                                                                                                                                                  │             │
+    │                                              ┌──────────────────────────────────────────────────────┐                                                                                                             │             │
+    │                                              │ 11-unrolled-loop-invariant.c:10:5-10:8               │                                                                                                             │             │
+    │                                              │ (11-unrolled-loop-invariant.c:10:5-10:8)             │                                                                                                             │             │
+    │                              Neg(k < 100)    │ YAML loc: 11-unrolled-loop-invariant.c:10:5-10:8     │                                                                                                             │             │
+    └────────────────────────────────────────────▶ │ GraphML: true; server: true                          │ ────────────────────────────────────────────────────────────────────────────────────────────────────────────┘             │
+                                                   └──────────────────────────────────────────────────────┘                                                                                                                           │
+                                                     ▲                                                      Neg(k < 100)                                                                                                              │
+                                                     └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 
-  $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 11-unrolled-loop-invariant.c
+  $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' 11-unrolled-loop-invariant.c
   [Info] unrolling loop at 11-unrolled-loop-invariant.c:3:3-4:8 with factor 5
   [Info] unrolling loop at 11-unrolled-loop-invariant.c:8:5-9:10 with factor 5
   [Info] unrolling loop at 11-unrolled-loop-invariant.c:7:3-11:3 with factor 5
@@ -168,63 +211,190 @@
   [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:12-8:19)
   [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:7:10-7:16)
   [Info][Witness] witness generation summary:
-    total generation entries: 19
-
-TODO: use yamlWitnessStrip for this
-
-  $ cat witness.yml | grep -A 1 'value:'
-        value: i == 10
-        format: c_expression
-  --
-        value: i == 10
-        format: c_expression
-  --
-        value: j == 10
-        format: c_expression
-  --
-        value: k == 100
-        format: c_expression
-  --
-        value: i == 10
-        format: c_expression
-  --
-        value: k == 100
-        format: c_expression
-  --
-        value: ((((j == 1 || j == 4) || j == 0) || j == 3) || j == 2) || (5 <= j &&
-          j <= 9)
-  --
-        value: (((((5 <= i && i <= 9) || i == 4) || i == 3) || i == 2) || i == 1) ||
-          i == 0
-  --
-        value: i == 10
-        format: c_expression
-  --
-        value: j == 0
-        format: c_expression
-  --
-        value: (((((5 <= k && k <= 99) || k == 4) || k == 3) || k == 2) || k == 1) ||
-          k == 0
-  --
-        value: i == 10
-        format: c_expression
-  --
-        value: j == 0
-        format: c_expression
-  --
-        value: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) ||
-          i == 0
-  --
-        value: i == 10
-        format: c_expression
-  --
-        value: (((((((k == 100 && (((j == 2 || (5 <= j && j <= 9)) || j == 1) || j ==
-          4)) || ((5 <= k && k <= 100) && j == 0)) || (j == 0 && k == 4)) || (j == 0
-  --
-        value: i == 10
-        format: c_expression
-  --
-        value: ((k == 100 && (((j == 2 || (5 <= j && j <= 10)) || j == 1) || j == 4))
-          || (j == 0 && k == 0)) || (j == 3 && k == 100)
-
+    total generation entries: 16
 
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: loop_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 8
+      column: 4
+      function: main
+    loop_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 8
+      column: 4
+      function: main
+    loop_invariant:
+      string: (((((((k == 100 && (((j == 2 || (5 <= j && j <= 9)) || j == 1) || j ==
+        4)) || ((5 <= k && k <= 100) && j == 0)) || (j == 0 && k == 4)) || (j == 0 &&
+        k == 3)) || (j == 0 && k == 2)) || (j == 0 && k == 1)) || (j == 0 && k == 0))
+        || (j == 3 && k == 100)
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 2
+      function: main
+    loop_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 2
+      function: main
+    loop_invariant:
+      string: ((k == 100 && (((j == 2 || (5 <= j && j <= 10)) || j == 1) || j == 4))
+        || (j == 0 && k == 0)) || (j == 3 && k == 100)
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 3
+      column: 2
+      function: main
+    loop_invariant:
+      string: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) ||
+        i == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: k == 100
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 10
+      column: 4
+      function: main
+    location_invariant:
+      string: k == 100
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 10
+      column: 4
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 10
+      column: 4
+      function: main
+    location_invariant:
+      string: ((((j == 1 || j == 4) || j == 0) || j == 3) || j == 2) || (5 <= j && j
+        <= 9)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 6
+      function: main
+    location_invariant:
+      string: j == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 6
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 6
+      function: main
+    location_invariant:
+      string: (((((5 <= k && k <= 99) || k == 4) || k == 3) || k == 2) || k == 1) ||
+        k == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 6
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 11-unrolled-loop-invariant.c
+      file_hash: $FILE_HASH
+      line: 4
+      column: 4
+      function: main
+    location_invariant:
+      string: (((((5 <= i && i <= 9) || i == 4) || i == 3) || i == 2) || i == 1) ||
+        i == 0
+      type: assertion
+      format: C
diff --git a/tests/regression/56-witness/05-prec-problem.c b/tests/regression/56-witness/05-prec-problem.c
index 132ba6b466..08c665ce12 100644
--- a/tests/regression/56-witness/05-prec-problem.c
+++ b/tests/regression/56-witness/05-prec-problem.c
@@ -1,4 +1,4 @@
-//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types[+] precondition_loop_invariant
+//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]'
 #include <stdlib.h>
 #include <goblint.h>
 
@@ -9,7 +9,8 @@ int foo(int* ptr1, int* ptr2){
     } else {
         result = 1;
     }
-    // Look at the generated witness.yml to check whether there are contradictory precondition_loop_invariant[s]
+
+    while (0); // cram test checks for precondition invariant soundness
     return result;
 }
 
diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t
new file mode 100644
index 0000000000..4c7dd02fa9
--- /dev/null
+++ b/tests/regression/56-witness/05-prec-problem.t
@@ -0,0 +1,62 @@
+  $ goblint --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' 05-prec-problem.c
+  [Success][Assert] Assertion "y != z" will succeed (05-prec-problem.c:22:5-22:28)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 13
+    dead: 0
+    total lines: 13
+  [Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (05-prec-problem.c:13:12-13:13)
+  [Info][Witness] witness generation summary:
+    total generation entries: 6
+
+TODO: Don't generate duplicate entries from each context: should have generated just 3.
+
+Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`,
+and separately invariants `result == 0` and `result == 1`.
+The sound invariant is `result == 1 || result == 0`.
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 4
+      function: foo
+    loop_invariant:
+      string: result == 1 || result == 0
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 4
+      function: foo
+    loop_invariant:
+      string: '*ptr2 == 5'
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
+  - entry_type: precondition_loop_invariant
+    location:
+      file_name: 05-prec-problem.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 4
+      function: foo
+    loop_invariant:
+      string: '*ptr1 == 5'
+      type: assertion
+      format: C
+    precondition:
+      string: '*ptr1 == 5 && *ptr2 == 5'
+      type: assertion
+      format: C
diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t
index 64ab054549..bd7012ec25 100644
--- a/tests/regression/56-witness/08-witness-all-locals.t
+++ b/tests/regression/56-witness/08-witness-all-locals.t
@@ -6,7 +6,40 @@
   [Info][Witness] witness generation summary:
     total generation entries: 3
 
-TODO: check witness.yml content with yamlWitnessStrip
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 08-witness-all-locals.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: y == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 08-witness-all-locals.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 5
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 08-witness-all-locals.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 4
+      function: main
+    location_invariant:
+      string: x == 5
+      type: assertion
+      format: C
 
 Fewer entries are emitted if locals from nested block scopes are excluded:
 
@@ -19,4 +52,26 @@ Fewer entries are emitted if locals from nested block scopes are excluded:
   [Info][Witness] witness generation summary:
     total generation entries: 2
 
-TODO: check witness.yml content with yamlWitnessStrip
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 08-witness-all-locals.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 5
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 08-witness-all-locals.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 4
+      function: main
+    location_invariant:
+      string: x == 5
+      type: assertion
+      format: C
diff --git a/tests/regression/56-witness/10-apron-unassume-interval.c b/tests/regression/56-witness/10-apron-unassume-interval.c
index e35d42d563..1ee6117c61 100644
--- a/tests/regression/56-witness/10-apron-unassume-interval.c
+++ b/tests/regression/56-witness/10-apron-unassume-interval.c
@@ -3,7 +3,7 @@
 // Using polyhedra instead of octagon, because the former has no narrowing and really needs the witness.
 int main() {
   int i = 0;
-  while (i < 100) {
+  while (i < 100) { // TODO: location invariant before loop doesn't work anymore
     i++;
   }
   assert(i == 100);
diff --git a/tests/regression/56-witness/10-apron-unassume-interval.yml b/tests/regression/56-witness/10-apron-unassume-interval.yml
index 12cc344957..f7958922ae 100644
--- a/tests/regression/56-witness/10-apron-unassume-interval.yml
+++ b/tests/regression/56-witness/10-apron-unassume-interval.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
@@ -22,11 +22,11 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 100LL - (long long )i >= 0LL
     type: assertion
     format: C
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 4e078bcd-9e55-4874-a86e-0563927704a5
@@ -50,7 +50,7 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: (long long )i >= 0LL
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/11-base-unassume-interval.c b/tests/regression/56-witness/11-base-unassume-interval.c
index bfecee5bbe..f8b685fcb1 100644
--- a/tests/regression/56-witness/11-base-unassume-interval.c
+++ b/tests/regression/56-witness/11-base-unassume-interval.c
@@ -3,7 +3,7 @@
 
 int main() {
   int i = 0;
-  while (i < 100) {
+  while (i < 100) { // TODO: location invariant before loop doesn't work anymore
     i++;
   }
   assert(i == 100);
diff --git a/tests/regression/56-witness/11-base-unassume-interval.yml b/tests/regression/56-witness/11-base-unassume-interval.yml
index bb4740c7b0..df939b7ca4 100644
--- a/tests/regression/56-witness/11-base-unassume-interval.yml
+++ b/tests/regression/56-witness/11-base-unassume-interval.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
@@ -22,11 +22,11 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 100LL - (long long )i >= 0LL
     type: assertion
     format: C
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 4e078bcd-9e55-4874-a86e-0563927704a5
@@ -50,7 +50,7 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: (long long )i >= 0LL
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/14-base-unassume-precondition.c b/tests/regression/56-witness/14-base-unassume-precondition.c
index 8e6a1b3c73..23b2d8b923 100644
--- a/tests/regression/56-witness/14-base-unassume-precondition.c
+++ b/tests/regression/56-witness/14-base-unassume-precondition.c
@@ -3,7 +3,7 @@
 
 void foo(int n) {
   int i = 0;
-  while (i < n) {
+  while (i < n) { // TODO: (precondition) location invariant before loop doesn't work anymore
     i++;
   }
   assert(i == n);
diff --git a/tests/regression/56-witness/14-base-unassume-precondition.yml b/tests/regression/56-witness/14-base-unassume-precondition.yml
index df4bbc8dc7..2d84e4ea9f 100644
--- a/tests/regression/56-witness/14-base-unassume-precondition.yml
+++ b/tests/regression/56-witness/14-base-unassume-precondition.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 26e6d2de-13a6-4610-9b08-ee3d9e6b9338
@@ -21,7 +21,7 @@
     line: 6
     column: 2
     function: foo
-  location_invariant:
+  loop_invariant:
     string: 0 <= i
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/20-apron-unassume-global.c b/tests/regression/56-witness/20-apron-unassume-global.c
index 6ad4146ba2..f8cdc63ba4 100644
--- a/tests/regression/56-witness/20-apron-unassume-global.c
+++ b/tests/regression/56-witness/20-apron-unassume-global.c
@@ -3,7 +3,7 @@
 
 int i = 0;
 int main() {
-  while (i < 100) {
+  while (i < 100) { // TODO: location invariant before loop doesn't work anymore
     i++;
   }
   assert(i == 100);
diff --git a/tests/regression/56-witness/20-apron-unassume-global.yml b/tests/regression/56-witness/20-apron-unassume-global.yml
index 641adcac2b..6f824d4f9f 100644
--- a/tests/regression/56-witness/20-apron-unassume-global.yml
+++ b/tests/regression/56-witness/20-apron-unassume-global.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
@@ -22,11 +22,11 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 100LL - (long long )i >= 0LL
     type: assertion
     format: C
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 4e078bcd-9e55-4874-a86e-0563927704a5
@@ -50,7 +50,7 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: (long long )i >= 0LL
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.c b/tests/regression/56-witness/26-mine-tutorial-ex4.6.c
index d497c6344a..129f7e809a 100644
--- a/tests/regression/56-witness/26-mine-tutorial-ex4.6.c
+++ b/tests/regression/56-witness/26-mine-tutorial-ex4.6.c
@@ -2,7 +2,7 @@
 #include <goblint.h>
 int main() {
   int x = 40;
-  while (x != 0) {
+  while (x != 0) { // TODO: location invariant before loop doesn't work anymore
     __goblint_check(x <= 40);
     x--;
     __goblint_check(x >= 0);
diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml
index 1dc21aeacc..5e35fbc911 100644
--- a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml
+++ b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941482
@@ -19,7 +19,7 @@
     line: 5
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= x && x <= 40
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.c b/tests/regression/56-witness/27-mine-tutorial-ex4.7.c
index 10f83ba6e2..2589c596b8 100644
--- a/tests/regression/56-witness/27-mine-tutorial-ex4.7.c
+++ b/tests/regression/56-witness/27-mine-tutorial-ex4.7.c
@@ -3,7 +3,7 @@
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
   int x = 0;
-  while (__VERIFIER_nondet_bool() == 0) {
+  while (__VERIFIER_nondet_bool() == 0) { // TODO: location invariant before loop doesn't work anymore
     __goblint_check(0 <= x);
     __goblint_check(x <= 40);
     if (__VERIFIER_nondet_bool() == 0) {
diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml
index c0473adecb..06bae19e07 100644
--- a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml
+++ b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: e17f9860-95af-4213-a767-ab4876ead27e
@@ -17,9 +17,9 @@
     file_name: 27-mine-tutorial-ex4.7.c
     file_hash: 4d06e38718d405171bd503e630f6c7a247bb3b0d3c1c6c951466e4989883b43c
     line: 6
-    column: 8
+    column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= x && x <= 40
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.c b/tests/regression/56-witness/28-mine-tutorial-ex4.8.c
index 6892267fc8..b2881cdfa6 100644
--- a/tests/regression/56-witness/28-mine-tutorial-ex4.8.c
+++ b/tests/regression/56-witness/28-mine-tutorial-ex4.8.c
@@ -3,7 +3,7 @@
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
   int v = 0;
-  while (__VERIFIER_nondet_bool() == 0) {
+  while (__VERIFIER_nondet_bool() == 0) { // TODO: location invariant before loop doesn't work anymore
     __goblint_check(0 <= v);
     __goblint_check(v <= 1);
     if (v == 0)
diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml
index 2ccf85fdd2..49bd9b028b 100644
--- a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml
+++ b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 299c2080-fb13-4879-be2b-5d2758465577
@@ -19,7 +19,7 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= v && v <= 1
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.c b/tests/regression/56-witness/29-mine-tutorial-ex4.10.c
index 655c19e08e..437e20130c 100644
--- a/tests/regression/56-witness/29-mine-tutorial-ex4.10.c
+++ b/tests/regression/56-witness/29-mine-tutorial-ex4.10.c
@@ -3,7 +3,7 @@
 #include <goblint.h>
 int main() {
   int v = 1; // Not explicitly stated in Miné's example
-  while (v <= 50) {
+  while (v <= 50) { // TODO: location invariant before loop doesn't work anymore
     __goblint_check(1 <= v);
     v += 2;
     __goblint_check(v <= 52);
diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml
index f82c321f73..39fa14eb23 100644
--- a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml
+++ b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: f04fe372-3d6e-4a80-9567-80c64bd7fd03
@@ -19,7 +19,7 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 1 <= v && v <= 52
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/35-hh-ex1b.yml b/tests/regression/56-witness/35-hh-ex1b.yml
index 530ae08906..4d7b98fd17 100644
--- a/tests/regression/56-witness/35-hh-ex1b.yml
+++ b/tests/regression/56-witness/35-hh-ex1b.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 1a354f1e-76e8-40e9-808a-8d5efbe35496
@@ -17,9 +17,9 @@
     file_name: 35-hh-ex1b.c
     file_hash: 9fe07d5f950140350848bae4342d9d1b7c6c9f625f6985746089a36a37243600
     line: 7
-    column: 2
+    column: 4
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= i && i <= 99
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/36-hh-ex2b.c b/tests/regression/56-witness/36-hh-ex2b.c
index f8d35f28bd..41c5fcf71e 100644
--- a/tests/regression/56-witness/36-hh-ex2b.c
+++ b/tests/regression/56-witness/36-hh-ex2b.c
@@ -3,7 +3,7 @@
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
   int n = 0;
-  while (1) {
+  while (1) { // TODO: location invariant before loop doesn't work anymore
     __goblint_check(n <= 60);
     if (__VERIFIER_nondet_bool()) {
       if (n < 60) {
diff --git a/tests/regression/56-witness/36-hh-ex2b.yml b/tests/regression/56-witness/36-hh-ex2b.yml
index 9ec4a7845a..64e1b79f16 100644
--- a/tests/regression/56-witness/36-hh-ex2b.yml
+++ b/tests/regression/56-witness/36-hh-ex2b.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 9589b9d4-edce-4043-8413-279703946762
@@ -19,7 +19,7 @@
     line: 6
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= n && n <= 60
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/38-bh-ex3.c b/tests/regression/56-witness/38-bh-ex3.c
index 633394586f..2a5d07fc1e 100644
--- a/tests/regression/56-witness/38-bh-ex3.c
+++ b/tests/regression/56-witness/38-bh-ex3.c
@@ -4,7 +4,7 @@ extern _Bool __VERIFIER_nondet_bool();
 int main() {
   int m = 0;
   int n = 0;
-  while (1) {
+  while (1) { // TODO: location invariant before loop doesn't work anymore
     __goblint_check(m <= 60);
     __goblint_check(n <= 60);
     if (__VERIFIER_nondet_bool()) {
diff --git a/tests/regression/56-witness/38-bh-ex3.yml b/tests/regression/56-witness/38-bh-ex3.yml
index 8a55e96e3a..cfd80c21c8 100644
--- a/tests/regression/56-witness/38-bh-ex3.yml
+++ b/tests/regression/56-witness/38-bh-ex3.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: bd436e09-244f-45db-a5f4-9337ca997424
@@ -19,7 +19,7 @@
     line: 7
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= m && m <= 60 && 0 <= n && n <= 60
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/39-bh-ex-add.c b/tests/regression/56-witness/39-bh-ex-add.c
index 256e274b73..630ef344a4 100644
--- a/tests/regression/56-witness/39-bh-ex-add.c
+++ b/tests/regression/56-witness/39-bh-ex-add.c
@@ -4,7 +4,7 @@ extern _Bool __VERIFIER_nondet_bool();
 int main() {
   int m = 0;
   int n = 0;
-  while (1) {
+  while (1) { // TODO: location invariant before loop doesn't work anymore
     __goblint_check(m <= 60);
     __goblint_check(n <= 60);
     if (__VERIFIER_nondet_bool()) {
diff --git a/tests/regression/56-witness/39-bh-ex-add.yml b/tests/regression/56-witness/39-bh-ex-add.yml
index c20801d044..d51aa91699 100644
--- a/tests/regression/56-witness/39-bh-ex-add.yml
+++ b/tests/regression/56-witness/39-bh-ex-add.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: bd436e09-244f-45db-a5f4-9337ca997424
@@ -19,7 +19,7 @@
     line: 7
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= m && m <= 60 && 0 <= n && n <= 60
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/41-as-hybrid.c b/tests/regression/56-witness/41-as-hybrid.c
index 7735187036..3a3a4c6ea6 100644
--- a/tests/regression/56-witness/41-as-hybrid.c
+++ b/tests/regression/56-witness/41-as-hybrid.c
@@ -2,7 +2,7 @@
 #include <goblint.h>
 int main() {
   int i = 0;
-  while (1) {
+  while (1) { // TODO: location invariant before loop doesn't work anymore
     i++;
     int j = 0;
     while (j < 10) {
diff --git a/tests/regression/56-witness/41-as-hybrid.yml b/tests/regression/56-witness/41-as-hybrid.yml
index 336657e52d..5ade41e167 100644
--- a/tests/regression/56-witness/41-as-hybrid.yml
+++ b/tests/regression/56-witness/41-as-hybrid.yml
@@ -1,4 +1,4 @@
-- entry_type: location_invariant
+- entry_type: loop_invariant
   metadata:
     format_version: "0.1"
     uuid: 71b761c6-4f85-405e-8ee6-9a3a8f743513
@@ -19,7 +19,7 @@
     line: 5
     column: 2
     function: main
-  location_invariant:
+  loop_invariant:
     string: 0 <= i && i <= 9
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/44-base-unassume-array.yml b/tests/regression/56-witness/44-base-unassume-array.yml
index dbf7fb8e54..ad2e3a3ad2 100644
--- a/tests/regression/56-witness/44-base-unassume-array.yml
+++ b/tests/regression/56-witness/44-base-unassume-array.yml
@@ -21,7 +21,7 @@
     file_name: 44-base-unassume-array.c
     file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726
     line: 7
-    column: 6
+    column: 2
     function: main
   loop_invariant:
     string: 0 <= a[(long )"all_index"]
@@ -50,7 +50,7 @@
     file_name: 44-base-unassume-array.c
     file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726
     line: 7
-    column: 6
+    column: 2
     function: main
   loop_invariant:
     string: a[(long )"all_index"] < 3
diff --git a/tests/regression/66-interval-set-one/62-pfscan_widen_dependent_minimal.c b/tests/regression/66-interval-set-one/62-pfscan_widen_dependent_minimal.c
index 792be97752..7a14f7b3af 100644
--- a/tests/regression/66-interval-set-one/62-pfscan_widen_dependent_minimal.c
+++ b/tests/regression/66-interval-set-one/62-pfscan_widen_dependent_minimal.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/66-interval-set-one/98-widen-dependent-local.c b/tests/regression/66-interval-set-one/98-widen-dependent-local.c
index a5661256c0..44da5e682c 100644
--- a/tests/regression/66-interval-set-one/98-widen-dependent-local.c
+++ b/tests/regression/66-interval-set-one/98-widen-dependent-local.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init
+// PARAM: --enable ana.int.interval_set --enable exp.priv-distr-init --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/67-interval-sets-two/43-first-reads.c b/tests/regression/67-interval-sets-two/43-first-reads.c
index 852b76a509..87bfc614e6 100644
--- a/tests/regression/67-interval-sets-two/43-first-reads.c
+++ b/tests/regression/67-interval-sets-two/43-first-reads.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.int.interval_set true
+// PARAM: --set ana.int.interval_set true --enable ana.sv-comp.functions
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>
diff --git a/tests/regression/70-transform/01-ordering.t b/tests/regression/70-transform/01-ordering.t
index cd7ec8e36a..9ff5a9b739 100644
--- a/tests/regression/70-transform/01-ordering.t
+++ b/tests/regression/70-transform/01-ordering.t
@@ -1,3 +1,6 @@
+Suppress backtrace with code locations, especially for CI.
+  $ export OCAMLRUNPARAM=b=0
+
 Check that assert transform is not allowed to happen after dead code removal
   $ ./transform.sh --stderr remove_dead_code assert -- 01-empty.c
   [Error] trans.activated: the 'assert' transform may not occur after the 'remove_dead_code' transform
diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t
index a9f91bf4a6..6dcb21863e 100644
--- a/tests/regression/cfg/foo.t/run.t
+++ b/tests/regression/cfg/foo.t/run.t
@@ -1,48 +1,215 @@
   $ cfgDot foo.c
 
   $ graph-easy --as=boxart main.dot
-                                                ┌───────────────────────────────┐
-                                                │ main()                        │
-                                                └───────────────────────────────┘
-                                                  │
-                                                  │ (body)
-                                                  ▼
-                                                ┌───────────────────────────────┐
-                                                │ foo.c:2:7-2:12                │
-                                                │ (foo.c:2:7-2:12)              │
-                                                └───────────────────────────────┘
-                                                  │
-                                                  │ a = 1
-                                                  ▼
-                                                ┌───────────────────────────────┐
-                                                │ foo.c:2:14-2:19               │
-                                                │ (foo.c:2:14-2:19)             │
-                                                └───────────────────────────────┘
-                                                  │
-                                                  │ b = 1
-                                                  ▼
-             ┌──────────────────┐               ┌───────────────────────────────┐
-             │ foo.c:7:3-7:11   │  Neg(a > 0)   │ foo.c:3:3-6:3 (synthetic)     │
-    ┌──────▶ │ (unknown)        │ ◀──────────── │ (foo.c:3:10-3:20 (synthetic)) │ ◀┐
-    │        └──────────────────┘               └───────────────────────────────┘  │
-    │          │                                  │                                │
-    │          │ return 0                         │ Pos(a > 0)                     │
-    │          ▼                                  ▼                                │
-    │ Neg(b) ┌──────────────────┐               ┌───────────────────────────────┐  │
-    │        │ return of main() │               │ foo.c:3:3-6:3 (synthetic)     │  │
-    │        │                  │  ┌─────────── │ (foo.c:3:10-3:20 (synthetic)) │  │
-    │        └──────────────────┘  │            └───────────────────────────────┘  │
-    │                              │              │                                │
-    └──────────────────────────────┘              │ Pos(b)                         │ b = b - 1
-                                                  ▼                                │
-                                                ┌───────────────────────────────┐  │
-                                                │ foo.c:4:5-4:8                 │  │
-                                                │ (foo.c:4:5-4:8)               │  │
-                                                └───────────────────────────────┘  │
-                                                  │                                │
-                                                  │ a = a + 1                      │
-                                                  ▼                                │
-                                                ┌───────────────────────────────┐  │
-                                                │ foo.c:5:5-5:8                 │  │
-                                                │ (foo.c:5:5-5:8)               │ ─┘
-                                                └───────────────────────────────┘
+                                                           ┌───────────────────────────────┐
+                                                           │ main()                        │
+                                                           └───────────────────────────────┘
+                                                             │
+                                                             │ (body)
+                                                             ▼
+                                                           ┌───────────────────────────────┐
+                                                           │ foo.c:2:3-2:19                │
+                                                           │ (foo.c:2:7-2:12 (synthetic))  │
+                                                           │ YAML loc: foo.c:2:3-2:19      │
+                                                           │ GraphML: true; server: false  │
+                                                           └───────────────────────────────┘
+                                                             │
+                                                             │ a = 1
+                                                             ▼
+                                                           ┌───────────────────────────────┐
+                                                           │ foo.c:2:3-2:19 (synthetic)    │
+                                                           │ (foo.c:2:14-2:19 (synthetic)) │
+                                                           │ GraphML: true; server: false  │
+                                                           └───────────────────────────────┘
+                                                             │
+                                                             │ b = 1
+                                                             ▼
+             ┌─────────────────────────────┐               ┌───────────────────────────────┐
+             │ foo.c:7:3-7:11              │               │ foo.c:3:3-6:3 (synthetic)     │
+             │ (foo.c:7:10-7:11)           │               │ (foo.c:3:10-3:20 (synthetic)) │
+             │ YAML loc: foo.c:7:3-7:11    │               │ YAML loop: foo.c:3:3-6:3      │
+             │ GraphML: true; server: true │  Neg(a > 0)   │ GraphML: true; server: false  │
+    ┌──────▶ │                             │ ◀──────────── │ loop: foo.c:3:3-6:3           │ ◀┐
+    │        └─────────────────────────────┘               └───────────────────────────────┘  │
+    │          │                                             │                                │
+    │          │ return 0                                    │ Pos(a > 0)                     │
+    │          ▼                                             ▼                                │
+    │        ┌─────────────────────────────┐               ┌───────────────────────────────┐  │
+    │ Neg(b) │                             │               │ foo.c:3:3-6:3 (synthetic)     │  │
+    │        │ return of main()            │               │ (foo.c:3:10-3:20 (synthetic)) │  │
+    │        │                             │  ┌─────────── │ GraphML: true; server: false  │  │
+    │        └─────────────────────────────┘  │            └───────────────────────────────┘  │
+    │                                         │              │                                │
+    └─────────────────────────────────────────┘              │ Pos(b)                         │
+                                                             ▼                                │ b = b - 1
+                                                           ┌───────────────────────────────┐  │
+                                                           │ foo.c:4:5-4:8                 │  │
+                                                           │ (foo.c:4:5-4:8)               │  │
+                                                           │ YAML loc: foo.c:4:5-4:8       │  │
+                                                           │ GraphML: true; server: true   │  │
+                                                           └───────────────────────────────┘  │
+                                                             │                                │
+                                                             │ a = a + 1                      │
+                                                             ▼                                │
+                                                           ┌───────────────────────────────┐  │
+                                                           │ foo.c:5:5-5:8                 │  │
+                                                           │ (foo.c:5:5-5:8)               │  │
+                                                           │ YAML loc: foo.c:5:5-5:8       │  │
+                                                           │ GraphML: true; server: true   │ ─┘
+                                                           └───────────────────────────────┘
+
+  $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' --set sem.int.signed_overflow assume_none foo.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (foo.c:4:5-4:8)
+  [Warning][Integer > Overflow][CWE-191] Signed integer underflow (foo.c:5:5-5:8)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+  [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20)
+  [Info][Witness] witness generation summary:
+    total generation entries: 13
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: loop_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 3
+      column: 2
+      function: main
+    loop_invariant:
+      string: b <= 1
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 3
+      column: 2
+      function: main
+    loop_invariant:
+      string: 1 <= a
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 2
+      function: main
+    location_invariant:
+      string: b == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 2
+      function: main
+    location_invariant:
+      string: a != 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 7
+      column: 2
+      function: main
+    location_invariant:
+      string: 1 <= a
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 4
+      function: main
+    location_invariant:
+      string: b <= 1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 4
+      function: main
+    location_invariant:
+      string: b != 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 4
+      function: main
+    location_invariant:
+      string: a != 1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 4
+      function: main
+    location_invariant:
+      string: 2 <= a
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 4
+      column: 4
+      function: main
+    location_invariant:
+      string: b <= 1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 4
+      column: 4
+      function: main
+    location_invariant:
+      string: b != 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 4
+      column: 4
+      function: main
+    location_invariant:
+      string: a != 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: foo.c
+      file_hash: $FILE_HASH
+      line: 4
+      column: 4
+      function: main
+    location_invariant:
+      string: 1 <= a
+      type: assertion
+      format: C
diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t
index 78a81aff68..03dc2c1d0c 100644
--- a/tests/regression/cfg/issue-1356.t/run.t
+++ b/tests/regression/cfg/issue-1356.t/run.t
@@ -11,15 +11,18 @@
     │ Pos((long )a >= (long )b - 2147483648)                                │ (body)                                   │
     ▼                                                                       ▼                                          │
   ┌─────────────────────────────────────────┐                             ┌─────────────────────────────────────────┐  │
-  │ issue-1356.c:9:3-9:53 (synthetic)       │  Pos(b <= 0)                │ issue-1356.c:9:3-9:53                   │  │
-  │ (issue-1356.c:9:3-9:53 (synthetic))     │ ◀────────────────────────── │ (issue-1356.c:9:3-9:53)                 │  │
+  │ issue-1356.c:9:3-9:53 (synthetic)       │                             │ issue-1356.c:9:3-9:53                   │  │
+  │ (issue-1356.c:9:3-9:53 (synthetic))     │                             │ (issue-1356.c:9:3-9:53)                 │  │
+  │ GraphML: true; server: false            │  Pos(b <= 0)                │ YAML loc: issue-1356.c:9:3-9:53         │  │
+  │                                         │ ◀────────────────────────── │ GraphML: true; server: true             │  │
   └─────────────────────────────────────────┘                             └─────────────────────────────────────────┘  │
     │                                                                       │                                          │
     │                                                                       │ Neg(b <= 0)                              │
     │                                                                       ▼                                          │
     │                                                                     ┌─────────────────────────────────────────┐  │
     │                                                                     │ issue-1356.c:9:3-9:53 (synthetic)       │  │
-    │                                                                     │ (issue-1356.c:9:3-9:53 (synthetic))     │ ─┘
+    │                                                                     │ (issue-1356.c:9:3-9:53 (synthetic))     │  │
+    │                                                                     │ GraphML: true; server: false            │ ─┘
     │                                                                     └─────────────────────────────────────────┘
     │                                                                       │
     │                                                                       │ Neg((long )a >= (long )b - 2147483648)
@@ -27,48 +30,57 @@
     │                                                                     ┌─────────────────────────────────────────┐
     │                                                                     │ issue-1356.c:9:3-9:53 (synthetic)       │
     │                                                                     │ (issue-1356.c:9:3-9:53 (synthetic))     │
+    │                                                                     │ GraphML: true; server: false            │
     │                                                                     └─────────────────────────────────────────┘
     │                                                                       │
     │                                                                       │ tmp = 0
     │                                                                       ▼
     │                                                                     ┌─────────────────────────────────────────┐
-    │                                         tmp = 1                     │ issue-1356.c:9:3-9:53 (synthetic)       │
-    └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:9:3-9:53 (synthetic))     │
+    │                                                                     │ issue-1356.c:9:3-9:53 (synthetic)       │
+    │                                         tmp = 1                     │ (issue-1356.c:9:3-9:53 (synthetic))     │
+    └───────────────────────────────────────────────────────────────────▶ │ GraphML: true; server: false            │
                                                                           └─────────────────────────────────────────┘
                                                                             │
                                                                             │ assume_abort_if_not(tmp)
                                                                             ▼
                                                                           ┌─────────────────────────────────────────┐
                                                                           │ issue-1356.c:10:3-10:53                 │
-                                                                          │ (issue-1356.c:10:3-10:53)               │ ─┐
+                                                                          │ (issue-1356.c:10:3-10:53)               │
+                                                                          │ YAML loc: issue-1356.c:10:3-10:53       │
+                                                                          │ GraphML: true; server: true             │ ─┐
                                                                           └─────────────────────────────────────────┘  │
                                                                             │                                          │
                                                                             │ Neg(b >= 0)                              │
                                                                             ▼                                          │
   ┌─────────────────────────────────────────┐                             ┌─────────────────────────────────────────┐  │
-  │ issue-1356.c:10:3-10:53 (synthetic)     │  Neg(a <= b + 2147483647)   │ issue-1356.c:10:3-10:53 (synthetic)     │  │
-  │ (issue-1356.c:10:3-10:53 (synthetic))   │ ◀────────────────────────── │ (issue-1356.c:10:3-10:53 (synthetic))   │  │ Pos(b >= 0)
+  │ issue-1356.c:10:3-10:53 (synthetic)     │                             │ issue-1356.c:10:3-10:53 (synthetic)     │  │
+  │ (issue-1356.c:10:3-10:53 (synthetic))   │  Neg(a <= b + 2147483647)   │ (issue-1356.c:10:3-10:53 (synthetic))   │  │ Pos(b >= 0)
+  │ GraphML: true; server: false            │ ◀────────────────────────── │ GraphML: true; server: false            │  │
   └─────────────────────────────────────────┘                             └─────────────────────────────────────────┘  │
     │                                                                       │                                          │
     │                                                                       │ Pos(a <= b + 2147483647)                 │
     │                                                                       ▼                                          │
     │                                                                     ┌─────────────────────────────────────────┐  │
     │                                                                     │ issue-1356.c:10:3-10:53 (synthetic)     │  │
-    │                                                                     │ (issue-1356.c:10:3-10:53 (synthetic))   │ ◀┘
+    │                                                                     │ (issue-1356.c:10:3-10:53 (synthetic))   │  │
+    │                                                                     │ GraphML: true; server: false            │ ◀┘
     │                                                                     └─────────────────────────────────────────┘
     │                                                                       │
     │                                                                       │ tmp___0 = 1
     │                                                                       ▼
     │                                                                     ┌─────────────────────────────────────────┐
-    │                                         tmp___0 = 0                 │ issue-1356.c:10:3-10:53 (synthetic)     │
-    └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:10:3-10:53 (synthetic))   │
+    │                                                                     │ issue-1356.c:10:3-10:53 (synthetic)     │
+    │                                         tmp___0 = 0                 │ (issue-1356.c:10:3-10:53 (synthetic))   │
+    └───────────────────────────────────────────────────────────────────▶ │ GraphML: true; server: false            │
                                                                           └─────────────────────────────────────────┘
                                                                             │
                                                                             │ assume_abort_if_not(tmp___0)
                                                                             ▼
                                                                           ┌─────────────────────────────────────────┐
                                                                           │ issue-1356.c:11:3-11:15                 │
-                                                                          │ (unknown)                               │
+                                                                          │ (issue-1356.c:11:10-11:15)              │
+                                                                          │ YAML loc: issue-1356.c:11:3-11:15       │
+                                                                          │ GraphML: true; server: true             │
                                                                           └─────────────────────────────────────────┘
                                                                             │
                                                                             │ return a - b
@@ -76,3 +88,18 @@
                                                                           ┌─────────────────────────────────────────┐
                                                                           │ return of minus()                       │
                                                                           └─────────────────────────────────────────┘
+
+
+
+  $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (issue-1356.c:10:3-10:53)
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:10-11:15)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 13
+    dead: 0
+    total lines: 13
+  [Info][Witness] witness generation summary:
+    total generation entries: 0
+
+  $ yamlWitnessStrip < witness.yml
+  []
diff --git a/tests/regression/cfg/loops.t/loops.c b/tests/regression/cfg/loops.t/loops.c
new file mode 100644
index 0000000000..cac7837bcc
--- /dev/null
+++ b/tests/regression/cfg/loops.t/loops.c
@@ -0,0 +1,50 @@
+#include <goblint.h>
+
+int main() {
+  int i;
+
+  // while loop
+  i = 0;
+  while (i < 10) {
+    i++;
+  }
+
+  // for loop
+  for (i = 0; i < 10; i++) {
+    __goblint_check(1);
+  }
+
+  // for loop with empty body
+  for (i = 0; i < 10; i++) {
+
+  }
+
+  // for loop with empty increment
+  for (i = 0; i < 10;) {
+    i++;
+  }
+
+  // for loop with empty initializer
+  i = 0;
+  for (; i < 10; i++) {
+    __goblint_check(1);
+  }
+
+  // for loop with declaration initializer
+  for (int j = 0; j < 10; j++) {
+    __goblint_check(1);
+  }
+
+  // for loop with two initializers
+  for (int k = (i = 0); i < 10; i++) {
+    __goblint_check(1);
+  }
+
+  // do-while loop
+  i = 0;
+  do {
+    i++;
+  } while (i < 10);
+
+  return 0;
+}
diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t
new file mode 100644
index 0000000000..01216a624e
--- /dev/null
+++ b/tests/regression/cfg/loops.t/run.t
@@ -0,0 +1,807 @@
+  $ cfgDot loops.c
+
+  $ graph-easy --as=boxart main.dot
+  
+                                                        ┌──────────────────────────────────────────────────────────────────────────────┐
+                                                        │                                                                              │
+                                                        │                                                                              │
+    ┌───────────────────────────────────────────────────┼─────────────────────────────────────────────────────────────────────────┐    │
+    │                                                   │                                                                         │    │
+    │                                                   │                                                                         │    │
+    │    ┌──────────────────────────────────────────────┼────────────────────────────────────────────────────────────────────┐    │    │
+    │    │                                              │                                                                    │    │    │
+    │    │                                              │                                                                    │    │    │
+    │    │    ┌─────────────────────────────────────────┼────────────────────────────────────────────────────┐               │    │    │
+    │    │    │                                         │                                                    │               │    │    │
+    │    │    │                                         │             ┌───────────────────────────────────┐  │               │    │    │
+    │    │    │    ┌────────────────────────────────────┘             │ main()                            │  │               │    │    │
+    │    │    │    │                                                  └───────────────────────────────────┘  │               │    │    │
+    │    │    │    │                                                    │                                    │               │    │    │ i = i + 1
+    │    │    │    │                                                    │ (body)                             │               │    │    │
+    │    │    │    │                                                    ▼                                    │               │    │    │
+    │    │    │    │                                                  ┌───────────────────────────────────┐  │               │    │    │
+    │    │    │    │                                                  │ loops.c:7:3-7:8                   │  │               │    │    │
+    │    │    │    │                                                  │ (loops.c:7:3-7:8)                 │  │               │    │    │
+    │    │    │    │                                                  │ YAML loc: loops.c:7:3-7:8         │  │               │    │    │
+    │    │    │    │                                                  │ GraphML: true; server: true       │  │               │    │    │
+    │    │    │    │                                                  └───────────────────────────────────┘  │               │    │    │
+    │    │    │    │                                                    │                                    │               │    │    │
+    │    │    │    │                                                    │ i = 0                              │               │    │    │
+    │    │    │    │                                                    ▼                                    │               │    │    │
+    │    │    │  ┌───────────────────────────────────┐                ┌───────────────────────────────────┐  │               │    │    │
+    │    │    │  │ loops.c:9:5-9:8                   │                │ loops.c:8:3-10:3 (synthetic)      │  │               │    │    │
+    │    │    │  │ (loops.c:9:5-9:8)                 │                │ (loops.c:8:10-8:16 (synthetic))   │  │               │    │    │
+    │    │    │  │ YAML loc: loops.c:9:5-9:8         │                │ YAML loop: loops.c:8:3-10:3       │  │               │    │    │
+    │    │    │  │ GraphML: true; server: true       │  Pos(i < 10)   │ GraphML: true; server: false      │  │               │    │    │
+    │    │    │  │                                   │ ◀───────────── │ loop: loops.c:8:3-10:3            │ ◀┼───────────────┼────┼────┘
+    │    │    │  └───────────────────────────────────┘                └───────────────────────────────────┘  │               │    │
+    │    │    │                                                         │                                    │               │    │
+    │    │    │                                                         │ Neg(i < 10)                        │               │    │
+    │    │    │                                                         ▼                                    │               │    │
+    │    │    │                                                       ┌───────────────────────────────────┐  │               │    │
+    │    │    │                                                       │ loops.c:13:3-15:3                 │  │               │    │
+    │    │    │                                                       │ (loops.c:13:7-13:26 (synthetic))  │  │               │    │
+    │    │    │                                                       │ YAML loc: loops.c:13:3-15:3       │  │ i = i + 1     │    │
+    │    │    │                                                       │ GraphML: true; server: false      │  │               │    │
+    │    │    │                                                       └───────────────────────────────────┘  │               │    │
+    │    │    │                                                         │                                    │               │    │
+    │    │    │                                                         │ i = 0                              │               │    │
+    │    │    │                                                         ▼                                    │               │    │
+    │    │    │  ┌───────────────────────────────────┐                ┌───────────────────────────────────┐  │               │    │
+    │    │    │  │ loops.c:14:5-14:23                │                │ loops.c:13:3-15:3 (synthetic)     │  │               │    │
+    │    │    │  │ (loops.c:14:5-14:23)              │                │ (loops.c:13:7-13:26 (synthetic))  │  │               │    │
+    │    │    │  │ YAML loc: loops.c:14:5-14:23      │                │ YAML loop: loops.c:13:3-15:3      │  │               │    │
+    │    │    │  │ GraphML: true; server: true       │  Pos(i < 10)   │ GraphML: true; server: false      │  │               │    │
+    │    │    │  │                                   │ ◀───────────── │ loop: loops.c:13:3-15:3           │ ◀┘               │    │
+    │    │    │  └───────────────────────────────────┘                └───────────────────────────────────┘                  │    │
+    │    │    │    │                                                    │                                                    │    │
+    │    │    │    │ __goblint_check(1)                                 │ Neg(i < 10)                                        │    │
+    │    │    │    ▼                                                    ▼                                                    │    │
+    │    │    │  ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                  │    │
+    │    │    │  │ loops.c:13:3-15:3 (synthetic)     │                │ loops.c:18:3-20:3                 │                  │    │
+    │    │    │  │ (loops.c:13:7-13:26 (synthetic))  │                │ (loops.c:18:7-18:26 (synthetic))  │                  │    │
+    │    │    │  │ GraphML: true; server: false      │                │ YAML loc: loops.c:18:3-20:3       │                  │    │
+    │    │    └─ │                                   │                │ GraphML: true; server: false      │                  │    │
+    │    │       └───────────────────────────────────┘                └───────────────────────────────────┘                  │    │
+    │    │                                                              │                                                    │    │
+    │    │                                                              │ i = 0                                              │    │
+    │    │                                                              ▼                                                    │    │
+    │    │       ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                  │    │
+    │    │       │                                   │                │ loops.c:18:3-20:3 (synthetic)     │                  │    │
+    │    │       │ loops.c:18:3-20:3 (synthetic)     │                │ (loops.c:18:7-18:26 (synthetic))  │                  │    │
+    │    │       │ (loops.c:18:7-18:26 (synthetic))  │                │ YAML loop: loops.c:18:3-20:3      │                  │    │
+    │    │       │ GraphML: true; server: false      │  Pos(i < 10)   │ GraphML: true; server: false      │  i = i + 1       │    │
+    │    └────── │                                   │ ◀───────────── │ loop: loops.c:18:3-20:3           │ ◀────────────────┘    │
+    │            └───────────────────────────────────┘                └───────────────────────────────────┘                       │
+    │                                                                   │                                                         │
+    │                                                                   │ Neg(i < 10)                                             │
+    │                                                                   ▼                                                         │
+    │                                                                 ┌───────────────────────────────────┐                       │
+    │                                                                 │ loops.c:23:3-25:3                 │                       │
+    │                                                                 │ (loops.c:23:7-23:22 (synthetic))  │                       │
+    │                                                                 │ YAML loc: loops.c:23:3-25:3       │                       │
+    │                                                                 │ GraphML: true; server: false      │                       │
+    │                                                                 └───────────────────────────────────┘                       │
+    │                                                                   │                                                         │
+    │                                                                   │ i = 0                                                   │
+    │                                                                   ▼                                                         │
+    │            ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                       │
+    │            │ loops.c:24:5-24:8                 │                │ loops.c:23:3-25:3 (synthetic)     │                       │
+    │            │ (loops.c:24:5-24:8)               │                │ (loops.c:23:7-23:22 (synthetic))  │                       │
+    │            │ YAML loc: loops.c:24:5-24:8       │                │ YAML loop: loops.c:23:3-25:3      │                       │
+    │            │ GraphML: true; server: true       │  Pos(i < 10)   │ GraphML: true; server: false      │  i = i + 1            │
+    └─────────── │                                   │ ◀───────────── │ loop: loops.c:23:3-25:3           │ ◀─────────────────────┘
+                 └───────────────────────────────────┘                └───────────────────────────────────┘
+                                                                        │
+                                                                        │ Neg(i < 10)
+                                                                        ▼
+                                                                      ┌───────────────────────────────────┐
+                                                                      │ loops.c:28:3-28:8                 │
+                                                                      │ (loops.c:28:3-28:8)               │
+                                                                      │ YAML loc: loops.c:28:3-28:8       │
+                                                                      │ GraphML: true; server: true       │
+                                                                      └───────────────────────────────────┘
+                                                                        │
+                                                                        │ i = 0
+                                                                        ▼
+                 ┌───────────────────────────────────┐                ┌───────────────────────────────────┐
+                 │ loops.c:30:5-30:23                │                │ loops.c:29:3-31:3 (synthetic)     │
+                 │ (loops.c:30:5-30:23)              │                │ (loops.c:29:7-29:21 (synthetic))  │
+                 │ YAML loc: loops.c:30:5-30:23      │                │ YAML loop: loops.c:29:3-31:3      │
+                 │ GraphML: true; server: true       │  Pos(i < 10)   │ GraphML: true; server: false      │  i = i + 1
+                 │                                   │ ◀───────────── │ loop: loops.c:29:3-31:3           │ ◀─────────────────────┐
+                 └───────────────────────────────────┘                └───────────────────────────────────┘                       │
+                   │                                                    │                                                         │
+                   │ __goblint_check(1)                                 │ Neg(i < 10)                                             │
+                   ▼                                                    ▼                                                         │
+                 ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                       │
+                 │ loops.c:29:3-31:3 (synthetic)     │                │ loops.c:34:3-36:3                 │                       │
+                 │ (loops.c:29:7-29:21 (synthetic))  │                │ (loops.c:34:12-34:17 (synthetic)) │                       │
+                 │ GraphML: true; server: false      │                │ YAML loc: loops.c:34:3-36:3       │                       │
+         ┌────── │                                   │                │ GraphML: true; server: false      │                       │
+         │       └───────────────────────────────────┘                └───────────────────────────────────┘                       │
+         │                                                              │                                                         │
+         │                                                              │ j = 0                                                   │
+         │                                                              ▼                                                         │
+         │       ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                       │
+         │       │ loops.c:35:5-35:23                │                │ loops.c:34:3-36:3 (synthetic)     │                       │
+         │       │ (loops.c:35:5-35:23)              │                │ (loops.c:34:7-34:30 (synthetic))  │                       │
+         │       │ YAML loc: loops.c:35:5-35:23      │                │ YAML loop: loops.c:34:3-36:3      │                       │
+         │       │ GraphML: true; server: true       │  Pos(j < 10)   │ GraphML: true; server: false      │  j = j + 1            │
+         │       │                                   │ ◀───────────── │ loop: loops.c:34:3-36:3           │ ◀─────────────────────┼────┐
+         │       └───────────────────────────────────┘                └───────────────────────────────────┘                       │    │
+         │         │                                                    │                                                         │    │
+         │         │ __goblint_check(1)                                 │ Neg(j < 10)                                             │    │
+         │         ▼                                                    ▼                                                         │    │
+         │       ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                       │    │
+         │       │ loops.c:34:3-36:3 (synthetic)     │                │ loops.c:39:3-41:3                 │                       │    │
+         │       │ (loops.c:34:12-34:17 (synthetic)) │                │ (loops.c:39:12-39:23 (synthetic)) │                       │    │
+         │       │ GraphML: true; server: false      │                │ YAML loc: loops.c:39:3-41:3       │                       │    │
+         │       │                                   │                │ GraphML: true; server: false      │                       │    │
+         │       └───────────────────────────────────┘                └───────────────────────────────────┘                       │    │
+         │         │                                                    │                                                         │    │
+         │         │                                                    │ i = 0                                                   │    │
+         │         │                                                    ▼                                                         │    │
+         │         │                                                  ┌───────────────────────────────────┐                       │    │
+         │         │                                                  │ loops.c:39:3-41:3 (synthetic)     │                       │    │
+         │         │                                                  │ (loops.c:39:12-39:23 (synthetic)) │                       │    │
+         │         │                                                  │ GraphML: true; server: false      │                       │    │
+         │         │                                                  └───────────────────────────────────┘                       │    │
+         │         │                                                    │                                                         │    │
+         │    ┌────┘                                                    │ k = i                                                   │    │
+         │    │                                                         ▼                                                         │    │
+         │    │  ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                       │    │
+         │    │  │ loops.c:40:5-40:23                │                │ loops.c:39:3-41:3 (synthetic)     │                       │    │
+         │    │  │ (loops.c:40:5-40:23)              │                │ (loops.c:39:7-39:36 (synthetic))  │                       │    │
+         │    │  │ YAML loc: loops.c:40:5-40:23      │                │ YAML loop: loops.c:39:3-41:3      │                       │    │
+         │    │  │ GraphML: true; server: true       │  Pos(i < 10)   │ GraphML: true; server: false      │  i = i + 1            │    │
+         │    │  │                                   │ ◀───────────── │ loop: loops.c:39:3-41:3           │ ◀─────────────────────┼────┼─────────────┐
+         │    │  └───────────────────────────────────┘                └───────────────────────────────────┘                       │    │             │
+         │    │    │                                                    │                                                         │    │             │
+         │    │    │ __goblint_check(1)                                 │ Neg(i < 10)                                             │    │             │
+         │    │    ▼                                                    ▼                                                         │    │             │
+         │    │  ┌───────────────────────────────────┐                ┌───────────────────────────────────┐                       │    │             │
+         │    │  │ loops.c:39:3-41:3 (synthetic)     │                │ loops.c:44:3-44:8                 │                       │    │             │
+         │    │  │ (loops.c:39:12-39:23 (synthetic)) │                │ (loops.c:44:3-44:8)               │                       │    │             │
+         │    │  │ GraphML: true; server: false      │                │ YAML loc: loops.c:44:3-44:8       │                       │    │             │
+         │    │  │                                   │                │ GraphML: true; server: true       │                       │    │             │
+         │    │  └───────────────────────────────────┘                └───────────────────────────────────┘                       │    │             │
+         │    │    │                                                    │                                                         │    │             │
+         │    │    │                                                    │ i = 0                                                   │    │             │
+         │    │    │                                                    ▼                                                         │    │             │
+         │    │    │                                                  ┌───────────────────────────────────┐                       │    │             │
+         │    │    │                                                  │ loops.c:46:5-46:8                 │                       │    │             │
+         │    │    │                                                  │ (loops.c:46:5-46:8)               │                       │    │             │
+         │    │    │                                                  │ YAML loc: loops.c:46:5-46:8       │                       │    │             │
+         │    │    │                                                  │ YAML loop: loops.c:45:3-47:19     │                       │    │             │
+         │    │    │                                                  │ GraphML: true; server: true       │                       │    │             │
+         │    │    │                                                  │ loop: loops.c:45:3-47:19          │ ◀┐                    │    │             │
+         │    │    │                                                  └───────────────────────────────────┘  │                    │    │             │
+         │    │    │                                                    │                                    │                    │    │             │
+         │    │    │                                                    │ i = i + 1                          │ Pos(i < 10)        │    │             │
+         │    │    │                                                    ▼                                    │                    │    │             │
+         │    │    │                                                  ┌───────────────────────────────────┐  │                    │    │             │
+         │    │    │                                                  │ loops.c:45:3-47:19 (synthetic)    │  │                    │    │             │
+         │    │    │                                                  │ (loops.c:47:12-47:19 (synthetic)) │  │                    │    │             │
+         │    │    │                                                  │ GraphML: true; server: false      │ ─┘                    │    │             │
+         │    │    │                                                  └───────────────────────────────────┘                       │    │             │
+         │    │    │                                                    │                                                         │    │             │
+         │    │    │                                                    │ Neg(i < 10)                                             │    │             │
+         │    │    │                                                    ▼                                                         │    │             │
+         │    │    │                                                  ┌───────────────────────────────────┐                       │    │             │
+         │    │    │                                                  │ loops.c:49:3-49:11                │                       │    │             │
+         │    │    │                                                  │ (loops.c:49:10-49:11)             │                       │    │             │
+         │    │    │                                                  │ YAML loc: loops.c:49:3-49:11      │                       │    │             │
+         │    │    │                                                  │ GraphML: true; server: true       │                       │    │             │
+         │    │    │                                                  └───────────────────────────────────┘                       │    │             │
+         │    │    │                                                    │                                                         │    │             │
+         │    └────┼────────────────────────────────────┐               │ return 0                                                │    │             │
+         │         │                                    │               ▼                                                         │    │             │
+         │         │                                    │             ┌───────────────────────────────────┐                       │    │             │
+         │         │                                    │             │ return of main()                  │                       │    │             │
+         │         │                                    │             └───────────────────────────────────┘                       │    │             │
+         │         │                                    │                                                                         │    │             │
+         └─────────┼────────────────────────────────────┼─────────────────────────────────────────────────────────────────────────┘    │             │
+                   │                                    │                                                                              │             │
+                   │                                    │                                                                              │             │
+                   │                                    └──────────────────────────────────────────────────────────────────────────────┘             │
+                   │                                                                                                                                 │
+                   │                                                                                                                                 │
+                   └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+
+  $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' loops.c
+  [Success][Assert] Assertion "1" will succeed (loops.c:14:5-14:23)
+  [Success][Assert] Assertion "1" will succeed (loops.c:30:5-30:23)
+  [Success][Assert] Assertion "1" will succeed (loops.c:35:5-35:23)
+  [Success][Assert] Assertion "1" will succeed (loops.c:40:5-40:23)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 20
+    dead: 0
+    total lines: 20
+  [Info][Witness] witness generation summary:
+    total generation entries: 53
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 45
+      column: 2
+      function: main
+    loop_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 45
+      column: 2
+      function: main
+    loop_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 45
+      column: 2
+      function: main
+    loop_invariant:
+      string: i <= 9
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 45
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 39
+      column: 2
+      function: main
+    loop_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 39
+      column: 2
+      function: main
+    loop_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 39
+      column: 2
+      function: main
+    loop_invariant:
+      string: i <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 39
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 34
+      column: 2
+      function: main
+    loop_invariant:
+      string: j <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 34
+      column: 2
+      function: main
+    loop_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 34
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= j
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 29
+      column: 2
+      function: main
+    loop_invariant:
+      string: i <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 29
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 23
+      column: 2
+      function: main
+    loop_invariant:
+      string: i <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 23
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 18
+      column: 2
+      function: main
+    loop_invariant:
+      string: i <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 18
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    loop_invariant:
+      string: i <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 8
+      column: 2
+      function: main
+    loop_invariant:
+      string: i <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 8
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 49
+      column: 2
+      function: main
+    location_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 49
+      column: 2
+      function: main
+    location_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 49
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 46
+      column: 4
+      function: main
+    location_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 46
+      column: 4
+      function: main
+    location_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 46
+      column: 4
+      function: main
+    location_invariant:
+      string: i <= 9
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 46
+      column: 4
+      function: main
+    location_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 44
+      column: 2
+      function: main
+    location_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 44
+      column: 2
+      function: main
+    location_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 44
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 40
+      column: 4
+      function: main
+    location_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 40
+      column: 4
+      function: main
+    location_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 40
+      column: 4
+      function: main
+    location_invariant:
+      string: i <= 9
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 40
+      column: 4
+      function: main
+    location_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 39
+      column: 2
+      function: main
+    location_invariant:
+      string: j == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 39
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 35
+      column: 4
+      function: main
+    location_invariant:
+      string: j <= 9
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 35
+      column: 4
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 35
+      column: 4
+      function: main
+    location_invariant:
+      string: 0 <= j
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 34
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 30
+      column: 4
+      function: main
+    location_invariant:
+      string: i <= 9
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 30
+      column: 4
+      function: main
+    location_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 28
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 24
+      column: 4
+      function: main
+    location_invariant:
+      string: i <= 9
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 24
+      column: 4
+      function: main
+    location_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 23
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 18
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 4
+      function: main
+    location_invariant:
+      string: i <= 9
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 4
+      function: main
+    location_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 4
+      function: main
+    location_invariant:
+      string: i <= 9
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: loops.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 4
+      function: main
+    location_invariant:
+      string: 0 <= i
+      type: assertion
+      format: C
diff --git a/tests/regression/cfg/pr-758.t/pr-758.c b/tests/regression/cfg/pr-758.t/pr-758.c
index 87aa41889d..11db4589a2 100644
--- a/tests/regression/cfg/pr-758.t/pr-758.c
+++ b/tests/regression/cfg/pr-758.t/pr-758.c
@@ -3,7 +3,7 @@
 int main() {
   // for loop
   int x = 42;
-  for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line
+  for (x = 0; x < 10; x++) { // there shouldn't be location invariants x <= 9, x <= 10 and 0 <= x before this line
     // ...
   }
 
diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t
index d87d9128c7..04a68be3b6 100644
--- a/tests/regression/cfg/pr-758.t/run.t
+++ b/tests/regression/cfg/pr-758.t/run.t
@@ -11,22 +11,29 @@
     │                                                  │ (body)                              │
     │                                                  ▼                                     │
     │                                                ┌────────────────────────────────────┐  │
-    │                                                │ pr-758.c:5:7-5:13                  │  │
-    │                                                │ (pr-758.c:5:7-5:13)                │  │
+    │                                                │ pr-758.c:5:3-5:13                  │  │
+    │                                                │ (pr-758.c:5:7-5:13 (synthetic))    │  │
+    │                                                │ YAML loc: pr-758.c:5:3-5:13        │  │
+    │                                                │ GraphML: true; server: false       │  │
     │                                                └────────────────────────────────────┘  │
     │                                                  │                                     │ x = x + 1
     │                                                  │ x = 42                              │
     │                                                  ▼                                     │
     │                                                ┌────────────────────────────────────┐  │
-    │                                                │ pr-758.c:6:3-8:3 (synthetic)       │  │
+    │                                                │ pr-758.c:6:3-8:3                   │  │
     │                                                │ (pr-758.c:6:7-6:26 (synthetic))    │  │
+    │                                                │ YAML loc: pr-758.c:6:3-8:3         │  │
+    │                                                │ GraphML: true; server: false       │  │
     │                                                └────────────────────────────────────┘  │
     │                                                  │                                     │
     │                                                  │ x = 0                               │
     │                                                  ▼                                     │
   ┌─────────────────────────────────┐                ┌────────────────────────────────────┐  │
-  │ pr-758.c:6:3-8:3 (synthetic)    │  Pos(x < 10)   │ pr-758.c:6:3-8:3 (synthetic)       │  │
-  │ (pr-758.c:6:7-6:26 (synthetic)) │ ◀───────────── │ (pr-758.c:6:7-6:26 (synthetic))    │ ◀┘
+  │                                 │                │ pr-758.c:6:3-8:3 (synthetic)       │  │
+  │ pr-758.c:6:3-8:3 (synthetic)    │                │ (pr-758.c:6:7-6:26 (synthetic))    │  │
+  │ (pr-758.c:6:7-6:26 (synthetic)) │                │ YAML loop: pr-758.c:6:3-8:3        │  │
+  │ GraphML: true; server: false    │  Pos(x < 10)   │ GraphML: true; server: false       │  │
+  │                                 │ ◀───────────── │ loop: pr-758.c:6:3-8:3             │ ◀┘
   └─────────────────────────────────┘                └────────────────────────────────────┘
                                                        │
                                                        │ Neg(x < 10)
@@ -34,6 +41,8 @@
                                                      ┌────────────────────────────────────┐
                                                      │ pr-758.c:12:3-12:12                │
                                                      │ (pr-758.c:12:3-12:12)              │
+                                                     │ YAML loc: pr-758.c:12:3-12:12      │
+                                                     │ GraphML: true; server: true        │
                                                      └────────────────────────────────────┘
                                                        │
                                                        │ k = 0
@@ -41,27 +50,33 @@
                                                      ┌────────────────────────────────────┐
                                                      │ pr-758.c:12:3-12:12 (synthetic)    │
                                                      │ (pr-758.c:12:3-12:12 (synthetic))  │
+                                                     │ GraphML: true; server: false       │
                                                      └────────────────────────────────────┘
                                                        │
                                                        │ i = k
                                                        ▼
                                                      ┌────────────────────────────────────┐
-                                                     │ pr-758.c:20:15-20:24               │
-                                                     │ (pr-758.c:20:15-20:24)             │
+                                                     │ pr-758.c:20:3-20:25                │
+                                                     │ (pr-758.c:20:15-20:24 (synthetic)) │
+                                                     │ YAML loc: pr-758.c:20:3-20:25      │
+                                                     │ GraphML: true; server: false       │
                                                      └────────────────────────────────────┘
                                                        │
                                                        │ a.kaal = 2
                                                        ▼
                                                      ┌────────────────────────────────────┐
-                                                     │ pr-758.c:20:15-20:24 (synthetic)   │
+                                                     │ pr-758.c:20:3-20:25 (synthetic)    │
                                                      │ (pr-758.c:20:15-20:24 (synthetic)) │
+                                                     │ GraphML: true; server: false       │
                                                      └────────────────────────────────────┘
                                                        │
                                                        │ a.hind = 3
                                                        ▼
                                                      ┌────────────────────────────────────┐
                                                      │ pr-758.c:21:3-21:11                │
-                                                     │ (unknown)                          │
+                                                     │ (pr-758.c:21:10-21:11)             │
+                                                     │ YAML loc: pr-758.c:21:3-21:11      │
+                                                     │ GraphML: true; server: true        │
                                                      └────────────────────────────────────┘
                                                        │
                                                        │ return 0
@@ -69,3 +84,147 @@
                                                      ┌────────────────────────────────────┐
                                                      │ return of main()                   │
                                                      └────────────────────────────────────┘
+
+
+
+  $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["loop_invariant", "location_invariant"]' pr-758.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+  [Info][Witness] witness generation summary:
+    total generation entries: 12
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: loop_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 6
+      column: 2
+      function: main
+    loop_invariant:
+      string: x <= 10
+      type: assertion
+      format: C
+  - entry_type: loop_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 6
+      column: 2
+      function: main
+    loop_invariant:
+      string: 0 <= x
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 21
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 21
+      column: 2
+      function: main
+    location_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 21
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 21
+      column: 2
+      function: main
+    location_invariant:
+      string: a.kaal == 2
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 21
+      column: 2
+      function: main
+    location_invariant:
+      string: a.hind == 3
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 20
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 20
+      column: 2
+      function: main
+    location_invariant:
+      string: k == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 20
+      column: 2
+      function: main
+    location_invariant:
+      string: i == 0
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 10
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: pr-758.c
+      file_hash: $FILE_HASH
+      line: 6
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml
index 7eb7cb27c1..a58029086a 100644
--- a/tests/regression/cfg/util/cfgDot.ml
+++ b/tests/regression/cfg/util/cfgDot.ml
@@ -17,10 +17,14 @@ let main () =
   Cilfacade.init ();
   GobConfig.set_bool "dbg.cfg.loop-unrolling" true;
   GobConfig.set_int "exp.unrolling-factor" !unroll;
+  GobConfig.set_bool "witness.invariant.loop-head" true;
+  GobConfig.set_bool "witness.invariant.after-lock" true;
+  GobConfig.set_bool "witness.invariant.other" true;
 
   assert (List.length !files = 1);
   let ast = Cilfacade.getAST (Fpath.v (List.hd !files)) in
   CilCfg0.end_basic_blocks ast;
+  Cilfacade.current_file := ast;
   (* Part of CilCfg.createCFG *)
   GoblintCil.iterGlobals ast (function
       | GFun (fd, _) ->
@@ -31,6 +35,15 @@ let main () =
       | _ -> ()
     );
   let (module Cfg) = CfgTools.compute_cfg ast in
+  let module FileCfg =
+  struct
+    let file = ast
+    module Cfg = Cfg
+  end
+  in
+
+  let module GraphmlWitnessInvariant = WitnessUtil.Invariant (FileCfg) in
+  let module YamlWitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in
 
   let module LocationExtraNodeStyles =
   struct
@@ -49,12 +62,29 @@ let main () =
 
     let pp_label_locs ppf label =
       let locs = CilLocation.get_labelLoc label in
-      Format.fprintf ppf "[%a]" pp_locs locs
+      Format.fprintf ppf "@;[%a]" pp_locs locs
+
+    let pp_yaml_loc ppf loc =
+      Format.fprintf ppf "@;YAML loc: %a" CilType.Location.pp loc
+
+    let pp_yaml_loop ppf loc =
+      Format.fprintf ppf "@;YAML loop: %a" CilType.Location.pp loc
+
+    let pp_loop_loc ppf loop =
+      Format.fprintf ppf "@;loop: %a" CilType.Location.pp loop
 
     let extraNodeStyles = function
-      | Node.Statement stmt ->
+      | Node.Statement stmt as n ->
         let locs: CilLocation.locs = CilLocation.get_stmtLoc stmt in
-        let label = Format.asprintf "@[<v 2>%a@;%a@]" pp_locs locs (Format.pp_print_list ~pp_sep:Format.pp_print_cut pp_label_locs) stmt.labels in
+        let label =
+          Format.asprintf "@[<v 2>%a%a%a%a@;GraphML: %B; server: %B%a@]"
+            pp_locs locs
+            (Format.pp_print_list ~pp_sep:GobFormat.pp_print_nothing pp_label_locs) stmt.labels
+            (Format.pp_print_option pp_yaml_loc) (YamlWitnessInvariant.location_location n)
+            (Format.pp_print_option pp_yaml_loop) (YamlWitnessInvariant.loop_location n)
+            (GraphmlWitnessInvariant.is_invariant_node n) (Server.is_server_node n)
+            (Format.pp_print_option pp_loop_loc) (GraphmlWitnessInvariant.find_syntactic_loop_head n)
+        in
         [Printf.sprintf "label=\"%s\"" (Str.global_replace (Str.regexp "\n") "\\n" label)]
       | _ -> []
   end
diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune
index fe03f7a3ec..fb3c5e6899 100644
--- a/tests/regression/cfg/util/dune
+++ b/tests/regression/cfg/util/dune
@@ -4,7 +4,7 @@
    goblint-cil
    goblint_logs
    goblint_common
-   goblint_lib ; TODO: avoid: extract LoopUnrolling from goblint_lib
+   goblint_lib ; TODO: avoid: extract LoopUnrolling and WitnessUtil node predicates from goblint_lib
    fpath
    goblint.sites.dune
    goblint.build-info.dune)
diff --git a/tests/regression/dune b/tests/regression/dune
index 29a0dc0c20..7ff91483c6 100644
--- a/tests/regression/dune
+++ b/tests/regression/dune
@@ -1,6 +1,8 @@
 (env
  (_
-  (binaries ./cfg/util/cfgDot.exe)))
+  (binaries
+    ./cfg/util/cfgDot.exe
+    ../util/yamlWitnessStrip.exe)))
 
 (rule
  (alias runtest)
@@ -20,4 +22,6 @@
 (cram
  (applies_to :whole_subtree)
  (alias runcramtest)
- (deps (package goblint)))
+ (deps
+   (package goblint)
+   %{bin:yamlWitnessStrip}))
diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t
new file mode 100644
index 0000000000..b06164743b
--- /dev/null
+++ b/tests/regression/witness/typedef.t/run.t
@@ -0,0 +1,316 @@
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.typedefs typedef.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+  [Info][Witness] witness generation summary:
+    total generation entries: 13
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: q == (void *)(& a)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((int *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((int *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((int *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable witness.invariant.typedefs typedef.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+  [Info][Witness] witness generation summary:
+    total generation entries: 14
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: q == (void *)(& a)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: ((s *)q)->f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
diff --git a/tests/regression/witness/typedef.t/typedef.c b/tests/regression/witness/typedef.t/typedef.c
new file mode 100644
index 0000000000..1e60ad084d
--- /dev/null
+++ b/tests/regression/witness/typedef.t/typedef.c
@@ -0,0 +1,15 @@
+typedef int myint;
+
+typedef struct {
+  int f;
+} s;
+
+int main() {
+  myint x = 42;
+  void *p = &x;
+
+  s a;
+  a.f = 43;
+  void *q = &a;
+  return 0;
+}
diff --git a/tests/util/dune b/tests/util/dune
new file mode 100644
index 0000000000..6637217651
--- /dev/null
+++ b/tests/util/dune
@@ -0,0 +1,11 @@
+(executable
+ (name yamlWitnessStrip)
+ (libraries
+   batteries.unthreaded
+   goblint_std
+   goblint_lib
+   yaml
+   goblint.sites.dune
+   goblint.build-info.dune)
+ (flags :standard -open Goblint_std)
+ (preprocess (pps ppx_deriving.std)))
diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml
new file mode 100644
index 0000000000..8a5046d6ff
--- /dev/null
+++ b/tests/util/yamlWitnessStrip.ml
@@ -0,0 +1,86 @@
+open Goblint_lib
+open YamlWitnessType
+
+module StrippedEntry =
+struct
+  type t = {
+    entry_type: EntryType.t;
+  }
+  [@@deriving ord]
+
+  let strip_file_hashes {entry_type} =
+    let stripped_file_hash = "$FILE_HASH" in
+    let location_strip_file_hash location: Location.t =
+      {location with file_hash = stripped_file_hash}
+    in
+    let target_strip_file_hash target: Target.t =
+      {target with file_hash = stripped_file_hash}
+    in
+    let invariant_strip_file_hash ({invariant_type}: InvariantSet.Invariant.t): InvariantSet.Invariant.t =
+      let invariant_type: InvariantSet.InvariantType.t =
+        match invariant_type with
+        | LocationInvariant x ->
+          LocationInvariant {x with location = location_strip_file_hash x.location}
+        | LoopInvariant x ->
+          LoopInvariant {x with location = location_strip_file_hash x.location}
+      in
+      {invariant_type}
+    in
+    let entry_type: EntryType.t =
+      match entry_type with
+      | LocationInvariant x ->
+        LocationInvariant {x with location = location_strip_file_hash x.location}
+      | LoopInvariant x ->
+        LoopInvariant {x with location = location_strip_file_hash x.location}
+      | FlowInsensitiveInvariant x ->
+        FlowInsensitiveInvariant x (* no location to strip *)
+      | PreconditionLoopInvariant x ->
+        PreconditionLoopInvariant {x with location = location_strip_file_hash x.location}
+      | LoopInvariantCertificate x ->
+        LoopInvariantCertificate {x with target = target_strip_file_hash x.target}
+      | PreconditionLoopInvariantCertificate x ->
+        PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target}
+      | InvariantSet x ->
+        InvariantSet {content = List.map invariant_strip_file_hash x.content}
+    in
+    {entry_type}
+
+  let to_yaml {entry_type} =
+    `O ([
+        ("entry_type", `String (EntryType.entry_type entry_type));
+      ] @ EntryType.to_yaml' entry_type)
+end
+
+(* Use set for output, so order is deterministic regardless of Goblint. *)
+module StrippedEntrySet = Set.Make (StrippedEntry)
+
+let main () =
+  let yaml_str = Batteries.input_all stdin in
+  let yaml = Yaml.of_string_exn yaml_str in
+  let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
+
+  let stripped_entries = List.fold_left (fun stripped_entries yaml_entry ->
+      match YamlWitnessType.Entry.of_yaml yaml_entry with
+      | Ok {entry_type; _} ->
+        let stripped_entry: StrippedEntry.t = {entry_type} in
+        StrippedEntrySet.add stripped_entry stripped_entries
+      | Error (`Msg e) ->
+        Format.eprintf "couldn't parse entry: %s" e;
+        stripped_entries
+    ) StrippedEntrySet.empty yaml_entries
+  in
+  let stripped_yaml_entries =
+    StrippedEntrySet.elements stripped_entries
+    |> List.map StrippedEntry.strip_file_hashes
+    |> List.rev_map StrippedEntry.to_yaml
+  in
+
+  let stripped_yaml = `A stripped_yaml_entries in
+  (* to_file/to_string uses a fixed-size buffer... *)
+  let stripped_yaml_str = match GobYaml.to_string' stripped_yaml with
+    | Ok text -> text
+    | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m)
+  in
+  Batteries.output_string Batteries.stdout stripped_yaml_str
+
+let () = main ()