diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index edd251b66f..18935725ca 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -18,7 +18,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 907ff14386..5e586ee038 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -16,7 +16,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - 5.0.x
           - ocaml-variants.4.14.0+options,ocaml-option-flambda
@@ -91,7 +91,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
 
@@ -189,7 +189,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
 
diff --git a/conf/traces-rel.json b/conf/traces-rel.json
index 2b82a57554..eaf6a3f232 100644
--- a/conf/traces-rel.json
+++ b/conf/traces-rel.json
@@ -3,7 +3,8 @@
     "int": {
       "def_exc": true,
       "interval": false,
-      "enums": true
+      "enums": true,
+      "def_exc_widen_by_join": true
     },
     "malloc": {
       "wrappers": [
@@ -79,6 +80,9 @@
       "other": false,
       "loop-head": false,
       "after-lock": true
+    },
+    "yaml" : {
+      "entry-types": ["location_invariant"]
     }
   },
   "pre": {
diff --git a/conf/traces.json b/conf/traces.json
index 7ba21811c0..0e4548ab4f 100644
--- a/conf/traces.json
+++ b/conf/traces.json
@@ -3,7 +3,8 @@
     "int": {
       "def_exc": true,
       "interval": false,
-      "enums": true
+      "enums": true,
+      "def_exc_widen_by_join": true
     },
     "malloc": {
       "wrappers": [
@@ -24,6 +25,14 @@
         "ldv_xzalloc",
         "ldv_calloc"
       ]
+    },
+    "base" : {
+      "invariant": {
+        "enabled": false
+      },
+      "eval": {
+        "deep-query": false
+      }
     }
   },
   "sem": {
@@ -35,9 +44,18 @@
     },
     "builtin_unreachable": {
       "dead_code": true
+    },
+    "int": {
+      "signed_overflow": "assume_none"
     }
   },
   "exp": {
-    "priv-distr-init": false
+    "priv-distr-init": false,
+    "priv-prec-dump-proj" : true
+  },
+  "solvers" : {
+    "td3": {
+      "side_widen" : "sides-pp"
+    }
   }
 }
diff --git a/example_widening_effects.c b/example_widening_effects.c
new file mode 100644
index 0000000000..6074e60adc
--- /dev/null
+++ b/example_widening_effects.c
@@ -0,0 +1,30 @@
+#include <pthread.h>
+int occupied;
+
+pthread_mutex_t mtx;
+
+
+void* thread(void* arg) {
+  pthread_mutex_lock(&mtx);
+
+  if(occupied < 2) {
+    occupied++;
+  }
+
+  pthread_mutex_unlock(&mtx);
+ }
+
+int main() {
+  pthread_t worker;
+
+  pthread_create(&worker, 0, &thread, 0);
+
+  pthread_mutex_lock(&mtx);
+  occupied = 0;
+  pthread_mutex_unlock(&mtx);
+  
+  return 0;
+}
+
+
+// rm out.txt && ./goblint --conf conf/traces.json --set ana.base.privatization protection 2.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.protection.prec --enable ana.int.interval && ./goblint --conf conf/traces.json --set ana.base.privatization write 2.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.write.prec --enable ana.int.interval &&  ./privPrecCompare level-ip.protection.prec level-ip.write.prec &> out.txt
diff --git a/reduce_difference.sh b/reduce_difference.sh
new file mode 100755
index 0000000000..eb0a83a149
--- /dev/null
+++ b/reduce_difference.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+grep "void (\*argmatch_die)(void)  =    & __argmatch_die;" reduce.c
+if [ $? -eq 1 ]; then
+    exit 17
+fi
+grep "static void __argmatch_die(void)" reduce.c
+if [ $? -eq 1 ]; then
+    exit 17
+fi
+grep "usage(1)" reduce.c
+if [ $? -eq 1 ]; then
+    exit 17
+fi
+
+
+/home/michael/Documents/goblint-cil/analyzer/goblint-2  --conf /home/michael/Documents/goblint-cil/analyzer/conf/traces.json --set dbg.timeout 900 --set ana.base.privatization protection 1.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.protection.prec
+/home/michael/Documents/goblint-cil/analyzer/goblint-2  --conf /home/michael/Documents/goblint-cil/analyzer/conf/traces.json --set dbg.timeout 900 --set ana.base.privatization write 1.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.write.prec
+/home/michael/Documents/goblint-cil/analyzer/privPrecCompare level-ip.protection.prec level-ip.write.prec  2> details.txt 1> res.txt
+if [ $? -eq 0 ]; then
+    grep "protection more precise than write" res.txt >/dev/null 2>&1
+else
+    exit 5
+fi
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index f1ea72d0a1..f7aad3cdb5 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -56,7 +56,8 @@ struct
       Priv.read_global ask getg st g x
     else (
       let rel = st.rel in
-      let g_var = RV.global g in
+      (* If it has escaped and we have never been multi-threaded, we can still refer to the local *)
+      let g_var = if g.vglob then RV.global g else RV.local g in
       let x_var = RV.local x in
       let rel' = RD.add_vars rel [g_var] in
       let rel' = RD.assign_var rel' x_var g_var in
@@ -245,25 +246,21 @@ struct
   (* Basic transfer functions. *)
   let assign ctx (lv:lval) e =
     let st = ctx.local in
-    if !AnalysisState.global_initialization && e = MyCFG.unknown_exp then
-      st (* ignore extern inits because there's no body before assign, so env is empty... *)
-    else (
-      let simplified_e = replace_deref_exps ctx.ask e in
-      if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" d_lval lv  d_exp e d_exp simplified_e;
-      let ask = Analyses.ask_of_ctx ctx in
-      let r = assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
-          assign_from_globals_wrapper ask ctx.global st simplified_e (fun apr' e' ->
-              if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
-              if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
-              let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
-              if M.tracing then M.traceu "relation" "-> %a" RD.pretty r;
-              r
-            )
-        )
-      in
-      if M.tracing then M.traceu "relation" "-> %a" D.pretty r;
-      r
-    )
+    let simplified_e = replace_deref_exps ctx.ask e in
+    if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" d_lval lv  d_exp e d_exp simplified_e;
+    let ask = Analyses.ask_of_ctx ctx in
+    let r = assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
+        assign_from_globals_wrapper ask ctx.global st simplified_e (fun apr' e' ->
+            if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
+            if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
+            let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
+            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r;
+            r
+          )
+      )
+    in
+    if M.tracing then M.traceu "relation" "-> %a" D.pretty r;
+    r
 
   let branch ctx e b =
     let st = ctx.local in
@@ -469,10 +466,9 @@ struct
       | None -> None
       | Some st ->
         let ad = ask.f (Queries.ReachableFrom e) in
-        if Queries.AD.is_top ad then
-          None
-        else
-          Some (Queries.AD.join ad st)
+        (* See https://github.com/goblint/analyzer/issues/1535 *)
+        let ad = Queries.AD.remove UnknownPtr ad in
+        Some (Queries.AD.join ad st)
     in
     List.fold_right reachable es (Some (Queries.AD.empty ()))
 
@@ -513,6 +509,35 @@ struct
       if RD.is_bot_env res then raise Deadcode;
       {st with rel = res}
 
+  let special_unknown_invalidate ctx f args =
+    (* No warning here, base already produces the appropriate warnings *)
+    let desc = LibraryFunctions.find f in
+    let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
+    let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
+    let deep_addrs =
+      if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
+        foldGlobals !Cilfacade.current_file (fun acc global ->
+            match global with
+            | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
+              mkAddrOf (Var vi, NoOffset) :: acc
+            (* TODO: what about GVarDecl? *)
+            | _ -> acc
+          ) deep_addrs
+      )
+      else
+        deep_addrs
+    in
+    let lvallist e =
+      match ctx.ask (Queries.MayPointTo e) with
+      | ad when Queries.AD.is_top ad -> []
+      | ad ->
+        Queries.AD.to_mval ad
+        |> List.map ValueDomain.Addr.Mval.to_cil
+    in
+    let st' = forget_reachable ctx ctx.local deep_addrs in
+    let shallow_lvals = List.concat_map lvallist shallow_addrs in
+    List.fold_left (invalidate_one (Analyses.ask_of_ctx ctx) ctx) st' shallow_lvals
+
   let special ctx r f args =
     let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
@@ -548,31 +573,7 @@ struct
          assert_fn {ctx with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
        | None -> st)
     | _, _ ->
-      let lvallist e =
-        match ask.f (Queries.MayPointTo e) with
-        | ad when Queries.AD.is_top ad -> []
-        | ad ->
-          Queries.AD.to_mval ad
-          |> List.map ValueDomain.Addr.Mval.to_cil
-      in
-      let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
-      let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
-      let deep_addrs =
-        if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
-          foldGlobals !Cilfacade.current_file (fun acc global ->
-              match global with
-              | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-                mkAddrOf (Var vi, NoOffset) :: acc
-              (* TODO: what about GVarDecl? *)
-              | _ -> acc
-            ) deep_addrs
-        )
-        else
-          deep_addrs
-      in
-      let st' = forget_reachable ctx st deep_addrs in
-      let shallow_lvals = List.concat_map lvallist shallow_addrs in
-      let st' = List.fold_left (invalidate_one ask ctx) st' shallow_lvals in
+      let st' = special_unknown_invalidate ctx f args in
       (* invalidate lval if present *)
       match r with
       | Some lv -> invalidate_one ask ctx st' lv
@@ -602,6 +603,10 @@ struct
           | Some (Local v) ->
             if VH.mem v_ins_inv v then
               keep_global
+            else if ThreadEscape.has_escaped ask v then
+              (* Escaped local variables should be read in via their v#in# variables, this apron var may refer to stale values only *)
+              (* and is not a sound description of the C variable. *)
+              false
             else
               keep_local
           | _ -> false
@@ -662,35 +667,36 @@ struct
 
   let threadenter ctx ~multiple lval f args =
     let st = ctx.local in
+    (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
+       Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
+       sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
+       EnterMultithreaded events only execute after threadenter and threadspawn. *)
+    if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
+      ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
-      (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
-         Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
-         sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
-         EnterMultithreaded events only execute after threadenter and threadspawn. *)
-      if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
-        ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);
       let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in
       let new_rel = make_callee_rel ~thread:true ctx fd args in
       [{st' with rel = new_rel}]
     | exception Not_found ->
-      (* Unknown functions *)
-      (* TODO: do something like base? *)
-      failwith "relation.threadenter: unknown function"
+      [special_unknown_invalidate ctx f args]
 
   let threadspawn ctx ~multiple lval f args fctx =
     ctx.local
 
   let event ctx e octx =
+    let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
     match e with
-    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr
-    | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      if addr = UnknownPtr then
-        M.info ~category:Unsound "Unknown mutex unlocked, relation privatization unsound"; (* TODO: something more sound *)
+    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
+      CommonPriv.lift_lock ask (fun st m ->
+          Priv.lock ask ctx.global st m
+        ) st addr
+    | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
       WideningTokens.with_local_side_tokens (fun () ->
-          Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr
+          CommonPriv.lift_unlock ask (fun st m ->
+              Priv.unlock ask ctx.global ctx.sideg st m
+            ) st addr
         )
     | Events.EnterMultiThreaded ->
       Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st
@@ -769,7 +775,7 @@ struct
       PCU.RH.replace results ctx.node new_value;
     end;
     WideningTokens.with_local_side_tokens (fun () ->
-        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `Return | `Init | `Thread])
+        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread])
       )
 
   let init marshal =
@@ -778,7 +784,7 @@ struct
   let store_data file =
     let results = PCU.RH.map (fun _ v -> RD.marshal v) results in
     let name = RD.name () ^ "(domain: " ^ (RD.name ()) ^ ", privatization: " ^ (Priv.name ()) ^ (if GobConfig.get_bool "ana.apron.threshold_widening" then ", th" else "" ) ^ ")" in
-    let results: PCU.dump = {marshalled = results; name } in
+    let results: PCU.dump = {marshalled = results; name; disregard = None } in
     Serialize.marshal results file
 
   let finalize () =
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 66548c117c..3184d66bbb 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -36,7 +36,7 @@ module type S =
     val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
     val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
 
-    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `Return | `Init | `Thread] -> relation_components_t
+    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> relation_components_t
 
     val escape: Node.t -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> EscapeDomain.EscapedVars.t -> relation_components_t
     val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> relation_components_t
@@ -96,8 +96,7 @@ struct
     { st with rel = rel_local }
 
   let sync (ask: Q.ask) getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Join ->
+    let branched_sync () =
       if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
         st
       else
@@ -110,6 +109,14 @@ struct
           )
         in
         {st with rel = rel_local}
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread
@@ -336,18 +343,9 @@ struct
   let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
-  let sync ask getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Return -> (* required for thread return *)
-      (* TODO: implement? *)
-      begin match ThreadId.get_current ask with
-        | `Lifted x (* when CPA.mem x st.cpa *) ->
-          st
-        | _ ->
-          st
-      end
-    | `Join ->
-      if (ask.f (Q.MustBeSingleThreaded { since_start= true })) then
+  let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
+    let branched_sync () =
+      if ask.f (Q.MustBeSingleThreaded { since_start= true }) then
         st
       else
         (* must be like enter_multithreaded *)
@@ -375,6 +373,22 @@ struct
            let rel_local' = RD.meet rel_local (getg ()) in
            {st with rel = rel_local'} *)
         st
+    in
+    match reason with
+    | `Return -> (* required for thread return *)
+      (* TODO: implement? *)
+      begin match ThreadId.get_current ask with
+        | `Lifted x (* when CPA.mem x st.cpa *) ->
+          st
+        | _ ->
+          st
+      end
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call () ->
+      branched_sync ()
+    | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread ->
@@ -477,15 +491,21 @@ struct
     let get_mutex_inits' = keep_only_protected_globals ask m get_mutex_inits in
     RD.join get_m get_mutex_inits'
 
-  let get_mutex_global_g_with_mutex_inits ask getg g =
+  let get_mutex_global_g_with_mutex_inits (ask:Q.ask) getg g =
     let g_var = AV.global g in
     let get_mutex_global_g =
-      if Param.handle_atomic then (
-        (* Unprotected invariant is one big relation. *)
-        RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var]
-      )
+      let r =
+        if Param.handle_atomic then
+          (* Unprotected invariant is one big relation. *)
+          RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var]
+        else
+          getg (V.global g)
+      in
+      if RD.is_bot r && (ask.f (Queries.IsAllocVar g)) then
+        (* malloc'ed blobs may not have a value here yet *)
+        RD.top ()
       else
-        getg (V.global g)
+        r
     in
     let get_mutex_inits = getg V.mutex_inits in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
@@ -621,18 +641,9 @@ struct
   let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
-  let sync ask getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Return -> (* required for thread return *)
-      (* TODO: implement? *)
-      begin match ThreadId.get_current ask with
-        | `Lifted x (* when CPA.mem x st.cpa *) ->
-          st
-        | _ ->
-          st
-      end
-    | `Join ->
-      if (ask.f (Q.MustBeSingleThreaded {since_start = true})) then
+  let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
+    let branched_sync () =
+      if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
         st
       else
         let rel = st.rel in
@@ -654,6 +665,22 @@ struct
           )
         in
         {st with rel = rel_local}
+    in
+    match reason with
+    | `Return -> (* required for thread return *)
+      (* TODO: implement? *)
+      begin match ThreadId.get_current ask with
+        | `Lifted x (* when CPA.mem x st.cpa *) ->
+          st
+        | _ ->
+          st
+      end
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call () ->
+      branched_sync ()
+    | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread ->
@@ -697,11 +724,17 @@ module type ClusterArg = functor (RD: RelationDomain.RD) ->
 sig
   module LRD: Lattice.S
 
+  module Cluster: sig
+    include Printable.S
+  end
+
   val keep_only_protected_globals: Q.ask -> LockDomain.Addr.t -> LRD.t -> LRD.t
   val keep_global: varinfo -> LRD.t -> LRD.t
 
   val lock: RD.t -> LRD.t -> LRD.t -> RD.t
-  val unlock: W.t -> RD.t -> LRD.t
+  val unlock: W.t -> RD.t -> LRD.t * (Cluster.t list)
+
+  val filter_clusters: LRD.t -> (Cluster.t -> bool) -> LRD.t
 
   val name: unit -> string
 end
@@ -711,6 +744,7 @@ module NoCluster:ClusterArg = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   module LRD = RD
+  module Cluster = Printable.Unit
 
   let keep_only_protected_globals = keep_only_protected_globals
 
@@ -722,7 +756,13 @@ struct
     RD.meet oct (RD.join local_m get_m)
 
   let unlock w oct_side =
-    oct_side
+    oct_side, [()]
+
+  let filter_clusters oct f =
+    if f () then
+      oct
+    else
+      RD.bot ()
 
   let name () = "no-clusters"
 end
@@ -796,6 +836,8 @@ struct
   module VS = SetDomain.Make (CilType.Varinfo)
   module LRD = MapDomain.MapBot (VS) (RD)
 
+  module Cluster = VS
+
   let keep_only_protected_globals ask m octs =
     (* normal (strong) mapping: contains only still fully protected *)
     (* must filter by protection to avoid later meeting with non-protecting *)
@@ -807,7 +849,9 @@ struct
     let g_var = V.global g in
     (* normal (strong) mapping: contains only still fully protected *)
     let g' = VS.singleton g in
-    let oct = LRD.find g' octs in
+    (* If there is no map entry yet which contains the global, default to top rather than bot *)
+    (* Happens e.g. in 46/86 because of escape *)
+    let oct = Option.default (RD.top ()) (LRD.find_opt g' octs) in
     LRD.singleton g' (RD.keep_vars oct [g_var])
 
   let lock_get_m oct local_m get_m =
@@ -843,7 +887,10 @@ struct
     let oct_side_cluster gs =
       RD.keep_vars oct_side (gs |> VS.elements |> List.map V.global)
     in
-    LRD.add_list_fun clusters oct_side_cluster (LRD.empty ())
+    (LRD.add_list_fun clusters oct_side_cluster (LRD.empty ()), clusters)
+
+  let filter_clusters oct f =
+    LRD.filter (fun gs _ -> f gs) oct
 
   let name = ClusteringArg.name
 end
@@ -859,6 +906,8 @@ struct
   module LRD1 = DCCluster.LRD
   module LRD = Lattice.Prod (LRD1) (LRD1) (* second component is only used between keep_* and lock for additional weak mapping *)
 
+  module Cluster = DCCluster.Cluster
+
   let name = ClusteringArg.name
 
   let filter_map' f m =
@@ -920,7 +969,11 @@ struct
     r
 
   let unlock w oct_side =
-    (DCCluster.unlock w oct_side, LRD1.bot ())
+    let lad, clusters = DCCluster.unlock w oct_side in
+    ((lad, LRD1.bot ()), clusters)
+
+  let filter_clusters (lad,lad') f =
+    (LRD1.filter (fun gs _ -> f gs) lad, LRD1.filter (fun gs _ -> f gs) lad')
 end
 
 (** Per-mutex meet with TIDs. *)
@@ -934,7 +987,7 @@ struct
   module Cluster = NC
   module LRD = NC.LRD
 
-  include PerMutexTidCommon (Digest) (LRD)
+  include PerMutexTidCommon (Digest) (LRD) (NC.Cluster)
 
   module AV = RD.V
   module P = UnitP
@@ -956,13 +1009,11 @@ struct
     let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
     if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.Addr.pretty m LRD.pretty get_m;
     let r =
-      if not inits then
-        get_m
-      else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
-        let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in
-        if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
-        LRD.join get_m get_mutex_inits'
+      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+      let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in
+      let get_mutex_inits' = Cluster.filter_clusters get_mutex_inits' inits in
+      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
+      LRD.join get_m get_mutex_inits'
     in
     if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
     r
@@ -981,13 +1032,11 @@ struct
     in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
-      if not inits then
-        get_mutex_global_g
-      else
-        let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
-        let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in
-        if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
-        LRD.join get_mutex_global_g get_mutex_inits'
+      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+      let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in
+      let get_mutex_inits' = Cluster.filter_clusters get_mutex_inits' inits in
+      if M.tracing then M.trace "relationpriv" "inits=%a\n  inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits';
+      LRD.join get_mutex_global_g get_mutex_inits'
     in
     if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
     r
@@ -995,11 +1044,9 @@ struct
   let get_mutex_global_g_with_mutex_inits_atomic inits ask getg =
     (* Unprotected invariant is one big relation. *)
     let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
-    if not inits then
-      get_mutex_global_g
-    else
-      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
-      LRD.join get_mutex_global_g get_mutex_inits
+    let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+    let get_mutex_inits' = Cluster.filter_clusters get_mutex_inits inits in
+    LRD.join get_mutex_global_g get_mutex_inits'
 
   let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
     let atomic = Param.handle_atomic && ask.f MustBeAtomic in
@@ -1013,9 +1060,9 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg) (* Read unprotected invariant as full relation. *)
       else
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg g)
     in
     (* read *)
     let g_var = AV.global g in
@@ -1047,9 +1094,9 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg) (* Read unprotected invariant as full relation. *)
       else
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg g)
     in
     (* write *)
     let g_var = AV.global g in
@@ -1059,7 +1106,7 @@ struct
     (* unlock *)
     if not atomic then (
       let rel_side = RD.keep_vars rel_local [g_var] in
-      let rel_side = Cluster.unlock (W.singleton g) rel_side in
+      let rel_side, clusters = Cluster.unlock (W.singleton g) rel_side in
       let digest = Digest.current ask in
       let sidev = GMutex.singleton digest rel_side in
       if Param.handle_atomic then
@@ -1073,7 +1120,8 @@ struct
         else
           rel_local
       in
-      {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
+      let lmust' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in
+      {rel = rel_local'; priv = (W.add g w,lmust',l')}
     )
     else
       (* Delay publishing unprotected write in the atomic section. *)
@@ -1085,7 +1133,7 @@ struct
       let rel = st.rel in
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
-      let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
+      let get_m = get_m_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg m in
       let local_m = BatOption.default (LRD.bot ()) (L.find_opt lm l) in
       (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
       let local_m = Cluster.keep_only_protected_globals ask m local_m in
@@ -1115,13 +1163,14 @@ struct
         {rel = rel_local; priv = (w',lmust,l)}
       else
         let rel_side = keep_only_protected_globals ask m rel in
-        let rel_side = Cluster.unlock w rel_side in
+        let rel_side, clusters = Cluster.unlock w rel_side in
         let digest = Digest.current ask in
         let sidev = GMutex.singleton digest rel_side in
         sideg (V.mutex m) (G.create_mutex sidev);
         let lm = LLock.mutex m in
         let l' = L.add lm rel_side l in
-        {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
+        let lmust' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in
+        {rel = rel_local; priv = (w',lmust',l')}
     )
     else (
       (* Publish delayed unprotected write as if it were protected by the atomic section. *)
@@ -1132,14 +1181,15 @@ struct
         {rel = rel_local; priv = (w',lmust,l)}
       else
         let rel_side = keep_only_globals ask m rel in
-        let rel_side = Cluster.unlock w rel_side in
+        let rel_side, clusters = Cluster.unlock w rel_side in
         let digest = Digest.current ask in
         let sidev = GMutex.singleton digest rel_side in
         (* Unprotected invariant is one big relation. *)
         sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
         let (lmust', l') = W.fold (fun g (lmust, l) ->
             let lm = LLock.global g in
-            (LMust.add lm lmust, L.add lm rel_side l)
+            let lmust'' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in
+            (lmust'', L.add lm rel_side l)
           ) w (lmust, l)
         in
         {rel = rel_local; priv = (w',lmust',l')}
@@ -1184,10 +1234,8 @@ struct
     st
 
   let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Return -> st (* TODO: implement? *)
-    | `Join ->
-      if (ask.f (Q.MustBeSingleThreaded {since_start = true})) then
+    let branched_sync () =
+      if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
         st
       else
         let rel = st.rel in
@@ -1201,6 +1249,15 @@ struct
           )
         in
         {st with rel = rel_local}
+    in
+    match reason with
+    | `Return -> st (* TODO: implement? *)
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call () ->
+      branched_sync ()
+    | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread ->
@@ -1222,7 +1279,7 @@ struct
       ) (RD.vars rel)
     in
     let rel_side = RD.keep_vars rel g_vars in
-    let rel_side = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *)
+    let rel_side, clusters = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *)
     let digest = Digest.current ask in
     let sidev = GMutex.singleton digest rel_side in
     sideg V.mutex_inits (G.create_mutex sidev);
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 8e79a5c969..7afe8861b0 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -449,7 +449,7 @@ struct
     else
       ctx.local
 
-  let sync ctx reason = sync' (reason :> [`Normal | `Join | `Return | `Init | `Thread]) ctx
+  let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) ctx
 
   let publish_all ctx reason =
     ignore (sync' reason ctx)
@@ -468,7 +468,6 @@ struct
    *  For the exp argument it is always ok to put None. This means not using precise information about
    *  which part of an array is involved.  *)
   let rec get ~ctx ?(top=VD.top ()) ?(full=false) (st: store) (addrs:address) (exp:exp option): value =
-    let at = AD.type_of addrs in
     let firstvar = if M.tracing then match AD.to_var_may addrs with [] -> "" | x :: _ -> x.vname else "" in
     if M.tracing then M.traceli "get" ~var:firstvar "Address: %a\nState: %a" AD.pretty addrs CPA.pretty st.cpa;
     (* Finding a single varinfo*offset pair *)
@@ -495,10 +494,18 @@ struct
       in
       (* We form the collecting function by joining *)
       let c (x:value) = match x with (* If address type is arithmetic, and our value is an int, we cast to the correct ik *)
-        | Int _ when Cil.isArithmeticType at -> VD.cast at x
+        | Int _ ->
+          let at = AD.type_of addrs in
+          if Cil.isArithmeticType at then
+            VD.cast at x
+          else
+            x
         | _ -> x
       in
       let f x a = VD.join (c @@ f x) a in      (* Finally we join over all the addresses in the set. *)
+      if !AnalysisState.postsolving && get_string "exp.priv-prec-dump" <> "" &&  AD.mem Addr.UnknownPtr addrs then
+        (Hashtbl.replace AnalysisState.location_to_topsify !Goblint_tracing.current_loc ();
+         M.warn "DDDDDDebug: top_pointer at %a" d_loc !Goblint_tracing.current_loc);
       AD.fold f addrs (VD.bot ())
     in
     if M.tracing then M.traceu "get" "Result: %a" VD.pretty res;
@@ -979,41 +986,45 @@ struct
     (* Evaluate structurally using base at first. *)
     let a1 = eval_rv ~ctx st e1 in
     let a2 = eval_rv ~ctx st e2 in
-    let t1 = Option.default_delayed (fun () -> Cilfacade.typeOf e1) t1 in
-    let t2 = Option.default_delayed (fun () -> Cilfacade.typeOf e2) t2 in
-    let r = evalbinop_base ~ctx op t1 a1 t2 a2 t in
-    if Cil.isIntegralType t then (
-      match r with
-      | Int i when ID.to_int i <> None -> r (* Avoid fallback, cannot become any more precise. *)
-      | _ ->
-        (* Fallback to MustBeEqual query, could get extra precision from exprelation/var_eq. *)
-        let must_be_equal () =
-          let r = Q.must_be_equal (Analyses.ask_of_ctx ctx) e1 e2 in
-          if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b" d_exp e1 d_exp e2 r;
-          r
-        in
-        match op with
-        | MinusA when must_be_equal () ->
-          let ik = Cilfacade.get_ikind t in
-          Int (ID.of_int ik Z.zero)
-        | MinusPI (* TODO: untested *)
-        | MinusPP when must_be_equal () ->
-          let ik = Cilfacade.ptrdiff_ikind () in
-          Int (ID.of_int ik Z.zero)
-        (* Eq case is unnecessary: Q.must_be_equal reconstructs BinOp (Eq, _, _, _) and repeats EvalInt query for that, yielding a top from query cycle and never being must equal *)
-        | Le
-        | Ge when must_be_equal () ->
-          let ik = Cilfacade.get_ikind t in
-          Int (ID.of_bool ik true)
-        | Ne
-        | Lt
-        | Gt when must_be_equal () ->
-          let ik = Cilfacade.get_ikind t in
-          Int (ID.of_bool ik false)
-        | _ -> r (* Fallback didn't help. *)
-    )
-    else
-      r (* Avoid fallback, above cases are for ints only. *)
+    try
+      let t1 = Option.default_delayed (fun () -> Cilfacade.typeOf e1) t1 in
+      let t2 = Option.default_delayed (fun () -> Cilfacade.typeOf e2) t2 in
+      let r = evalbinop_base ~ctx op t1 a1 t2 a2 t in
+      if Cil.isIntegralType t then (
+        match r with
+        | Int i when ID.to_int i <> None -> r (* Avoid fallback, cannot become any more precise. *)
+        | _ ->
+          (* Fallback to MustBeEqual query, could get extra precision from exprelation/var_eq. *)
+          let must_be_equal () =
+            let r = Q.must_be_equal (Analyses.ask_of_ctx ctx) e1 e2 in
+            if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b" d_exp e1 d_exp e2 r;
+            r
+          in
+          match op with
+          | MinusA when must_be_equal () ->
+            let ik = Cilfacade.get_ikind t in
+            Int (ID.of_int ik Z.zero)
+          | MinusPI (* TODO: untested *)
+          | MinusPP when must_be_equal () ->
+            let ik = Cilfacade.ptrdiff_ikind () in
+            Int (ID.of_int ik Z.zero)
+          (* Eq case is unnecessary: Q.must_be_equal reconstructs BinOp (Eq, _, _, _) and repeats EvalInt query for that, yielding a top from query cycle and never being must equal *)
+          | Le
+          | Ge when must_be_equal () ->
+            let ik = Cilfacade.get_ikind t in
+            Int (ID.of_bool ik true)
+          | Ne
+          | Lt
+          | Gt when must_be_equal () ->
+            let ik = Cilfacade.get_ikind t in
+            Int (ID.of_bool ik false)
+          | _ -> r (* Fallback didn't help. *)
+      )
+      else
+        r (* Avoid fallback, above cases are for ints only. *)
+    with Cilfacade.TypeOfError _ ->
+      (* Emit top value of corresponding type when there are issues *)
+      VD.top_value t
 
   (* A hackish evaluation of expressions that should immediately yield an
    * address, e.g. when calling functions. *)
@@ -1262,7 +1273,9 @@ struct
   (* TODO: deduplicate https://github.com/goblint/analyzer/pull/1297#discussion_r1477804502 *)
   let rec exp_may_signed_overflow ctx exp =
     let res = match Cilfacade.get_ikind_exp exp with
-      | exception _ -> BoolDomain.MayBool.top ()
+      | exception (Cilfacade.TypeOfError _) (* Cilfacade.typeOf *)
+      | exception (Invalid_argument _) -> (* get_ikind *)
+        BoolDomain.MayBool.top ()
       | ik ->
         let checkBinop e1 e2 binop =
           match ctx.ask (EvalInt e1), ctx.ask (EvalInt e2) with
@@ -1551,7 +1564,7 @@ struct
   let set ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store =
     let update_variable x t y z =
       if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pretty y CPA.pretty z;
-      let r = update_variable x t y z in (* refers to defintion that is outside of set *)
+      let r = update_variable x t y z in (* refers to definition that is outside of set *)
       if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pretty y CPA.pretty z CPA.pretty r;
       r
     in
@@ -1710,7 +1723,7 @@ struct
       (* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *)
       (* If the address was definite, then we just return it. If the address
        * was ambiguous, we have to join it with the initial state. *)
-      let nst = if AD.cardinal lval > 1 then { nst with cpa = CPA.join st.cpa nst.cpa } else nst in
+      let nst = if AD.cardinal lval > 1 then D.join st nst else nst in
       (* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *)
       nst
     with
@@ -2019,7 +2032,7 @@ struct
     (* To invalidate a single address, we create a pair with its corresponding
      * top value. *)
     let invalidate_address st a =
-      let t = AD.type_of a in
+      let t = try AD.type_of a with Not_found -> voidType in (* TODO: why is this called with empty a to begin with? *)
       let v = get ~ctx st a None in (* None here is ok, just causes us to be a bit less precise *)
       let nv =  VD.invalidate_value (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) t v in
       (a, t, nv)
@@ -2136,7 +2149,7 @@ struct
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
-         But here we consider all non-ThreadCrate functions also unknown, so old-style LibraryFunctions access
+         But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
          definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
          Need this to not have memmove spawn in SV-COMP. *)
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
@@ -2338,7 +2351,9 @@ struct
           | Addr.Addr (v, o) -> Addr.Addr (v, lo o)
           | other -> other in
         AD.map rmLastOffset a
-      | _ -> raise (Failure "String function: not an address")
+      | _ ->
+        M.debug ~category:Analyzer "Argument to string function did not evaluate to an address!";
+        AD.top ()
     in
     let string_manipulation s1 s2 lv all op_addr op_array =
       let s1_v = eval_rv ~ctx st s1 in
@@ -3033,12 +3048,14 @@ struct
     match e with
     | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
       if M.tracing then M.tracel "priv" "LOCK EVENT %a" LockDomain.Addr.pretty addr;
-      Priv.lock ask (priv_getg ctx.global) st addr
+      CommonPriv.lift_lock ask (fun st m ->
+          Priv.lock ask (priv_getg ctx.global) st m
+        ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      if addr = UnknownPtr then
-        M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *)
       WideningTokens.with_local_side_tokens (fun () ->
-          Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr
+          CommonPriv.lift_unlock ask (fun st m ->
+              Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st m
+            ) st addr
         )
     | Events.Escape escaped ->
       Priv.escape ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 527d11b1de..0b1aea2dd7 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -31,7 +31,7 @@ sig
   val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
   val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
 
-  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseComponents (D).t
+  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseComponents (D).t
 
   val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t
   val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
@@ -306,8 +306,8 @@ struct
     st
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
-    match reason with
-    | `Join -> (* required for branched thread creation *)
+    let branched_sync () =
+      (* required for branched thread creation *)
       let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in
       sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *)
       (* TODO: this makes mutex-oplus less precise in 28-race_reach/10-ptrmunge_racefree and 28-race_reach/trylock2_racefree, why? *)
@@ -318,6 +318,14 @@ struct
             sideg (V.global x) (CPA.singleton x v)
         ) st.cpa;
       st
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call () ->
+      branched_sync ()
+    | `Join
+    | `JoinCall
     | `Return
     | `Normal
     | `Init
@@ -403,8 +411,8 @@ struct
     {st with cpa = cpa'}
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
-    match reason with
-    | `Join -> (* required for branched thread creation *)
+    let branched_sync () =
+      (* required for branched thread creation *)
       let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in
       sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *)
 
@@ -421,6 +429,14 @@ struct
         ) st.cpa st.cpa
       in
       {st with cpa = cpa'}
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call () ->
+      branched_sync ()
+    | `Join
+    | `JoinCall
     | `Return
     | `Normal
     | `Init
@@ -432,7 +448,7 @@ module PerMutexMeetTIDPriv (Digest: Digest): S =
 struct
   open Queries.Protection
   include PerMutexMeetPrivBase
-  include PerMutexTidCommon (Digest) (CPA)
+  include PerMutexTidCommonNC (Digest) (CPA)
 
   let iter_sys_vars getg vq vf =
     match vq with
@@ -770,9 +786,9 @@ struct
       ) st.cpa st
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
-    let sideg = Wrapper.sideg ask sideg in
-    match reason with
-    | `Join -> (* required for branched thread creation *)
+    let branched_sync () =
+      (* required for branched thread creation *)
+      let sideg = Wrapper.sideg ask sideg in
       CPA.fold (fun x v (st: BaseComponents (D).t) ->
           if is_global ask x && is_unprotected ask x then (
             sideg (V.unprotected x) v;
@@ -782,6 +798,14 @@ struct
           else
             st
         ) st.cpa st
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call () ->
+      branched_sync ()
+    | `Join
+    | `JoinCall
     | `Return
     | `Normal
     | `Init
@@ -1031,6 +1055,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1086,6 +1111,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1157,6 +1183,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1315,6 +1342,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1493,6 +1521,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1675,6 +1704,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1753,8 +1783,10 @@ struct
 
   let read_global ask getg st x =
     let v = Priv.read_global ask getg st x in
-    if !AnalysisState.postsolving && !is_dumping then
-      LVH.modify_def (VD.bot ()) (!Goblint_tracing.current_loc, x) (VD.join v) lvh;
+    if !AnalysisState.postsolving && !is_dumping then (
+      let v_proj = if get_bool "exp.priv-prec-dump-proj" then VD.project ~force_refine:true (Queries.to_value_domain_ask ask) (Some (true,true,true,false,false)) None v else v in
+      LVH.modify_def (VD.bot ()) (!Goblint_tracing.current_loc, x) (VD.join v_proj) lvh
+    );
     v
 
   let dump () =
@@ -1762,7 +1794,7 @@ struct
     (* LVH.iter (fun (l, x) v ->
         Logs.debug "%a %a = %a" CilType.Location.pretty l CilType.Varinfo.pretty x VD.pretty v
       ) lvh; *)
-    Marshal.output f ({name = get_string "ana.base.privatization"; results = lvh}: result);
+    Marshal.output f ({name = get_string "ana.base.privatization" ^ get_string "exp.priv-prec-dump-suffix"; results = lvh; disregard = Some AnalysisState.location_to_topsify}: result);
     close_out_noerr f
 
   let finalize () =
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
index e176a450fa..87b17e5ad0 100644
--- a/src/analyses/basePriv.mli
+++ b/src/analyses/basePriv.mli
@@ -20,7 +20,7 @@ sig
   val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
   val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
 
-  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
+  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
 
   val escape: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseDomain.BaseComponents (D).t
   val enter_multithreaded: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 6376a6ca11..d7174ea850 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -50,6 +50,24 @@ struct
         if not threadflag_path_sens then failwith "The activated privatization requires the 'threadflag' analysis to be path sensitive if it is enabled (it is currently enabled, but not path sensitive)";
         ()
   end
+
+  (** Whether branched thread creation needs to be handled by [sync `Join] of privatization. *)
+  let branched_thread_creation () =
+    let threadflag_active = List.mem "threadflag" (GobConfig.get_string_list "ana.activated") in
+    if threadflag_active then
+      let threadflag_path_sens = List.mem "threadflag" (GobConfig.get_string_list "ana.path_sens") in
+      not threadflag_path_sens
+    else
+      true
+
+  (** Whether branched thread creation at start nodes of procedures needs to be handled by [sync `JoinCall] of privatization. *)
+  let branched_thread_creation_at_call () =
+    let threadflag_active = List.mem "threadflag" (GobConfig.get_string_list "ana.activated") in
+    if threadflag_active then
+      let threadflag_ctx_sens = not (List.mem "threadflag" @@ GobConfig.get_string_list "ana.ctx_insens") in
+      not threadflag_ctx_sens
+    else
+      true
 end
 
 module Protection =
@@ -73,8 +91,8 @@ struct
     ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})
 
   let protected_vars (ask: Q.ask): varinfo list =
-    Q.AD.fold (fun m acc ->
-        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
+    LockDomain.MustLockset.fold (fun ml acc ->
+        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; write = true})) acc
       ) (ask.f Q.MustLockset) (Q.VS.empty ())
     |> Q.VS.elements
 end
@@ -136,8 +154,8 @@ struct
     if !AnalysisState.global_initialization then
       Lockset.empty ()
     else
-      let ad = ask.f Queries.MustLockset in
-      Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* TODO: use AD as Lockset *)
+      let mls = ask.f Queries.MustLockset in
+      LockDomain.MustLockset.fold (fun ml acc -> Lockset.add (Addr (LockDomain.MustLock.to_mval ml)) acc) mls (Lockset.empty ()) (* TODO: use MustLockset as Lockset *)
 
   (* TODO: reversed SetDomain.Hoare *)
   module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
@@ -219,7 +237,7 @@ struct
     | _ -> false
 end
 
-module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
+module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) (Cluster:Printable.S) =
 struct
   include ConfCheck.RequireThreadFlagPathSensInit
 
@@ -250,7 +268,7 @@ struct
 
   (** Mutexes / globals to which values have been published, i.e. for which the initializers need not be read **)
   module LMust = struct
-    include SetDomain.Reverse (SetDomain.ToppedSet (LLock) (struct let topname = "All locks" end))
+    include SetDomain.Reverse (SetDomain.ToppedSet (Printable.Prod(LLock)(Cluster)) (struct let topname = "All locks" end))
     let name () = "LMust"
   end
 
@@ -296,3 +314,49 @@ struct
 
   let startstate () = W.bot (), LMust.top (), L.bot ()
 end
+
+module PerMutexTidCommonNC (Digest: Digest) (LD:Lattice.S) = struct
+  include PerMutexTidCommon (Digest) (LD) (Printable.Unit)
+  module LMust = struct
+    include LMust
+    let mem lm lmust = mem (lm, ()) lmust
+    let add lm lmust = add (lm, ()) lmust
+  end
+end
+
+let lift_lock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
+  (* Should be in sync with:
+     1. LocksetAnalysis.MakeMust.event
+     2. MutexAnalysis.Spec.Arg.add
+     3. LockDomain.MustLocksetRW.add_mval_rw *)
+  match addr with
+  | UnknownPtr -> st
+  | Addr (v, _) when ask.f (IsMultiple v) -> st
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr _
+  | NullPtr
+  | StrPtr _ -> st
+
+let lift_unlock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
+  (* Should be in sync with:
+     1. LocksetAnalysis.MakeMust.event
+     2. MutexAnalysis.Spec.Arg.remove
+     3. MutexAnalysis.Spec.Arg.remove_all
+     4. LockDomain.MustLocksetRW.remove_mval_rw *)
+  match addr with
+  | UnknownPtr ->
+    LockDomain.MustLockset.fold (fun ml st ->
+        (* call privatization's unlock only with definite lock *)
+        f st (LockDomain.Addr.Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+      ) (ask.f MustLockset) st
+  | StrPtr _
+  | NullPtr -> st
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr mv ->
+    LockDomain.MustLockset.fold (fun ml st ->
+        if LockDomain.MustLock.semantic_equal_mval ml mv = Some false then
+          st
+        else
+          (* call privatization's unlock only with definite lock *)
+          f st (Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+      ) (ask.f MustLockset) st
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index c23d6f4294..e83b122fd9 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -30,7 +30,7 @@ struct
     let part_access ctx: MCPAccess.A.t =
       Obj.obj (ctx.ask (PartAccess Point))
 
-    let add ctx ((l, _): LockDomain.Lockset.Lock.t) =
+    let add ctx ((l, _): LockDomain.AddrRW.t) =
       let after: LockEvent.t = (l, ctx.prev_node, part_access ctx) in (* use octx for access to use locksets before event *)
       D.iter (fun before ->
           side_lock_event_pair ctx before after
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 6a816b9e6c..4c8ec3544c 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -29,7 +29,7 @@ sig
   module G: Lattice.S
   module V: SpecSysVar
 
-  val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
+  val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.AddrRW.t -> D.t
   val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
 end
 
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 138f65ab47..b44795b6da 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -1,9 +1,12 @@
 (** Must lockset and protecting lockset analysis ([mutex]). *)
 
 module M = Messages
+module Mval = ValueDomain.Mval
 module Addr = ValueDomain.Addr
-module Lockset = LockDomain.Lockset
-module Mutexes = LockDomain.Mutexes
+module AddrRW = LockDomain.AddrRW
+module MustLockset = LockDomain.MustLockset
+module MustLocksetRW = LockDomain.MustLocksetRW
+module MustMultiplicity = LockDomain.MustMultiplicity
 module LF = LibraryFunctions
 open GoblintCil
 open Analyses
@@ -15,40 +18,10 @@ module Spec =
 struct
   module Arg =
   struct
-    module Multiplicity = struct
-      (* the maximum multiplicity which we keep track of precisely *)
-      let max_count () = 4
-
-      module Count = Lattice.Reverse (
-          Lattice.Chain (
-          struct
-            let n () = max_count () + 1
-            let names x = if x = max_count () then Format.asprintf ">= %d" x else Format.asprintf "%d" x
-          end
-          )
-        )
-
-      include MapDomain.MapTop_LiftBot (ValueDomain.Addr) (Count)
-
-      let name () = "multiplicity"
-
-      let increment v x =
-        let current = find v x in
-        if current = max_count () then
-          x
-        else
-          add v (current + 1) x
-
-      let decrement v x =
-        let current = find v x in
-        if current = 0 then
-          (x, true)
-        else
-          (add v (current - 1) x, current - 1 = 0)
-    end
-
-    module D = struct include Lattice.Prod(Lockset)(Multiplicity)
-      let empty () = (Lockset.empty (), Multiplicity.empty ())
+    module D =
+    struct
+      include Lattice.Prod (MustLocksetRW) (MustMultiplicity)
+      let empty () = (MustLocksetRW.empty (), MustMultiplicity.empty ())
     end
 
 
@@ -60,7 +33,7 @@ struct
 
     module V =
     struct
-      include Printable.Either (struct include CilType.Varinfo let name () = "protecting" end) (struct include ValueDomain.Addr let name () = "protected" end)
+      include Printable.Either (struct include CilType.Varinfo let name () = "protecting" end) (struct include LockDomain.MustLock let name () = "protected" end)
       let name () = "mutex"
       let protecting x = `Left x
       let protected x = `Right x
@@ -98,17 +71,17 @@ struct
     (** Collects information about which variables are protected by which mutexes *)
     module GProtecting: sig
       include Lattice.S
-      val make: write:bool -> recovered:bool -> Mutexes.t -> t
-      val get: write:bool -> Queries.Protection.t -> t -> Mutexes.t
+      val make: write:bool -> recovered:bool -> MustLockset.t -> t
+      val get: write:bool -> Queries.Protection.t -> t -> MustLockset.t
     end = struct
-      include MakeP (LockDomain.Simple)
+      include MakeP (MustLockset)
 
       let make ~write ~recovered locks =
         (* If the access is not a write, set to T so intersection with current write-protecting is identity *)
-        let wlocks = if write then locks else Mutexes.top () in
+        let wlocks = if write then locks else MustLockset.all () in
         if recovered then
           (* If we are in single-threaded mode again, this does not need to be added to set of mutexes protecting in mt-mode only *)
-          ((locks, wlocks), (Mutexes.top (), Mutexes.top ()))
+          ((locks, wlocks), (MustLockset.all (), MustLockset.all ()))
         else
           ((locks, wlocks), (locks, wlocks))
     end
@@ -146,38 +119,57 @@ struct
       let create_protected protected = `Lifted2 protected
     end
 
-    let add ctx (l:Mutexes.elt*bool) =
-      let s,m = ctx.local in
-      let s' = Lockset.add l s in
-      match Addr.to_mval (fst l) with
-      | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
-        (s', Multiplicity.increment (fst l) m)
-      | _ -> (s', m)
-
-    let remove' ctx ~warn l =
-      let s, m = ctx.local in
-      let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
-      if warn &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
-      match Addr.to_mval l with
-      | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
-        let m',rmed = Multiplicity.decrement l m in
-        if rmed then
-          (rm s, m')
+    let add ctx ((addr, rw): AddrRW.t): D.t =
+      match addr with
+      | Addr mv ->
+        let (s, m) = ctx.local in
+        let s' = MustLocksetRW.add_mval_rw (mv, rw) s in
+        let m' =
+          if MutexTypeAnalysis.must_be_recursive ctx mv then
+            MustMultiplicity.increment mv m
+          else
+            m
+        in
+        (s', m')
+      | NullPtr ->
+        M.warn "locking NULL mutex";
+        ctx.local
+      | StrPtr _
+      | UnknownPtr -> ctx.local
+
+    let remove' ctx ~warn (addr: Addr.t): D.t =
+      match addr with
+      | StrPtr _
+      | UnknownPtr -> ctx.local
+      | NullPtr ->
+        if warn then
+          M.warn "unlocking NULL mutex";
+        ctx.local
+      | Addr mv ->
+        let (s, m) = ctx.local in
+        if warn && not (MustLocksetRW.mem_mval mv s) then
+          M.warn "unlocking mutex (%a) which may not be held" Mval.pretty mv;
+        if MutexTypeAnalysis.must_be_recursive ctx mv then (
+          let (m', rmed) = MustMultiplicity.decrement mv m in
+          if rmed then
+            (* TODO: don't repeat the same semantic_equal checks *)
+            (* TODO: rmed per lockset element, not aggregated *)
+            (MustLocksetRW.remove_mval mv s, m')
+          else
+            (s, m')
+        )
         else
-          (s, m')
-      | _ -> (rm s, m)
+          (MustLocksetRW.remove_mval mv s, m) (* Should decrement something if may be recursive? No: https://github.com/goblint/analyzer/pull/1430#discussion_r1615266081. *)
 
     let remove = remove' ~warn:true
 
-    let remove_all ctx =
+    let remove_all ctx: D.t =
       (* Mutexes.iter (fun m ->
            ctx.emit (MustUnlock m)
          ) (D.export_locks ctx.local); *)
       (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *)
       M.warn "unlocking unknown mutex which may not be held";
-      (Lockset.empty (), Multiplicity.empty ())
-
-    let empty () = (Lockset.empty (), Multiplicity.empty ())
+      D.empty ()
   end
   include LocksetAnalysis.MakeMust (Arg)
   let name () = "mutex"
@@ -190,7 +182,7 @@ struct
   module GProtected = Arg.GProtected
   module G = Arg.G
 
-  module GM = Hashtbl.Make (ValueDomain.Addr)
+  module GM = Hashtbl.Make (LockDomain.MustLock)
 
   let max_protected = ref 0
   let num_mutexes = ref 0
@@ -201,46 +193,45 @@ struct
     num_mutexes := 0;
     sum_protected := 0
 
-  let query ctx (type a) (q: a Queries.t): a Queries.result =
+  let query (ctx: (D.t, _, _, V.t) ctx) (type a) (q: a Queries.t): a Queries.result =
     let ls, m = ctx.local in
     (* get the set of mutexes protecting the variable v in the given mode *)
     let protecting ~write mode v = GProtecting.get ~write mode (G.protecting (ctx.global (V.protecting v))) in
-    let non_overlapping locks1 locks2 = Mutexes.is_empty @@ Mutexes.inter locks1 locks2 in
     match q with
-    | Queries.MayBePublic _ when Lockset.is_bot ls -> false
+    | Queries.MayBePublic _ when MustLocksetRW.is_all ls -> false
     | Queries.MayBePublic {global=v; write; protection} ->
-      let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
+      let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if Mutexes.mem verifier_atomic (Lockset.export_locks ctx.local) then
         false
       else *)
-      non_overlapping held_locks protecting
-    | Queries.MayBePublicWithout _ when Lockset.is_bot ls -> false
+      MustLockset.disjoint held_locks protecting
+    | Queries.MayBePublicWithout _ when MustLocksetRW.is_all ls -> false
     | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} ->
-      let held_locks = Lockset.export_locks @@ fst @@ Arg.remove' ctx ~warn:false without_mutex in
+      let held_locks = MustLocksetRW.to_must_lockset @@ fst @@ Arg.remove' ctx ~warn:false without_mutex in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then
         false
       else *)
-      non_overlapping held_locks protecting
-    | Queries.MustBeProtectedBy {mutex; global=v; write; protection} ->
-      let mutex_lockset = Lockset.export_locks @@ Lockset.singleton (mutex, true) in
+      MustLockset.disjoint held_locks protecting
+    | Queries.MustBeProtectedBy {mutex = Addr mutex_mv; global=v; write; protection} when Mval.is_definite mutex_mv -> (* only definite Addrs can be in must-locksets to begin with, anything else cannot protect anything *)
+      let ml = LockDomain.MustLock.of_mval mutex_mv in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
         true
       else *)
-      Mutexes.leq mutex_lockset protecting
+      MustLockset.mem ml protecting
     | Queries.MustLockset ->
-      let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
-      Mutexes.fold (fun addr ls -> Queries.AD.add addr ls) held_locks (Queries.AD.empty ())
+      let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in
+      held_locks
     | Queries.MustBeAtomic ->
-      let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
-      Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks
-    | Queries.MustProtectedVars {mutex = m; write} ->
-      let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
+      let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in
+      MustLockset.mem (LF.verifier_atomic_var, `NoOffset) held_locks (* TODO: Mval.of_var *)
+    | Queries.MustProtectedVars {mutex; write} ->
+      let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected mutex))) in
       VarSet.fold (fun v acc ->
           Queries.VS.add v acc
         ) protected (Queries.VS.empty ())
@@ -252,8 +243,8 @@ struct
         | `Left g' -> (* protecting *)
           if GobConfig.get_bool "dbg.print_protection" then (
             let protecting = GProtecting.get ~write:false Strong (G.protecting (ctx.global g)) in (* readwrite protecting *)
-            let s = Mutexes.cardinal protecting in
-            M.info_noloc ~category:Race "Variable %a read-write protected by %d mutex(es): %a" CilType.Varinfo.pretty g' s Mutexes.pretty protecting
+            let s = MustLockset.cardinal protecting in
+            M.info_noloc ~category:Race "Variable %a read-write protected by %d mutex(es): %a" CilType.Varinfo.pretty g' s MustLockset.pretty protecting
           )
         | `Right m -> (* protected *)
           if GobConfig.get_bool "dbg.print_protection" then (
@@ -262,14 +253,14 @@ struct
             max_protected := max !max_protected s;
             sum_protected := !sum_protected + s;
             incr num_mutexes;
-            M.info_noloc ~category:Race "Mutex %a read-write protects %d variable(s): %a" ValueDomain.Addr.pretty m s VarSet.pretty protected
+            M.info_noloc ~category:Race "Mutex %a read-write protects %d variable(s): %a" LockDomain.MustLock.pretty m s VarSet.pretty protected
           )
       end
     | _ -> Queries.Result.top q
 
   module A =
   struct
-    include Lockset
+    include MustLocksetRW
     let name () = "lock"
     let may_race ls1 ls2 =
       (* not mutually exclusive *)
@@ -287,7 +278,7 @@ struct
   let access ctx (a: Queries.access) =
     fst ctx.local
 
-  let event ctx e octx =
+  let event (ctx: (D.t, _, _, V.t) ctx) e (octx: (D.t, _, _, _) ctx) =
     match e with
     | Events.Access {exp; ad; kind; _} when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
       let is_recovered_to_st = not (ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx)) in
@@ -297,8 +288,8 @@ struct
         (*privatization*)
         match var_opt with
         | Some v ->
-          if not (Lockset.is_bot (fst octx.local)) then
-            let locks = Lockset.export_locks (Lockset.filter snd (fst octx.local)) in
+          if not (MustLocksetRW.is_all (fst octx.local)) then
+            let locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd (fst octx.local)) in
             let write = match kind with
               | Write | Free -> true
               | Read -> false
@@ -314,10 +305,10 @@ struct
               let held_weak = protecting Weak in
               let vs = VarSet.singleton v in
               let protected = G.create_protected @@ GProtected.make ~write vs in
-              Mutexes.iter (fun addr -> ctx.sideg (V.protected addr) protected) held_strong;
+              MustLockset.iter (fun ml -> ctx.sideg (V.protected ml) protected) held_strong;
               (* If the mutex set here is top, it is actually not accessed *)
-              if is_recovered_to_st && not @@ Mutexes.is_top held_weak then
-                Mutexes.iter (fun addr -> ctx.sideg (V.protected addr) protected) held_weak;
+              if is_recovered_to_st && not @@ MustLockset.is_all held_weak then
+                MustLockset.iter (fun ml -> ctx.sideg (V.protected ml) protected) held_weak;
             )
         | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound."
       in
diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
index 7f544b0ffd..2f31384ab9 100644
--- a/src/analyses/mutexEventsAnalysis.ml
+++ b/src/analyses/mutexEventsAnalysis.ml
@@ -4,8 +4,6 @@
 
 module M = Messages
 module Addr = ValueDomain.Addr
-module Lockset = LockDomain.Lockset
-module Mutexes = LockDomain.Mutexes
 module LF = LibraryFunctions
 open Batteries
 open GoblintCil
@@ -21,7 +19,7 @@ struct
   let eval_exp_addr (a: Queries.ask) exp = a.f (Queries.MayPointTo exp)
 
   let lock ctx rw may_fail nonzero_return_when_aquired a lv_opt arg =
-    let compute_refine_split (e:Mutexes.elt) = match e with
+    let compute_refine_split (e: Addr.t) = match e with
       | Addr a ->
         let e' = BinOp(Eq, arg, AddrOf ((PreValueDomain.Mval.to_cil a)), intType) in
         [Events.SplitBranch  (e',true)]
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 6fd18de6ff..b1727ace81 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -23,8 +23,8 @@ struct
 
   exception Top
 
-  module D = LockDomain.Symbolic
-  module C = LockDomain.Symbolic
+  module D = SymbLocksDomain.Symbolic
+  module C = SymbLocksDomain.Symbolic
 
   let name () = "symb_locks"
 
diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml
index b153e71d4e..654f4ee2e1 100644
--- a/src/cdomain/value/cdomains/addressDomain.ml
+++ b/src/cdomain/value/cdomains/addressDomain.ml
@@ -110,6 +110,11 @@ struct
     | StrPtr _, UnknownPtr -> None
     | _, _ -> Some false
 
+  let amenable_to_meet x y = match x,y with
+    | StrPtr _, StrPtr _ -> true
+    | Addr x, Addr y when Mval.equal (Mval.top_indices x) (Mval.top_indices y) -> true
+    | _ -> false
+
   let leq x y = match x, y with
     | StrPtr s1, StrPtr s2   -> SD.leq s1 s2
     | Addr x, Addr y -> Mval.leq x y
@@ -178,6 +183,7 @@ struct
   struct
     include SetDomain.Joined (Addr)
     let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true
+    let amenable_to_meet = Addr.amenable_to_meet
   end
   module OffsetSplit = DisjointDomain.ProjectiveSetPairwiseMeet (Addr) (J) (Addr.UnitOffsetRepr)
 
@@ -238,10 +244,16 @@ struct
     else
       ID.top_of ik
 
+  (** @raise Not_found if set is empty. *)
   let type_of xs =
-    try Addr.type_of (choose xs)
-    with (* WTF? Returns TVoid when it is unknown and stuff??? *)
-    | _ -> voidType
+    try
+      Addr.type_of (choose xs) (* TODO: what if ambiguous type? what if chooses NullPtr but also contains Addr with proper type? *)
+    with
+    (* to be consistent with pre-#1435 behavior *)
+    | Not_found
+    | Cilfacade.TypeOfError _
+    | Offset.Type_of_error _ ->
+      voidPtrType
 
   let of_var x = singleton (Addr.of_var x)
   let of_mval x = singleton (Addr.of_mval x)
diff --git a/src/cdomain/value/cdomains/addressDomain_intf.ml b/src/cdomain/value/cdomains/addressDomain_intf.ml
index f65b2977c4..78c65dd98a 100644
--- a/src/cdomain/value/cdomains/addressDomain_intf.ml
+++ b/src/cdomain/value/cdomains/addressDomain_intf.ml
@@ -80,8 +80,11 @@ sig
 
     val semantic_equal: t -> t -> bool option
     (** Check semantic equality of two addresses.
-
         @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *)
+
+    val amenable_to_meet: t -> t -> bool
+    (** Whether two addresses are amenable to meet operation, i.e., their lattice meet overapproximates the intersection
+        of concretizations. If true, meet is used instead of semantic_equal *)
   end
 
   (** Address lattice with sublattice representatives for {!DisjointDomain}. *)
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 0a850b03a3..a0fbcd15b3 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -228,7 +228,7 @@ sig
   val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t
   val refine_with_incl_list: Cil.ikind -> t -> int_t list option -> t
 
-  val project: Cil.ikind -> int_precision -> t -> t
+  val project: ?force_refine:bool -> Cil.ikind -> int_precision -> t -> t
   val arbitrary: Cil.ikind -> t QCheck.arbitrary
 end
 
@@ -275,7 +275,7 @@ sig
   val ending     : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val is_top_of: Cil.ikind -> t -> bool
 
-  val project: int_precision -> t -> t
+  val project: ?force_refine:bool -> int_precision -> t -> t
   val invariant: Cil.exp -> t -> Invariant.t
 end
 
@@ -381,7 +381,7 @@ struct
 
   let relift x = { v = I.relift x.v; ikind = x.ikind }
 
-  let project p v =  { v = I.project v.ikind p v.v; ikind = v.ikind }
+  let project ?(force_refine=false) p v =  { v = I.project ~force_refine v.ikind p v.v; ikind = v.ikind }
 end
 
 module type Ikind =
@@ -982,7 +982,7 @@ struct
       | Some m1, Some m2 -> refine_with_interval ik (Some(l, u)) (Some (m1, m2))
       | _, _-> intv
 
-  let project ik p t = t
+  let project ?(force_refine=false) ik p t = t
 end
 
 (** IntervalSetFunctor that is not just disjunctive completion of intervals, but attempts to be precise for wraparound arithmetic for unsigned types *)
@@ -1515,7 +1515,7 @@ struct
       let excl_list = List.map (excl_to_intervalset ik range) xs in
       List.fold_left (meet ik) intv excl_list
 
-  let project ik p t = t
+  let project ?(force_refine=false) ik p t = t
 
   let arbitrary ik =
     let open QCheck.Iter in
@@ -2334,7 +2334,7 @@ struct
     | _ -> a
   let refine_with_incl_list ik a b = a
 
-  let project ik p t = t
+  let project ?(force_refine=false) ik p t = t
 end
 
 (* BOOLEAN DOMAINS *)
@@ -2767,7 +2767,7 @@ module Enums : S with type int_t = Z.t = struct
     | Inc x, Some (ls) -> meet ik (Inc x) (Inc (BISet.of_list ls))
     | _ -> a
 
-  let project ik p t = t
+  let project ?(force_refine=false) ik p t = t
 end
 
 module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option =
@@ -3263,7 +3263,7 @@ struct
   let refine_with_excl_list ik a b = a
   let refine_with_incl_list ik a b = a
 
-  let project ik p t = t
+  let project ?(force_refine=false) ik p t = t
 end
 
 module SOverflowLifter (D : S) : SOverflow with type int_t = D.int_t and type t = D.t = struct
@@ -3544,8 +3544,11 @@ module IntDomTupleImpl = struct
      (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b);
      (fun (a, b, c, d, e) -> maybe refine_with_congruence ik (a, b, c, d, e) d)]
 
-  let refine ik ((a, b, c, d, e) : t ) : t =
+  let refine ?(force_refine=false) ik ((a, b, c, d, e) : t ) : t =
     let dt = ref (a, b, c, d, e) in
+    if force_refine then
+      List.iter (fun f -> dt := f !dt) (refine_functions ik)
+    else
     (match get_refinement () with
      | "never" -> ()
      | "once" ->
@@ -3560,7 +3563,8 @@ module IntDomTupleImpl = struct
          if M.tracing then M.trace "cong-refine-loop" "old: %a, new: %a" pretty old_dt pretty !dt;
        done;
      | _ -> ()
-    ); !dt
+    );
+    !dt
 
 
   (* map with overflow check *)
@@ -3669,9 +3673,9 @@ module IntDomTupleImpl = struct
    * ~keep:true will keep elements that are `Some x` but should be set to `None` by p.
    *  This way we won't loose any information for the refinement.
    * ~keep:false will set the elements to `None` as defined by p *)
-  let project ik (p: int_precision) t =
+  let project ?(force_refine=false) ik (p: int_precision) t =
     let t_padded = map ~keep:true { f3 = fun (type a) (module I:SOverflow with type t = a) -> Some (I.top_of ik) } t p in
-    let t_refined = refine ik t_padded in
+    let t_refined = refine ~force_refine ik t_padded in
     map ~keep:false { f3 = fun (type a) (module I:SOverflow with type t = a) -> None } t_refined p
 
 
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index ca64692290..15a7ecf8bb 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -270,7 +270,7 @@ sig
   val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t
   val refine_with_incl_list: Cil.ikind -> t -> int_t list option -> t
 
-  val project: Cil.ikind -> PrecisionUtil.int_precision -> t -> t
+  val project: ?force_refine:bool -> Cil.ikind -> PrecisionUtil.int_precision -> t -> t
   val arbitrary: Cil.ikind -> t QCheck.arbitrary
 end
 (** Interface of IntDomain implementations taking an ikind for arithmetic operations *)
@@ -330,7 +330,7 @@ sig
 
   val is_top_of: Cil.ikind -> t -> bool
 
-  val project: PrecisionUtil.int_precision -> t -> t
+  val project: ?force_refine:bool -> PrecisionUtil.int_precision -> t -> t
   val invariant: Cil.exp -> t -> Invariant.t
 end
 (** The signature of integral value domains keeping track of ikind information *)
diff --git a/src/cdomain/value/cdomains/mval.ml b/src/cdomain/value/cdomains/mval.ml
index 2bc5658460..b9831fa513 100644
--- a/src/cdomain/value/cdomains/mval.ml
+++ b/src/cdomain/value/cdomains/mval.ml
@@ -36,12 +36,13 @@ struct
   let to_cil_exp lv = Lval (to_cil lv)
 
   let is_definite (_, o) = Offs.is_definite o
-  let top_indices (x, o) = (x, Offs.top_indices o)
 end
 
 module MakeLattice (Offs: Offset.Lattice): Lattice with type idx = Offs.idx =
 struct
   include MakePrintable (Offs)
+  
+  let top_indices (x, o) = (x, Offs.top_indices o)
 
   let semantic_equal (x, xoffs) (y, yoffs) =
     if CilType.Varinfo.equal x y then
@@ -72,3 +73,4 @@ end
 
 module Unit = MakePrintable (Offset.Unit)
 module Exp = MakePrintable (Offset.Exp)
+module Z = MakePrintable (Offset.Z)
diff --git a/src/cdomain/value/cdomains/mval_intf.ml b/src/cdomain/value/cdomains/mval_intf.ml
index 7b956bf8b8..542eb1a300 100644
--- a/src/cdomain/value/cdomains/mval_intf.ml
+++ b/src/cdomain/value/cdomains/mval_intf.ml
@@ -17,9 +17,6 @@ sig
 
       @return [Some o] if it is (such that the variables are equal and [add_offset m1 o = m2]), [None] if it is not. *)
 
-  val top_indices: t -> t
-  (** Change all indices to top indices. *)
-
   val to_cil: t -> GoblintCil.lval
   (** Convert to CIL lvalue. *)
 
@@ -35,6 +32,9 @@ sig
   include Printable (** @closed *)
   include Lattice.S with type t := t (** @closed *)
 
+  val top_indices: t -> t
+  (** Change all indices to top indices. *)
+
   val semantic_equal: t -> t -> bool option
   (** Check semantic equality of two mvalues.
 
@@ -57,4 +57,7 @@ sig
 
   (** Mvalue with {!Offset.Exp} indices in offset. *)
   module Exp: Printable with type idx = GoblintCil.exp
+
+  (** Mvalue with {!Offset.Z} indices in offset. *)
+  module Z: Printable with type idx = Z.t
 end
diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
index 7166e0642e..9c9c5c3333 100644
--- a/src/cdomain/value/cdomains/offset.ml
+++ b/src/cdomain/value/cdomains/offset.ml
@@ -41,11 +41,29 @@ struct
 
     let equal_to _ _ = `Top (* TODO: more precise for definite indices *)
     let to_int _ = None (* TODO: more precise for definite indices *)
-    let top () = Lazy.force any
+  end
+
+  module Z =
+  struct
+    include Printable.Z
+    let name () = "Z index"
+    let to_int z = Some z
+    let equal_to z1 z2 =
+      if Z.equal z2 z2 then
+        `Eq
+      else
+        `Neq
   end
 end
 
 
+module Poly =
+struct
+  let rec map_indices g: 'a t -> 'b t = function
+    | `NoOffset -> `NoOffset
+    | `Field (f, o) -> `Field (f, map_indices g o)
+    | `Index (i, o) -> `Index (g i, map_indices g o)
+end
 
 module MakePrintable (Idx: Index.Printable): Printable with type idx = Idx.t =
 struct
@@ -79,6 +97,8 @@ struct
     end
     )
 
+  include Poly
+
   let rec is_definite: t -> bool = function
     | `NoOffset -> true
     | `Field (f,o) -> is_definite o
@@ -103,7 +123,7 @@ struct
     | `Field(f,o) -> Field(f, to_cil_offset o)
     | `Index(i,o) -> NoOffset (* array domain can not deal with this -> leads to being handeled as access to unknown part *)
 
-  let rec to_exp: t -> exp offs = function
+  let rec to_exp: t -> exp offs = function (* TODO: Poly.map_indices *)
     | `NoOffset    -> `NoOffset
     | `Index (i,o) ->
       let i_exp = match Idx.to_int i with
@@ -128,13 +148,6 @@ struct
     | `Field (_, os) -> contains_index os
     | `Index _ -> true
 
-  let rec map_indices g: t -> t = function
-    | `NoOffset -> `NoOffset
-    | `Field (f, o) -> `Field (f, map_indices g o)
-    | `Index (i, o) -> `Index (g i, map_indices g o)
-
-  let top_indices = map_indices (fun _ -> Idx.top ())
-
   (* tries to follow o in t *)
   let rec type_of ~base:t o = match unrollType t, o with (* resolves TNamed *)
     | t, `NoOffset -> t
@@ -179,9 +192,11 @@ struct
   let widen x y = merge `Widen x y
   let narrow x y = merge `Narrow x y
 
+  let top_indices = map_indices (fun _ -> Idx.top ())
+
   (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain
      element) answers with any_index_exp on all non-concrete cases. *)
-  let rec of_exp: exp offs -> t = function
+  let rec of_exp: exp offs -> t = function (* TODO: Poly.map_indices *)
     | `NoOffset    -> `NoOffset
     | `Index (Const (CInt (i,ik,s)),o) -> `Index (Idx.of_int ik i, of_exp o)
     | `Index (_,o) -> `Index (Idx.top (), of_exp o)
@@ -231,7 +246,7 @@ struct
   include MakePrintable (Index.Unit)
 
   (* TODO: rename to of_poly? *)
-  let rec of_offs: 'i offs -> t = function
+  let rec of_offs: 'i offs -> t = function (* TODO: Poly.map_indices *)
     | `NoOffset -> `NoOffset
     | `Field (f,o) -> `Field (f, of_offs o)
     | `Index (i,o) -> `Index ((), of_offs o)
@@ -246,6 +261,8 @@ module Exp =
 struct
   include MakePrintable (Index.Exp)
 
+  let top_indices = map_indices (fun _ -> Lazy.force Index.Exp.any)
+
   let rec of_cil: offset -> t = function
     | NoOffset    -> `NoOffset
     | Index (i,o) -> `Index (i, of_cil o)
@@ -258,6 +275,13 @@ struct
     | `Field (f,o) -> Field (f, to_cil o)
 end
 
+module Z =
+struct
+  include MakePrintable (Index.Z)
+
+  let is_definite _ = true (* override to avoid iterating over offset *)
+end
+
 
 let () = Printexc.register_printer (function
     | Type_of_error (t, o) -> Some (GobPretty.sprintf "Offset.Type_of_error(%a, %s)" d_plaintype t o)
diff --git a/src/cdomain/value/cdomains/offset_intf.ml b/src/cdomain/value/cdomains/offset_intf.ml
index 82117b7d9f..e858f72214 100644
--- a/src/cdomain/value/cdomains/offset_intf.ml
+++ b/src/cdomain/value/cdomains/offset_intf.ml
@@ -15,9 +15,6 @@ struct
   sig
     include Printable.S (** @closed *)
 
-    val top: unit -> t
-    (** Unknown index. *)
-
     val equal_to: Z.t -> t -> [`Eq | `Neq | `Top]
     (** Check semantic equality of an integer and the index.
 
@@ -59,9 +56,6 @@ sig
   val map_indices: (idx -> idx) -> t -> t
   (** Apply function to all indexing. *)
 
-  val top_indices: t -> t
-  (** Change all indices to top indices. *)
-
   val to_cil: t -> GoblintCil.offset
   (** Convert to CIL offset. *)
 
@@ -89,6 +83,9 @@ sig
   include Printable (** @closed *)
   include Lattice.S with type t := t (** @closed *)
 
+  val top_indices: t -> t
+  (** Change all indices to top indices. *)
+
   val of_exp: GoblintCil.exp offs -> t
   (** Convert from Goblint offset with {!GoblintCil.exp} indices. *)
 
@@ -136,11 +133,24 @@ sig
           Used for Goblint-specific witness invariants. *)
       val all: GoblintCil.exp Lazy.t
     end
+
+    module Z: Printable with type t = Z.t
+    (** {!Z} index.
+        Represents a definite index. *)
   end
 
   exception Type_of_error of GoblintCil.typ * string
   (** {!Printable.type_of} could not follow offset completely. *)
 
+  (** Polymorphic offset operations. *)
+  module Poly:
+  sig
+    val map_indices: ('a -> 'b) -> 'a t -> 'b t
+    (** Apply function to all indexing. *)
+
+    (* TODO: include more operations *)
+  end
+
   module type Printable = Printable
   module type Lattice = Lattice
 
@@ -166,10 +176,16 @@ sig
   sig
     include Printable with type idx = GoblintCil.exp
 
+    val top_indices: t -> t
+    (** Change all indices to top indices. *)
+
     val of_cil : GoblintCil.offset -> t
     (** Convert from CIL offset. *)
 
     val to_cil : t -> GoblintCil.offset
     (** Convert to CIL offset. *)
   end
+
+  (** Offset with {!Index.Z} indices. *)
+  module Z: Printable with type idx = Z.t
 end
diff --git a/src/cdomain/value/cdomains/unionDomain.ml b/src/cdomain/value/cdomains/unionDomain.ml
index ad5c531061..cb61b93ab1 100644
--- a/src/cdomain/value/cdomains/unionDomain.ml
+++ b/src/cdomain/value/cdomains/unionDomain.ml
@@ -26,7 +26,11 @@ module Field = struct
     if equal f g then
       f
     else
-      raise Lattice.Uncomparable
+      match f, g with
+      | `Top, f
+      | f, `Top -> f
+      | _ -> raise Lattice.Uncomparable
+
 end
 
 module Simple (Values: Arg) =
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 52bcbd2c7d..0531fb772b 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -40,7 +40,7 @@ sig
 
   include ArrayDomain.Null with type t := t
 
-  val project: VDQ.t -> int_precision option-> ( attributes * attributes ) option -> t -> t
+  val project: ?force_refine:bool -> VDQ.t -> int_precision option-> ( attributes * attributes ) option -> t -> t
   val mark_jmpbufs_as_copied: t -> t
 end
 
@@ -527,32 +527,6 @@ struct
   let warn_type op x y =
     Logs.debug "warn_type %s: incomparable abstr. values %a and %a at %a: %a and %a" op pretty_tag x pretty_tag y CilType.Location.pretty !Goblint_tracing.current_loc pretty x pretty y
 
-  let rec leq x y =
-    match (x,y) with
-    | (_, Top) -> true
-    | (Top, _) -> false
-    | (Bot, _) -> true
-    | (_, Bot) -> false
-    | (Int x, Int y) -> ID.leq x y
-    | (Float x, Float y) -> FD.leq x y
-    | (Int x, Address y) when ID.to_int x = Some Z.zero && not (AD.is_not_null y) -> true
-    | (Int _, Address y) when AD.may_be_unknown y -> true
-    | (Address _, Int y) when ID.is_top_of (Cilfacade.ptrdiff_ikind ()) y -> true
-    | (Address x, Address y) -> AD.leq x y
-    | (Struct x, Struct y) -> Structs.leq x y
-    | (Union x, Union y) -> Unions.leq x y
-    | (Array x, Array y) -> CArrays.leq x y
-    | (Blob x, Blob y) -> Blobs.leq x y
-    | Blob (x,s,o), y -> leq (x:t) y
-    | x, Blob (y,s,o) -> leq x (y:t)
-    | (Thread x, Thread y) -> Threads.leq x y
-    | (Int x, Thread y) -> true
-    | (Address x, Thread y) -> true
-    | (JmpBuf x, JmpBuf y) -> JmpBufs.leq x y
-    | (Mutex, Mutex) -> true
-    | (MutexAttr x, MutexAttr y) -> MutexAttr.leq x y
-    | _ -> warn_type "leq" x y; false
-
   let rec join x y =
     match (x,y) with
     | (Top, _) -> Top
@@ -585,6 +559,41 @@ struct
       warn_type "join" x y;
       Top
 
+  let rec leq x y =
+    match (x,y) with
+    | (_, Top) -> true
+    | (Top, _) -> false
+    | (Bot, _) -> true
+    | (x, Bot) ->
+      if !AnalysisState.bot_in_blob_leq_bot then
+        match x with
+        | Blob (x,s,o) when o -> leq x Bot (* allow only in the case of not zero-initialized blobs *)
+        | Array x ->
+          let contents = CArrays.fold_left join Bot x in
+          leq contents Bot
+        | _ -> false
+      else
+        false
+    | (Int x, Int y) -> ID.leq x y
+    | (Float x, Float y) -> FD.leq x y
+    | (Int x, Address y) when ID.to_int x = Some Z.zero && not (AD.is_not_null y) -> true
+    | (Int _, Address y) when AD.may_be_unknown y -> true
+    | (Address _, Int y) when ID.is_top_of (Cilfacade.ptrdiff_ikind ()) y -> true
+    | (Address x, Address y) -> AD.leq x y
+    | (Struct x, Struct y) -> Structs.leq x y
+    | (Union x, Union y) -> Unions.leq x y
+    | (Array x, Array y) -> CArrays.leq x y
+    | (Blob x, Blob y) -> Blobs.leq x y
+    | Blob (x,s,o), y -> leq (x:t) y
+    | x, Blob (y,s,o) -> leq x (y:t)
+    | (Thread x, Thread y) -> Threads.leq x y
+    | (Int x, Thread y) -> true
+    | (Address x, Thread y) -> true
+    | (JmpBuf x, JmpBuf y) -> JmpBufs.leq x y
+    | (Mutex, Mutex) -> true
+    | (MutexAttr x, MutexAttr y) -> MutexAttr.leq x y
+    | _ -> warn_type "leq" x y; false
+
   let widen x y =
     match (x,y) with
     | (Top, _) -> Top
@@ -973,26 +982,29 @@ struct
           end
         | Blob (x,s,orig), _ ->
           begin
-            let l', o' = shift_one_over l o in
-            let x = zero_init_calloced_memory orig x t in
-            (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
-            let do_strong_update =
-              begin match v with
-                | (Var var, _) ->
-                  let blob_size_opt = ID.to_int s in
-                  not @@ ask.is_multiple var
-                  && Option.is_some blob_size_opt (* Size of blob is known *)
-                  && ((
-                      not @@ Cil.isVoidType t     (* Size of value is known *)
-                      && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t)
-                    ) || blob_destructive)
-                | _ -> false
-              end
-            in
-            if do_strong_update then
-              Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
-            else
-              mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
+            match offs, value with
+            | `NoOffset, Blob (x2, s2, orig2) -> mu (Blob (join x x2, ID.join s s2,ZeroInit.join orig orig2))
+            | _ ->
+              let l', o' = shift_one_over l o in
+              let x = zero_init_calloced_memory orig x t in
+              (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
+              let do_strong_update =
+                begin match v with
+                  | (Var var, _) ->
+                    let blob_size_opt = ID.to_int s in
+                    not @@ ask.is_multiple var
+                    && Option.is_some blob_size_opt (* Size of blob is known *)
+                    && ((
+                        not @@ Cil.isVoidType t     (* Size of value is known *)
+                        && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t)
+                      ) || blob_destructive)
+                  | _ -> false
+                end
+              in
+              if do_strong_update then
+                Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
+              else
+                mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
           end
         | Thread _, _ ->
           (* hack for pthread_t variables *)
@@ -1217,36 +1229,36 @@ struct
   let arbitrary () = QCheck.always Bot (* S TODO: other elements *)
 
   (*Changes the value: if p is present, change all Integer precisions. If array_attr=(varAttr, typeAttr) is present, change the top level array domain according to the attributes *)
-  let rec project ask p array_attr (v: t): t =
+  let rec project ?(force_refine=false) ask p array_attr (v: t): t =
     match v, p, array_attr with
     | _, None, None -> v (*Nothing to change*)
     (* as long as we only have one representation, project is a nop*)
     | Float n, _, _ ->  Float n
-    | Int n, Some p, _->  Int (ID.project p n)
-    | Address n, Some p, _-> Address (project_addr p n)
-    | Struct n, _, _ -> Struct (Structs.map (fun (x: t) -> project ask p None x) n)
-    | Union (f, v), _, _ -> Union (f, project ask p None v)
-    | Array n , _, _ -> Array (project_arr ask p array_attr n)
-    | Blob (v, s, z), Some p', _ -> Blob (project ask p None v, ID.project p' s, z)
+    | Int n, Some p, _->  Int (ID.project ~force_refine p n)
+    | Address n, Some p, _-> Address (project_addr ~force_refine p n)
+    | Struct n, _, _ -> Struct (Structs.map (fun (x: t) -> project ~force_refine ask p None x) n)
+    | Union (f, v), _, _ -> Union (f, project ~force_refine ask p None v)
+    | Array n , _, _ -> Array (project_arr ~force_refine ask p array_attr n)
+    | Blob (v, s, z), Some p', _ -> Blob (project ~force_refine ask p None v, ID.project ~force_refine p' s, z)
     | Thread n, _, _ -> Thread n
     | Bot, _, _ -> Bot
     | Top, _, _ -> Top
     | _, _, _ -> v (*Nothing to change*)
-  and project_addr p a =
+  and project_addr ?(force_refine=false) p a =
     AD.map (fun addr ->
         match addr with
-        | Addr.Addr (v, o) -> Addr.Addr (v, project_offs p o)
+        | Addr.Addr (v, o) -> Addr.Addr (v, project_offs ~force_refine p o)
         | ptr -> ptr) a
-  and project_offs p offs = Offs.map_indices (ID.project p) offs
-  and project_arr ask p array_attr n =
+  and project_offs ?(force_refine=false) p offs = Offs.map_indices (ID.project ~force_refine p) offs
+  and project_arr ?(force_refine=false) ask p array_attr n =
     let n = match array_attr with
       | Some (varAttr,typAttr) -> CArrays.project ~varAttr ~typAttr ask n
       | _ -> n
-    in let n' = CArrays.map (fun (x: t) -> project ask p None x) n in
+    in let n' = CArrays.map (fun (x: t) -> project ~force_refine ask p None x) n in
     match CArrays.length n, p with
     | None, _
     | _, None -> n'
-    | Some l, Some p -> CArrays.update_length (ID.project p l) n'
+    | Some l, Some p -> CArrays.update_length (ID.project ~force_refine p l) n'
 
   let relift state =
     match state with
diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index 813ec25818..c037d70fc2 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -29,7 +29,7 @@ let exp_deep_unroll_types =
 
 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 *)
+  | None ->  true (* vi.vstorage <> Static  CIL pulls static locals into globals, but they aren't syntactically in global scope *)
   | Some fd ->
     if CilType.Fundec.equal fd scope then
       GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index d0ef268ca6..9f0572a32e 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -443,7 +443,18 @@ struct
 
   let show (x:t) =
     Format.asprintf "%a (env: %a)" A.print x (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)
-  let pretty () (x:t) = text (show x)
+
+  (* HACK: Hotfix for https://github.com/goblint/cil/issues/169, remove once that is resolved and dependencies updated *)
+  let custom_text (s:string) =
+    let lines = String.split_on_char '\n' s in
+    let rec doit = function
+      | [] -> nil
+      | [x1] -> text x1
+      | x1::xs -> (text x1) ++ line ++ doit xs
+    in
+    doit lines
+
+  let pretty () (x:t) = custom_text (show x)
 
   let equal x y =
     Environment.equal (A.env x) (A.env y) && A.is_eq Man.mgr x y
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index cc1fb5026a..49d936ddf7 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -263,8 +263,7 @@ struct
     let expr = ref (fst @@ coeff_to_const false (Linexpr1.get_cst linexpr1)) in
     let append_summand (c:Coeff.union_5) v =
       match V.to_cil_varinfo v with
-      | Some vinfo ->
-        (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *)
+      | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
         let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
         let coeff, flip = coeff_to_const true c in
         let prod = BinOp(Mult, coeff, var, longlong) in
@@ -273,6 +272,7 @@ struct
         else
           expr := BinOp(PlusA,!expr,prod,longlong)
       | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %s"  (Var.to_string v); raise Unsupported_Linexpr1
+      | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %s"  (Var.to_string v); raise Unsupported_Linexpr1
     in
     Linexpr1.iter append_summand linexpr1;
     !expr
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index baee8a2ce6..35d73e5f28 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -1,126 +1,161 @@
 (** Lockset domains. *)
 
-module Addr = ValueDomain.Addr
-module Offs = ValueDomain.Offs
-module Exp = CilType.Exp
-module IdxDom = ValueDomain.IndexDomain
+open struct
+  module MvalZ = Mval.Z (* So we can define MustLock using Mval.Z after redefining Mval *)
+end
 
-open GoblintCil
+module IndexDomain = ValueDomain.IndexDomain
+module Mval = ValueDomain.Mval
+module Addr = ValueDomain.Addr
 
-module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO: AD? *)
-module Simple = Lattice.Reverse (Mutexes)
-module Priorities = IntDomain.Lifted
+module MustLock =
+struct
+  include MvalZ
+
+  let semantic_equal_mval ((v, o): t) ((v', o'): Mval.t): bool option =
+    if CilType.Varinfo.equal v v' then (
+      let (index1, _) = GoblintCil.bitsOffset v.vtype (Offset.Z.to_cil o) in (* TODO: better way to compute this? as Z.t not int *)
+      let index2: IndexDomain.t = ValueDomain.Offs.to_index ~typ:v.vtype o' in (* TODO: is this bits or bytes? *)
+      match IndexDomain.equal_to (Z.of_int index1) index2 with
+      | `Eq -> Some true
+      | `Neq -> Some false
+      | `Top -> None
+    )
+    else
+      Some false
+
+  let of_mval ((v, o): Mval.t): t =
+    (v, Offset.Poly.map_indices (fun i -> IndexDomain.to_int i |> Option.get) o)
+
+  let to_mval ((v, o): t): Mval.t =
+    (v, Offset.Poly.map_indices (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) o)
+end
 
-module Lockset =
+module MustLockset =
 struct
+  include SetDomain.Reverse (SetDomain.ToppedSet (MustLock) (struct let topname = "All mutexes" end))
 
-  (* true means exclusive lock and false represents reader lock*)
-  module RW   = IntDomain.Booleans
+  let all (): t = `Top
+  let is_all (set: t) = set = `Top
+end
 
-  (* pair Addr and RW; also change pretty printing*)
-  module Lock =
-  struct
-    include Printable.Prod (Addr) (RW)
+(* true means exclusive lock and false represents reader lock*)
+module RW   = IntDomain.Booleans
 
-    let pretty () (a, write) =
-      if write then
-        Addr.pretty () a
-      else
-        Pretty.dprintf "read lock %a" Addr.pretty a
+(* pair Addr and RW; also change pretty printing*)
+module MakeRW (P: Printable.S) =
+struct
+  include Printable.Prod (P) (RW)
+
+  let pretty () (a, write) =
+    if write then
+      P.pretty () a
+    else
+      GoblintCil.Pretty.dprintf "read lock %a" P.pretty a
+
+  include Printable.SimplePretty (
+    struct
+      type nonrec t = t
+      let pretty = pretty
+    end
+    )
+end
 
-    include Printable.SimplePretty (
-      struct
-        type nonrec t = t
-        let pretty = pretty
-      end
-      )
-  end
+module MvalRW = MakeRW (Mval)
+module AddrRW = MakeRW (Addr)
+module MustLockRW = MakeRW (MustLock)
 
-  include SetDomain.Reverse(SetDomain.ToppedSet (Lock) (struct let topname = "All mutexes" end))
+module MustLocksetRW =
+struct
+  include SetDomain.Reverse (SetDomain.ToppedSet (MustLockRW) (struct let topname = "All mutexes" end))
   let name () = "lockset"
 
-  let add ((addr, _) as lock) set =
-    match addr with
-    | Addr.Addr mv when Addr.Mval.is_definite mv -> (* avoids NULL *)
-      add lock set
-    | _ ->
+  let add_mval_rw ((mv, rw): MvalRW.t) (set: t) =
+    if Addr.Mval.is_definite mv then
+      add (MustLock.of_mval mv, rw) set
+    else
       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
+  let remove_mval_rw ((mv, rw): MvalRW.t) (set: t) =
+    if Addr.Mval.is_definite mv then
+      remove (MustLock.of_mval mv, rw) set
+    else
+      filter (fun (ml, _) ->
+          MustLock.semantic_equal_mval ml mv = Some false
         ) set
 
-  let export_locks ls =
-    let f (x,_) set = Mutexes.add x set in
-    fold f ls (Mutexes.empty ())
+  let mem_mval (mv: Mval.t) (set: t) =
+    if Mval.is_definite mv then (
+      let ml = MustLock.of_mval mv in
+      mem (ml, true) set || mem (ml, false) set
+    )
+    else
+      false
+
+  let remove_mval (mv: Mval.t) set =
+    remove_mval_rw (mv, true) (remove_mval_rw (mv, false) set)
+
+  let all (): t = `Top
+  let is_all (set: t) = set = `Top
+
+  let to_must_lockset (ls: t): MustLockset.t =
+    let f (ml, _) set = MustLockset.add ml set in
+    fold f ls (MustLockset.empty ())
 end
 
-module MayLockset =
-struct
-  include Lockset
-  let leq x y = leq y x
-  let join = Lockset.meet
-  let meet = Lockset.join
-  let top = Lockset.bot
-  let bot = Lockset.top
+module MustMultiplicity = struct
+  (* the maximum multiplicity which we keep track of precisely *)
+  let max_count () = 4
+
+  module Count = Lattice.Reverse (
+      Lattice.Chain (
+      struct
+        let n () = max_count () + 1
+        let names x = if x = max_count () then Format.asprintf ">= %d" x else Format.asprintf "%d" x
+      end
+      )
+    )
+
+  include MapDomain.MapTop_LiftBot (MustLock) (Count)
+
+  let name () = "multiplicity"
+
+  let increment v x =
+    let current = find v x in
+    if current = max_count () then
+      x
+    else
+      add v (current + 1) x
+
+  let increment mv m =
+    if Addr.Mval.is_definite mv then
+      increment (MustLock.of_mval mv) m
+    else
+      m
+
+  let decrement v x =
+    let current = find v x in
+    if current = 0 then
+      (x, true)
+    else
+      (add v (current - 1) x, current - 1 = 0) (* TODO: remove if 0? *)
+
+  let decrement mv m =
+    if Addr.Mval.is_definite mv then
+      decrement (MustLock.of_mval mv) m
+    else
+      (* TODO: non-definite should also decrement (to 0)? *)
+      fold (fun ml _ (m, rmed) ->
+          if MustLock.semantic_equal_mval ml mv = Some false then
+            (m, rmed)
+          else (
+            let (m', rmed') = decrement ml m in
+            (m', rmed || rmed')
+          )
+        ) m (m, false)
 end
 
 module MayLocksetNoRW =
 struct
   include PreValueDomain.AD
 end
-
-module Symbolic =
-struct
-  (* TODO: use SetDomain.Reverse *)
-  module S = SetDomain.ToppedSet (Exp) (struct let topname = "All mutexes" end)
-  include Lattice.Reverse (S)
-
-  let rec eq_set (ask: Queries.ask) e =
-    S.union
-      (match ask.f (Queries.EqualSet e) with
-       | es when not (Queries.ES.is_bot es) ->
-         Queries.ES.fold S.add es (S.empty ())
-       | _ -> S.empty ())
-      (match e with
-       | SizeOf _
-       | SizeOfE _
-       | SizeOfStr _
-       | AlignOf _
-       | Const _
-       | AlignOfE _
-       | UnOp _
-       | BinOp _
-       | Question _
-       | Real _
-       | Imag _
-       | AddrOfLabel _ -> S.empty ()
-       | AddrOf  (Var _,_)
-       | StartOf (Var _,_)
-       | Lval    (Var _,_) -> S.singleton e
-       | AddrOf  (Mem e,ofs) -> S.map (fun e -> AddrOf  (Mem e,ofs)) (eq_set ask e)
-       | StartOf (Mem e,ofs) -> S.map (fun e -> StartOf (Mem e,ofs)) (eq_set ask e)
-       | Lval    (Mem e,ofs) -> S.map (fun e -> Lval    (Mem e,ofs)) (eq_set ask e)
-       | CastE (_,e)           -> eq_set ask e
-      )
-
-  let add (ask: Queries.ask) e st =
-    let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
-    let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
-    S.union addrs st
-  let remove ask e st =
-    (* TODO: Removing based on must-equality sets is not sound! *)
-    let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
-    let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
-    S.diff st addrs
-  let remove_var v st = S.filter (fun x -> not (SymbLocksDomain.Exp.contains_var v x)) st
-
-  let filter = S.filter
-  let fold = S.fold
-
-end
diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml
index ba2b96e8d0..10ea70da1d 100644
--- a/src/cdomains/symbLocksDomain.ml
+++ b/src/cdomains/symbLocksDomain.ml
@@ -317,3 +317,54 @@ struct
 
   let of_mval (v, o) = of_mval (v, conv_const_offset o)
 end
+
+
+module Symbolic =
+struct
+  (* TODO: use SetDomain.Reverse *)
+  module S = SetDomain.ToppedSet (CilType.Exp) (struct let topname = "All mutexes" end)
+  include Lattice.Reverse (S)
+
+  let rec eq_set (ask: Queries.ask) e =
+    S.union
+      (match ask.f (Queries.EqualSet e) with
+       | es when not (Queries.ES.is_bot es) ->
+         Queries.ES.fold S.add es (S.empty ())
+       | _ -> S.empty ())
+      (match e with
+       | SizeOf _
+       | SizeOfE _
+       | SizeOfStr _
+       | AlignOf _
+       | Const _
+       | AlignOfE _
+       | UnOp _
+       | BinOp _
+       | Question _
+       | Real _
+       | Imag _
+       | AddrOfLabel _ -> S.empty ()
+       | AddrOf  (Var _,_)
+       | StartOf (Var _,_)
+       | Lval    (Var _,_) -> S.singleton e
+       | AddrOf  (Mem e,ofs) -> S.map (fun e -> AddrOf  (Mem e,ofs)) (eq_set ask e)
+       | StartOf (Mem e,ofs) -> S.map (fun e -> StartOf (Mem e,ofs)) (eq_set ask e)
+       | Lval    (Mem e,ofs) -> S.map (fun e -> Lval    (Mem e,ofs)) (eq_set ask e)
+       | CastE (_,e)           -> eq_set ask e
+      )
+
+  let add (ask: Queries.ask) e st =
+    let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
+    let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
+    S.union addrs st
+  let remove ask e st =
+    (* TODO: Removing based on must-equality sets is not sound! *)
+    let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
+    let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
+    S.diff st addrs
+  let remove_var v st = S.filter (fun x -> not (Exp.contains_var v x)) st
+
+  let filter = S.filter
+  let fold = S.fold
+
+end
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index b0e5d725a7..79b2f73518 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -803,3 +803,17 @@ struct
 
   let to_yojson x = x (* override SimplePretty *)
 end
+
+module Z: S with type t = Z.t =
+struct
+  include StdLeaf
+  include GobZ
+  let name () = "Z"
+
+  include SimplePretty (
+    struct
+      type nonrec t = t
+      let pretty = pretty
+    end
+    )
+end
diff --git a/src/common/framework/analysisState.ml b/src/common/framework/analysisState.ml
index fd76e1bb67..8ca89f8c28 100644
--- a/src/common/framework/analysisState.ml
+++ b/src/common/framework/analysisState.ml
@@ -30,3 +30,8 @@ let postsolving = ref false
 
 (* None if verification is disabled, Some true if verification succeeded, Some false if verification failed *)
 let verified : bool option ref = ref None
+
+(* Comparison mode where blobs with bot content that are not zero-initalized are considered equivalent to top-level bot *)
+let bot_in_blob_leq_bot = ref false
+
+let location_to_topsify: (GoblintCil.location,unit) Hashtbl.t = Hashtbl.create 10
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 2a4e73d588..99430ee8b6 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -199,7 +199,8 @@ let getFuns fileAST : startfuns =
 let getFirstStmt fd = List.hd fd.sbody.bstmts
 
 
-(* Returns the ikind of a TInt(_) and TEnum(_). Unrolls typedefs. *)
+(** Returns the ikind of a TInt(_) and TEnum(_). Unrolls typedefs.
+    @raise Invalid_argument if not integral type. *)
 let rec get_ikind t =
   (* important to unroll the type here, otherwise problems with typedefs *)
   match Cil.unrollType t with
@@ -208,6 +209,7 @@ let rec get_ikind t =
   | TPtr _ -> get_ikind !Cil.upointType
   | _ -> invalid_arg ("Cilfacade.get_ikind: non-integer type " ^ CilType.Typ.show t)
 
+(** @raise Invalid_argument if not floating-point type. *)
 let get_fkind t =
   (* important to unroll the type here, otherwise problems with typedefs *)
   match Cil.unrollType t with
@@ -245,6 +247,7 @@ let () = Printexc.register_printer (function
 (* Cil doesn't expose this *)
 let stringLiteralType = ref charPtrType
 
+(** @raise TypeOfError *)
 let typeOfRealAndImagComponents t =
   match unrollType t with
   | TInt _ -> t
@@ -272,6 +275,7 @@ let isComplexFKind = function
   | FComplexLongDouble
   | FComplexFloat128 -> true
 
+(** @raise TypeOfError *)
 let rec typeOf (e: exp) : typ =
   match e with
   | Const(CInt (_, ik, _)) -> TInt(ik, [])
@@ -308,11 +312,13 @@ let rec typeOf (e: exp) : typ =
       | _ -> raise (TypeOfError StartOf_NonArray)
     end
 
+(** @raise TypeOfError *)
 and typeOfInit (i: init) : typ =
   match i with
     SingleInit e -> typeOf e
   | CompoundInit (t, _) -> t
 
+(** @raise TypeOfError *)
 and typeOfLval = function
     Var vi, off -> typeOffset vi.vtype off
   | Mem addr, off -> begin
@@ -321,6 +327,7 @@ and typeOfLval = function
       | _ -> raise (TypeOfError (Mem_NonPointer addr))
     end
 
+(** @raise TypeOfError *)
 and typeOffset basetyp =
   let blendAttributes baseAttrs =
     let (_, _, contageous) =
@@ -363,7 +370,12 @@ let mkCast ~(e: exp) ~(newt: typ) =
   in
   Cil.mkCastT ~e ~oldt ~newt
 
+(** @raise TypeOfError
+    @raise Invalid_argument if not integral type. *)
 let get_ikind_exp e = get_ikind (typeOf e)
+
+(** @raise TypeOfError
+    @raise Invalid_argument if not floating-point type. *)
 let get_fkind_exp e = get_fkind (typeOf e)
 
 (** Make {!Cil.BinOp} with correct implicit casts inserted. *)
diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml
index 355a999fbf..1a3daf616d 100644
--- a/src/config/gobConfig.ml
+++ b/src/config/gobConfig.ml
@@ -168,7 +168,8 @@ struct
         Index (parse_index idx, parse_path' pth)
       | _ -> raise PathParseError
 
-  (** Parse a string path, but you may ignore the first dot. *)
+  (** Parse a string path, but you may ignore the first dot.
+      @raise Failure if path couldn't be parsed. *)
   let parse_path (s:string) : path =
     let s = String.trim s in
     try
@@ -180,7 +181,7 @@ struct
       end
     with PathParseError ->
       Logs.error "Error: Couldn't parse the json path '%s'" s;
-      failwith "parsing"
+      failwith "parsing" (* TODO: return ParsePathError still? *)
 
   (** Here we store the actual configuration. *)
   let json_conf : Yojson.Safe.t ref = ref `Null
@@ -252,7 +253,11 @@ struct
       Fun.protect ~finally:(fun () -> set_immutable false) f
     )
 
-  (** The main function to write new values into the conf. Use [set_value] to properly invalidate cache and check immutability. *)
+  (** The main function to write new values into the conf. Use [set_value] to properly invalidate cache and check immutability.
+      @raise Failure
+      @raise TypeError
+      @raise Invalid_argument
+      @raise Json_encoding.Cannot_destruct *)
   let unsafe_set_value v o orig_pth =
     let rec set_value v o pth =
       match o, pth with
@@ -343,13 +348,19 @@ struct
 
   (** Helper functions for writing values. *)
 
-  (** Sets a value, preventing changes when the configuration is immutable and invalidating the cache. *)
+  (** Sets a value, preventing changes when the configuration is immutable and invalidating the cache.
+      @raise Immutable *)
   let set_value v o pth =
     if is_immutable () then raise (Immutable pth);
     drop_memo ();
     unsafe_set_value v o pth
 
-  (** Helper function for writing values. Handles the tracing. *)
+  (** Helper function for writing values. Handles the tracing.
+      @raise Failure if path couldn't be parsed.
+      @raise Immutable
+      @raise TypeError
+      @raise Invalid_argument
+      @raise Json_encoding.Cannot_destruct *)
   let set_path_string st v =
     if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pretty v;
     set_value v json_conf (parse_path st)
@@ -377,9 +388,15 @@ struct
         set_path_string st v
       with Yojson.Json_error _ | TypeError _ ->
         set_string st s
-    with e ->
+    with
+    | Failure _
+    | Immutable _
+    | TypeError _
+    | Invalid_argument _
+    | Json_encoding.Cannot_destruct _ as e ->
+      let bt = Printexc.get_raw_backtrace () in
       Logs.error "Cannot set %s to '%s'." st s;
-      raise e
+      Printexc.raise_with_backtrace e bt
 
   let merge json =
     Validator.validate_exn json;
diff --git a/src/config/jsonSchema.ml b/src/config/jsonSchema.ml
index 59b9733ca2..b2a0ef8735 100644
--- a/src/config/jsonSchema.ml
+++ b/src/config/jsonSchema.ml
@@ -153,7 +153,7 @@ module Validator (Schema: Schema) =
 struct
   let schema_encoding = encoding_of_schema Schema.schema
 
-  (** Raises [Json_encoding.Cannot_destruct] if invalid. *)
+  (** @raise Json_encoding.Cannot_destruct if invalid. *)
   let validate_exn json = JE.destruct schema_encoding json
 
   (* TODO: bool-returning validate? *)
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index db93e74ff4..f83ea88e75 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1634,6 +1634,18 @@
           "type": "string",
           "default": ""
         },
+        "priv-prec-dump-suffix": {
+          "title": "exp.priv-prec-dump-suffix",
+          "description": "Suffix for name of precision dump. Useful if one has several configurations for one privatization.",
+          "type": "string",
+          "default": ""
+        },
+        "priv-prec-dump-proj": {
+          "title": "exp.priv-prec-dump-proj",
+          "description": "Project to (enums * def_exc * interval) precision for privatization precision dump.",
+          "type": "boolean",
+          "default": false
+        },
         "priv-distr-init": {
           "title": "exp.priv-distr-init",
           "description":
@@ -1794,7 +1806,7 @@
           "title": "exp.hide-std-globals",
           "description": "Hide standard extern globals (e.g. `stdout`) from cluttering local states.",
           "type": "boolean",
-          "default": true
+          "default": false
         },
         "arg": {
           "title": "exp.arg",
diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml
index d8e59c4ba7..00f875bb3a 100644
--- a/src/domain/disjointDomain.ml
+++ b/src/domain/disjointDomain.ml
@@ -182,16 +182,26 @@ module type MayEqualSetDomain =
 sig
   include SetDomain.S
   val may_be_equal: elt -> elt -> bool
+  val amenable_to_meet: elt -> elt -> bool
 end
 
-module ProjectiveSetPairwiseMeet (E: Printable.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct
+module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct
   include ProjectiveSet (E) (B) (R)
 
   let meet m1 m2 =
     let meet_buckets b1 b2 acc =
       B.fold (fun e1 acc ->
           B.fold (fun e2 acc ->
-              if B.may_be_equal e1 e2 then
+              if B.amenable_to_meet e1 e2 then
+                try
+                  let m = E.meet e1 e2 in
+                  if not (E.is_bot m) then
+                    add m acc
+                  else
+                    acc
+                with Lattice.Uncomparable ->
+                  failwith (GobPretty.sprintf "amenable_to_meet %a %a returned true, but meet throws!" E.pretty e1 E.pretty e2)
+              else if B.may_be_equal e1 e2 then
                 add e1 (add e2 acc)
               else
                 acc
diff --git a/src/domains/events.ml b/src/domains/events.ml
index 06561bddbe..b194847bac 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -4,7 +4,7 @@ open GoblintCil
 open Pretty
 
 type t =
-  | Lock of LockDomain.Lockset.Lock.t
+  | Lock of LockDomain.AddrRW.t
   | Unlock of LockDomain.Addr.t
   | Escape of EscapeDomain.EscapedVars.t
   | EnterMultiThreaded
@@ -35,7 +35,7 @@ let emit_on_deadcode = function
     false
 
 let pretty () = function
-  | Lock m -> dprintf "Lock %a" LockDomain.Lockset.Lock.pretty m
+  | Lock m -> dprintf "Lock %a" LockDomain.AddrRW.pretty m
   | Unlock m -> dprintf "Unlock %a" LockDomain.Addr.pretty m
   | Escape escaped -> dprintf "Escape %a" EscapeDomain.EscapedVars.pretty escaped
   | EnterMultiThreaded -> text "EnterMultiThreaded"
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index f5d7be21a4..a904f696eb 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -51,7 +51,7 @@ end
 type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
 type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: PreValueDomain.Addr.t; protection: Protection.t} [@@deriving ord, hash]
 type mustbeprotectedby = {mutex: PreValueDomain.Addr.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
-type mustprotectedvars = {mutex: PreValueDomain.Addr.t; write: bool} [@@deriving ord, hash]
+type mustprotectedvars = {mutex: LockDomain.MustLock.t; write: bool} [@@deriving ord, hash]
 type access =
   | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *)
   | Point (** Program point and state access (MHP), independent of memory location. *)
@@ -74,7 +74,7 @@ type _ t =
   | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *)
   | MayBePublicWithout: maybepublicwithout -> MayBool.t t
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
-  | MustLockset: AD.t t
+  | MustLockset: LockDomain.MustLockset.t t
   | MustBeAtomic: MustBool.t t
   | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t
   | MustBeUniqueThread: MustBool.t t
@@ -147,7 +147,7 @@ struct
     | MayPointTo _ -> (module AD)
     | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
-    | MustLockset -> (module AD)
+    | MustLockset -> (module LockDomain.MustLockset)
     | EvalFunvar _ -> (module AD)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
@@ -216,7 +216,7 @@ struct
     | MayPointTo _ -> AD.top ()
     | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
-    | MustLockset -> AD.top ()
+    | MustLockset -> LockDomain.MustLockset.top ()
     | EvalFunvar _ -> AD.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index c8464f6e84..844a387b2b 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -208,7 +208,7 @@ sig
 
   val context : fundec -> D.t -> C.t
 
-  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `Return] -> D.t
+  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall | `Return] -> D.t
   val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result
 
   (** A transfer function which handles the assignment of a rval to a lval, i.e.,
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index aba2ad695f..478864d62e 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -528,9 +528,10 @@ struct
 
   let sync ctx =
     match ctx.prev_node, Cfg.prev ctx.prev_node with
-    | _, _ :: _ :: _ (* Join in CFG. *)
-    | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+    | _, _ :: _ :: _ -> (* Join in CFG. *)
       S.sync ctx `Join
+    | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+      S.sync ctx `JoinCall
     | _, _ -> S.sync ctx `Normal
 
   let side_context sideg f c =
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 62abcbcb60..a8f0c71912 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -384,6 +384,8 @@ module MessageUtil = MessageUtil
 module AnsiColors = AnsiColors
 module XmlUtil = XmlUtil
 
+module GobExn = GobExn
+
 (** {2 CIL} *)
 
 module CilType = CilType
diff --git a/src/privPrecCompare.ml b/src/privPrecCompare.ml
index b4588e25bd..3b2e385383 100644
--- a/src/privPrecCompare.ml
+++ b/src/privPrecCompare.ml
@@ -4,4 +4,5 @@ open Goblint_lib
 module A = PrecCompare.MakeDump (PrivPrecCompareUtil)
 
 let () =
+  AnalysisState.bot_in_blob_leq_bot := true;
   A.main ()
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index eab06222ef..034dd4d257 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -27,7 +27,7 @@ module EvalAssert = struct
   let surroundByAtomic = true
 
   (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-  let ass = makeVarinfo true "__VERIFIER_assert" (TVoid [])
+  let ass = makeVarinfo true "assert" (TVoid [])
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml
index 88b273ab6d..66fc85bafa 100644
--- a/src/transform/expressionEvaluation.ml
+++ b/src/transform/expressionEvaluation.ml
@@ -31,7 +31,7 @@ struct
 
   let (~?) exception_function =
     try Some (exception_function ()) with
-    | _ -> None
+    | exn when GobExn.catch_all_filter exn -> None (* TODO: don't catch all *)
   let (~!) value_option =
     match value_option with
     | Some value -> value
diff --git a/src/util/apron/relationPrecCompareUtil.apron.ml b/src/util/apron/relationPrecCompareUtil.apron.ml
index 15b59c2e22..f820081547 100644
--- a/src/util/apron/relationPrecCompareUtil.apron.ml
+++ b/src/util/apron/relationPrecCompareUtil.apron.ml
@@ -1,4 +1,4 @@
-(** {!RelationPriv} precison comparison. *)
+(** {!RelationPriv} precision comparison. *)
 
 open PrecCompareUtil
 
diff --git a/src/util/backtrace/goblint_backtrace.ml b/src/util/backtrace/goblint_backtrace.ml
index a4355ac921..29198c27ea 100644
--- a/src/util/backtrace/goblint_backtrace.ml
+++ b/src/util/backtrace/goblint_backtrace.ml
@@ -47,7 +47,7 @@ let apply_mark_printers m =
       match f m with
       | Some s -> Some s
       | None
-      | exception _ -> None
+      | exception _ -> None (* TODO: do not catch all? Stdlib.Printexc also catches all *)
     ) !mark_printers
 
 let mark_to_string_default m =
diff --git a/src/util/gobExn.ml b/src/util/gobExn.ml
new file mode 100644
index 0000000000..f14df57c2d
--- /dev/null
+++ b/src/util/gobExn.ml
@@ -0,0 +1,15 @@
+(** Exception utilities. *)
+
+(** Filter for catching and swallowing all exceptions.
+    This avoids swallowing some very important exceptions that shouldn't be caught to begin with. *)
+let catch_all_filter = function
+  | Out_of_memory
+  | Stack_overflow -> false (* OCaml runtime *)
+  | Assert_failure _
+  | Match_failure _
+  | Undefined_recursive_module _ -> false (* Broken program *)
+  | Sys.Break -> false (* Ctrl-C *)
+  | Timeout.Timeout -> false (* Goblint timeout *)
+  | _ -> true
+
+(* TODO: can't move to goblint.std because Timeout.Timeout *)
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 02cce23f42..e433c34b4a 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -292,7 +292,7 @@ let fixedLoopSize loopStatement func =
         Logs.debug "iterations:";
         Logs.debug "%d" s';
         Some s'
-      with  _ -> Logs.debug "iterations too big for integer"; None
+      with Z.Overflow -> Logs.debug "iterations too big for integer"; None
 
 
 class arrayVisitor = object
diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml
index a04e395e83..2386367967 100644
--- a/src/util/precCompare.ml
+++ b/src/util/precCompare.ml
@@ -1,4 +1,4 @@
-(** Precison comparison. *)
+(** Precision comparison. *)
 
 open Batteries
 module Pretty = GoblintCil.Pretty
@@ -97,14 +97,30 @@ struct
   let load filename =
     let f = open_in_bin filename in
     let dump: dump = Marshal.from_channel f in
-    let dump: result = {name = dump.name; results = unmarshal dump.marshalled } in
+    let dump: result = {name = dump.name; results = unmarshal dump.marshalled; disregard = dump.disregard } in
     close_in_noerr f;
     dump
 
   module CompareDump = MakeHashtbl (Key) (Dom) (RH)
 
-  let compare_dumps ({name = name1; results = lvh1}: result) ({name = name2; results = lvh2}: result) =
-    CompareDump.compare ~verbose:true ~name1 lvh1 ~name2 lvh2
+  let comparisons = ref []
+
+  let compare_dumps ({name = name1; results = lvh1; disregard = disregard1}: result) ({name = name2; results = lvh2; disregard = disregard2}: result) =
+    let (lvh1:Dom.t RH.t) =
+      match disregard1, disregard2 with
+      | Some disregard1, Some disregard2 ->
+        RH.filter_map (fun k v -> if Hashtbl.mem disregard1 (Key.to_location k) || Hashtbl.mem disregard2 (Key.to_location k) then None else Some v) lvh1
+      | _ -> lvh1
+    in
+    let (lvh2:Dom.t RH.t) =
+      match disregard1, disregard2 with
+      | Some disregard1, Some disregard2 ->
+        RH.filter_map (fun k v -> if Hashtbl.mem disregard1 (Key.to_location k) || Hashtbl.mem disregard2 (Key.to_location k) then None else Some v) lvh2
+      | _ -> lvh2
+    in
+    let (c, d) = CompareDump.compare ~verbose:true ~name1 lvh1 ~name2 lvh2 in
+    comparisons := (name1, name2, c, d) :: !comparisons;
+    (c, d)
 
   let count_locations (dumps: result list) =
     let module LH = Hashtbl.Make (CilType.Location) in
@@ -118,8 +134,50 @@ struct
       ) dumps;
     (LH.length locations, RH.length location_vars)
 
+  let group () =
+    let new_bucket_id = ref 0 in
+    let equality_buckets = Hashtbl.create 113 in
+    let sorted = List.sort (fun (n1, _, _, _) (n2, _, _, _) -> String.compare n1 n2) !comparisons in
+    List.iter (fun (name1, name2, (c:Comparison.t), _) ->
+        (if not (Hashtbl.mem equality_buckets name1) then
+           (* Make its own bucket if it does not appear yet *)
+           (let bucket_id = !new_bucket_id in
+            incr new_bucket_id;
+            Hashtbl.add equality_buckets name1 bucket_id));
+        if c.more_precise = 0 && c.less_precise = 0 && c.incomparable = 0 then
+          Hashtbl.replace equality_buckets name2 (Hashtbl.find equality_buckets name1)
+        else
+          ()
+      ) sorted;
+    let bindings = Hashtbl.bindings equality_buckets in
+    let buckets = List.group (fun (_, b) (_, b') -> compare b b') bindings in
+    List.iter (fun bucket ->
+        Logs.result "Bucket %d:" (snd (List.hd bucket));
+        List.iter (fun (name, _) -> Logs.result "  %s" name) bucket
+      ) buckets;
+    let comparison_produced = Hashtbl.create 113 in
+    List.iter (fun (name1, name2, c,d) ->
+        let bucket1 = Hashtbl.find equality_buckets name1 in
+        let bucket2 = Hashtbl.find equality_buckets name2 in
+        if bucket1 = bucket2 then
+          ()
+        else
+          begin
+            let comp_tumple = (min bucket1 bucket2, max bucket1 bucket2) in
+            if not @@ Hashtbl.mem comparison_produced comp_tumple then
+              begin
+                Hashtbl.add comparison_produced comp_tumple ();
+                Logs.result "Comparison between bucket %d and %d: %t" (fst comp_tumple) (snd comp_tumple) (fun () -> d);
+              end
+          end
+      ) sorted;
+    ()
+
   let main () =
     Util.init ();
+    GobConfig.set_bool "dbg.full-output" true;
+    (* Do not colorize stderr output *)
+    AnsiColors.stderr := false;
     let filenames = List.tl (Array.to_list Sys.argv) in
     let dumps = List.map load filenames in
     let (locations_count, location_vars_count) = count_locations dumps in
@@ -131,5 +189,6 @@ struct
     |> List.map (uncurry compare_dumps)
     |> List.iter (fun (_, msg) -> Logs.result "%t" (fun () -> msg));
     Logs.newline ();
-    Logs.result "Total locations: %d\nTotal %s: %d" locations_count (Key.name ()) location_vars_count
+    Logs.result "Total locations: %d\nTotal %s: %d" locations_count (Key.name ()) location_vars_count;
+    group ()
 end
diff --git a/src/util/precCompareUtil.ml b/src/util/precCompareUtil.ml
index e00447fd60..fd8f96fbb7 100644
--- a/src/util/precCompareUtil.ml
+++ b/src/util/precCompareUtil.ml
@@ -13,11 +13,13 @@ end
 type 'a dump_gen = {
   name: string;
   marshalled: 'a;
+  disregard: (GoblintCil.location,unit) Hashtbl.t option
 }
 
 type 'a result_gen = {
   name: string;
   results: 'a;
+  disregard: (GoblintCil.location,unit) Hashtbl.t option
 }
 
 module type R =
@@ -28,10 +30,10 @@ sig
   (** Module for the result hash map *)
   module RH : Hashtbl.S with type key = Key.t
 
-  (** Type to which the result hashmap is actually convered before storing it to disc *)
+  (** Type to which the result hashmap is actually converted before storing it to disc *)
   type marshal
 
-  (** Wrapper of marhshal type, together with a name for the analysis + privatization combination *)
+  (** Wrapper of marshal type, together with a name for the analysis + privatization combination *)
   type dump = marshal dump_gen
 
   (** Type of the actually usable result. To be obtained from the dump via the unmarshal function below  *)
diff --git a/src/util/privPrecCompareUtil.ml b/src/util/privPrecCompareUtil.ml
index 8f0a24db3b..0e857c9063 100644
--- a/src/util/privPrecCompareUtil.ml
+++ b/src/util/privPrecCompareUtil.ml
@@ -1,4 +1,4 @@
-(** {!BasePriv} precison comparison. *)
+(** {!BasePriv} precision comparison. *)
 
 open GoblintCil
 open PrecCompareUtil
diff --git a/src/util/server.ml b/src/util/server.ml
index 1b67dbf8a3..80ddc81d31 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -338,7 +338,7 @@ let () =
       try
         GobConfig.set_auto conf (Yojson.Safe.to_string json);
         Maingoblint.handle_options ();
-      with exn -> (* TODO: Be more specific in what we catch. *)
+      with exn when GobExn.catch_all_filter exn -> (* TODO: Be more specific in what we catch. *)
         Response.Error.(raise (of_exn exn))
   end);
 
@@ -350,7 +350,7 @@ let () =
       try
         GobConfig.set_conf Options.defaults;
         Maingoblint.parse_arguments ();
-      with exn -> (* TODO: Be more specific in what we catch. *)
+      with exn when GobExn.catch_all_filter exn -> (* TODO: Be more specific in what we catch. *)
         Response.Error.(raise (of_exn exn))
   end);
 
@@ -362,7 +362,7 @@ let () =
       try
         GobConfig.merge json;
         Maingoblint.handle_options ();
-      with exn -> (* TODO: Be more specific in what we catch. *)
+      with exn when GobExn.catch_all_filter exn -> (* TODO: Be more specific in what we catch. *)
         Response.Error.(raise (of_exn exn))
   end);
 
@@ -374,7 +374,7 @@ let () =
       try
         GobConfig.merge_file (Fpath.v fname);
         Maingoblint.handle_options ();
-      with exn -> (* TODO: Be more specific in what we catch. *)
+      with exn when GobExn.catch_all_filter exn -> (* TODO: Be more specific in what we catch. *)
         Response.Error.(raise (of_exn exn))
   end);
 
diff --git a/src/util/std/gobZ.ml b/src/util/std/gobZ.ml
index 02110ac8bb..72f4b3bd74 100644
--- a/src/util/std/gobZ.ml
+++ b/src/util/std/gobZ.ml
@@ -1,4 +1,4 @@
-type t = Z.t
+type t = Z.t [@@deriving eq, ord, hash]
 
 let to_yojson z =
   `Intlit (Z.to_string z)
diff --git a/src/util/timeout.ml b/src/util/timeout.ml
index ce1352ef67..99fca2adcc 100644
--- a/src/util/timeout.ml
+++ b/src/util/timeout.ml
@@ -4,7 +4,7 @@ module Unix = struct
   let timeout f arg tsecs timeout_fn =
     let oldsig = Sys.signal Sys.sigprof (Sys.Signal_handle (fun _ -> timeout_fn ())) in
     (* https://ocaml.org/api/Unix.html#TYPEinterval_timer ITIMER_PROF is user (ITIMER_VIRTUAL) + system time; sends sigprof *)
-    ignore Unix.(setitimer ITIMER_PROF { it_interval = 0.0; it_value = tsecs });
+    ignore Unix.(setitimer ITIMER_PROF { it_interval = 1.0; it_value = tsecs }); (* Keep signaling timeout with 1s interval, so if we happen to be inside a catch-all exception handler (which we shouldn't have to begin with...) then we'll have more opportinities for timing out. *)
     let res = f arg in
     Sys.set_signal Sys.sigprof oldsig;
     res
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 42254f30de..aab006c610 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -605,7 +605,7 @@ struct
           let result = LvarS.fold (fun ((n, _) as lvar) (acc: VR.t) ->
               let fundec = Node.find_fundec n in
 
-              let result: VR.result = match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
+              let result: VR.result = match InvariantParser.parse_cil ~check:false inv_parser ~fundec ~loc inv_cabs with
                 | Ok inv_exp ->
                   let x = ask_local lvar (Queries.EvalInt inv_exp) in
                   if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *)
diff --git a/tests/regression/03-practical/33-axel.c b/tests/regression/03-practical/33-axel.c
new file mode 100644
index 0000000000..f8150a804f
--- /dev/null
+++ b/tests/regression/03-practical/33-axel.c
@@ -0,0 +1,20 @@
+// Should not crash (issue 1421)
+#include<pthread.h>
+struct a {
+  pthread_mutex_t b;
+};
+struct c {
+  struct a *conn;
+};
+
+int main() {
+  int x;
+  struct a str = {0};
+  struct c axel = {0};
+  axel.conn = &str;
+  pthread_mutex_t* ptr = &((axel.conn + 0)->b);
+  x = 4;
+  pthread_mutex_lock(ptr);
+  pthread_mutex_unlock(ptr);
+  pthread_mutex_lock(&((axel.conn + 0)->b));
+}
diff --git a/tests/regression/05-lval_ls/24-idxunknown_recursive.c b/tests/regression/05-lval_ls/24-idxunknown_recursive.c
new file mode 100644
index 0000000000..95e8bff798
--- /dev/null
+++ b/tests/regression/05-lval_ls/24-idxunknown_recursive.c
@@ -0,0 +1,38 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] pthreadMutexType
+_Bool __VERIFIER_nondet_bool();
+
+#define _GNU_SOURCE
+#include <pthread.h>
+
+int g;
+
+#ifdef __APPLE__
+pthread_mutex_t m[2] = {PTHREAD_RECURSIVE_MUTEX_INITIALIZER, PTHREAD_RECURSIVE_MUTEX_INITIALIZER};
+#else
+pthread_mutex_t m[2] = {PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP, PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP};
+#endif
+
+void *t_fun(void *arg) {
+  int i, j, k;
+  i = __VERIFIER_nondet_bool();
+  j = __VERIFIER_nondet_bool();
+  k = __VERIFIER_nondet_bool();
+
+  pthread_mutex_lock(&m[i]); // may lock m[1]
+  pthread_mutex_lock(&m[j]); // may lock m[1] recursively
+  pthread_mutex_lock(&m[0]); // must lock m[0]
+  pthread_mutex_unlock(&m[k]); // may unlock m[0]
+  // m[0] should not be in must-lockset here!
+  g++; // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  g++; // RACE!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}
diff --git a/tests/regression/05-lval_ls/25-idxunknown_recursive_2.c b/tests/regression/05-lval_ls/25-idxunknown_recursive_2.c
new file mode 100644
index 0000000000..47ea1ce0a7
--- /dev/null
+++ b/tests/regression/05-lval_ls/25-idxunknown_recursive_2.c
@@ -0,0 +1,36 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] pthreadMutexType
+_Bool __VERIFIER_nondet_bool();
+
+#define _GNU_SOURCE
+#include <pthread.h>
+
+int g;
+
+#ifdef __APPLE__
+pthread_mutex_t m[2] = {PTHREAD_RECURSIVE_MUTEX_INITIALIZER, PTHREAD_RECURSIVE_MUTEX_INITIALIZER};
+#else
+pthread_mutex_t m[2] = {PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP, PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP};
+#endif
+
+void *t_fun(void *arg) {
+  int i;
+  i = __VERIFIER_nondet_bool();
+
+  pthread_mutex_lock(&m[0]); // must lock m[0]
+  pthread_mutex_unlock(&m[i]); // may unlock m[0]
+  pthread_mutex_lock(&m[0]); // must lock m[0]
+  pthread_mutex_unlock(&m[0]); // must unlock m[0]
+  // m[0] should not be in must-lockset here!
+  g++; // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  g++; // RACE!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}
diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t
index 90f0661f67..ca2e219b05 100644
--- a/tests/regression/06-symbeq/21-mult_accs_rc.t
+++ b/tests/regression/06-symbeq/21-mult_accs_rc.t
@@ -10,7 +10,10 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Race] Memory location (struct s).data (race with conf. 100):
     write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
     write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
-  [Warning][Unknown] unlocking mutex (NULL) which may not be held (21-mult_accs_rc.c:35:3-35:26)
+  [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32)
+  [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:17:3-17:32)
+  [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:33:3-33:24)
+  [Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:35:3-35:26)
   [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14)
@@ -26,7 +29,10 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9)
   [Success][Race] Memory location (struct s).data (safe):
     write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
-  [Warning][Unknown] unlocking mutex (NULL) which may not be held (21-mult_accs_rc.c:35:3-35:26)
+  [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32)
+  [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:17:3-17:32)
+  [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:33:3-33:24)
+  [Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:35:3-35:26)
   [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:35:3-35:26)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:13:3-13:14)
   [Error][Imprecise][Unsound] Function definition missing for get_s (21-mult_accs_rc.c:15:3-15:14)
diff --git a/tests/regression/13-privatized/80-treachery-and-lies.c b/tests/regression/13-privatized/80-treachery-and-lies.c
new file mode 100644
index 0000000000..7670bad8f8
--- /dev/null
+++ b/tests/regression/13-privatized/80-treachery-and-lies.c
@@ -0,0 +1,54 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+struct a *ptr;
+struct a *straightandnarrow;
+
+pthread_mutex_t m;
+
+void doit() {
+  void *newa = malloc(sizeof(struct a));
+
+  pthread_mutex_lock(&m);
+  ptr->b = 5;
+
+  int fear = straightandnarrow->b;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  ptr = newa;
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = straightandnarrow->b;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  doit();
+  return NULL;
+}
+
+int main() {
+    int top;
+    struct a other = { 0 };
+    struct a other2 = { 42 };
+    if(top) {
+      ptr = &other;
+    } else {
+      ptr = &other2;
+    }
+
+    straightandnarrow = &other;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c b/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c
new file mode 100644
index 0000000000..d6a33dece4
--- /dev/null
+++ b/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c
@@ -0,0 +1,55 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 5 or 0, depending on which one the pointer points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    int da_oane = 0;
+    int de_andre = 42;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/82-well-laid-out-plans.c b/tests/regression/13-privatized/82-well-laid-out-plans.c
new file mode 100644
index 0000000000..8eb1cc11e1
--- /dev/null
+++ b/tests/regression/13-privatized/82-well-laid-out-plans.c
@@ -0,0 +1,56 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones.
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+int da_oane = 0;
+int de_andre = 42;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 0 or 5, depending on which one ptr points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  // This works
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/83-treachery-and-lies-write.c b/tests/regression/13-privatized/83-treachery-and-lies-write.c
new file mode 100644
index 0000000000..f317100825
--- /dev/null
+++ b/tests/regression/13-privatized/83-treachery-and-lies-write.c
@@ -0,0 +1,54 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+struct a *ptr;
+struct a *straightandnarrow;
+
+pthread_mutex_t m;
+
+void doit() {
+  void *newa = malloc(sizeof(struct a));
+
+  pthread_mutex_lock(&m);
+  ptr->b = 5;
+
+  int fear = straightandnarrow->b;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  ptr = newa;
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = straightandnarrow->b;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  doit();
+  return NULL;
+}
+
+int main() {
+    int top;
+    struct a other = { 0 };
+    struct a other2 = { 42 };
+    if(top) {
+      ptr = &other;
+    } else {
+      ptr = &other2;
+    }
+
+    straightandnarrow = &other;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c b/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c
new file mode 100644
index 0000000000..c62e49ba69
--- /dev/null
+++ b/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c
@@ -0,0 +1,55 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 5 or 0, depending on which one the pointer points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    int da_oane = 0;
+    int de_andre = 42;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/85-well-laid-out-plans-write.c b/tests/regression/13-privatized/85-well-laid-out-plans-write.c
new file mode 100644
index 0000000000..246804f82e
--- /dev/null
+++ b/tests/regression/13-privatized/85-well-laid-out-plans-write.c
@@ -0,0 +1,56 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones.
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+int da_oane = 0;
+int de_andre = 42;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 0 or 5, depending on which one ptr points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  // This works
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/86-treachery-and-lies-lock.c b/tests/regression/13-privatized/86-treachery-and-lies-lock.c
new file mode 100644
index 0000000000..aa21f89ea7
--- /dev/null
+++ b/tests/regression/13-privatized/86-treachery-and-lies-lock.c
@@ -0,0 +1,54 @@
+// PARAM: --set ana.base.privatization lock --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+struct a *ptr;
+struct a *straightandnarrow;
+
+pthread_mutex_t m;
+
+void doit() {
+  void *newa = malloc(sizeof(struct a));
+
+  pthread_mutex_lock(&m);
+  ptr->b = 5;
+
+  int fear = straightandnarrow->b;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  ptr = newa;
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = straightandnarrow->b;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  doit();
+  return NULL;
+}
+
+int main() {
+    int top;
+    struct a other = { 0 };
+    struct a other2 = { 42 };
+    if(top) {
+      ptr = &other;
+    } else {
+      ptr = &other2;
+    }
+
+    straightandnarrow = &other;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c b/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c
new file mode 100644
index 0000000000..02f5b721ba
--- /dev/null
+++ b/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c
@@ -0,0 +1,55 @@
+// PARAM: --set ana.base.privatization lock --enable ana.int.enums
+// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 5 or 0, depending on which one the pointer points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    int da_oane = 0;
+    int de_andre = 42;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/88-well-laid-out-plans-lock.c b/tests/regression/13-privatized/88-well-laid-out-plans-lock.c
new file mode 100644
index 0000000000..9caae2daf1
--- /dev/null
+++ b/tests/regression/13-privatized/88-well-laid-out-plans-lock.c
@@ -0,0 +1,56 @@
+// PARAM: --set ana.base.privatization lock --enable ana.int.enums
+// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones.
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+int da_oane = 0;
+int de_andre = 42;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 0 or 5, depending on which one ptr points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  // This works
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}
diff --git a/tests/regression/13-privatized/89-write-lacking-precision.c b/tests/regression/13-privatized/89-write-lacking-precision.c
new file mode 100644
index 0000000000..75ee78974d
--- /dev/null
+++ b/tests/regression/13-privatized/89-write-lacking-precision.c
@@ -0,0 +1,30 @@
+// PARAM: --set ana.base.privatization write
+#include<pthread.h>
+struct a {
+  char* b;
+};
+
+struct a *c;
+struct a h = {""};
+struct a i = {"string"};
+
+void* d(void* args) {
+  struct a r;
+  if (c->b) {
+    __goblint_check(strlen(h.b) == 0); // Should also work for write!
+  }
+}
+
+int main() {
+  int top;
+
+  if(top) {
+    c = &h;
+  } else {
+    c = &i;
+  }
+
+  pthread_t t;
+  pthread_create(&t, 0, d, 0);
+  return 0;
+}
diff --git a/tests/regression/13-privatized/90-union.c b/tests/regression/13-privatized/90-union.c
new file mode 100644
index 0000000000..df5990d7a4
--- /dev/null
+++ b/tests/regression/13-privatized/90-union.c
@@ -0,0 +1,29 @@
+// PARAM: --set ana.base.privatization write
+#include<pthread.h>
+#include<stdlib.h>
+#include<string.h>
+union g {
+  int h;
+  int i;
+};
+struct j {
+  union g data;
+};
+
+
+void* af(void* arg) {
+  int top;
+  struct j* jptr = (struct j*) malloc(sizeof(struct j));
+  memset(jptr, 0, sizeof(struct j));
+
+  while (top) {
+    if (jptr->data.i);
+
+    __goblint_check(jptr->data.i == 0); // Should alo work for write!
+  }
+}
+
+void main() {
+  pthread_t ah;
+  pthread_create(&ah, 0, af, 0);
+}
diff --git a/tests/regression/13-privatized/91-union-direct.c b/tests/regression/13-privatized/91-union-direct.c
new file mode 100644
index 0000000000..bf1127d389
--- /dev/null
+++ b/tests/regression/13-privatized/91-union-direct.c
@@ -0,0 +1,26 @@
+// PARAM: --set ana.base.privatization write
+#include<pthread.h>
+#include<stdlib.h>
+#include<string.h>
+union g {
+  int h;
+  int i;
+};
+
+void* af(void* arg) {
+  // Go MT
+}
+
+void main() {
+  pthread_t ah;
+  pthread_create(&ah, 0, af, 0);
+
+  int top;
+  union g* jptr = (union g*) malloc(sizeof(union g));
+  memset(jptr, 0, sizeof(union g));
+
+  while (top) {
+    if (jptr->i);
+    __goblint_check(jptr->i == 0); // Should alo work for write!
+  }
+}
diff --git a/tests/regression/13-privatized/92-widening-effect.c b/tests/regression/13-privatized/92-widening-effect.c
new file mode 100644
index 0000000000..c5faa9fa21
--- /dev/null
+++ b/tests/regression/13-privatized/92-widening-effect.c
@@ -0,0 +1,32 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.interval --set solvers.td3.side_widen never
+// For write side_widen never is needed, for protection it is not.
+// Alternatively, one can --disable ana.int.def_exc or  --set ana.int.refinement once
+#include <pthread.h>
+int occupied;
+pthread_mutex_t mtx;
+
+
+void* thread(void* arg) {
+  pthread_mutex_lock(&mtx);
+  if(occupied < 1) {
+    occupied++;
+    pthread_mutex_unlock(&mtx);
+  } else {
+    pthread_mutex_unlock(&mtx);
+  }
+ }
+
+int main() {
+  pthread_t worker;
+
+  pthread_create(&worker, 0, &thread, 0);
+
+  pthread_mutex_lock(&mtx);
+  occupied = 0;
+  pthread_mutex_unlock(&mtx);
+
+  pthread_mutex_lock(&mtx);
+  __goblint_check(occupied >= 0);
+   pthread_mutex_lock(&mtx);
+  return 0;
+}
diff --git a/tests/regression/13-privatized/93-unlock-idx-ambiguous.c b/tests/regression/13-privatized/93-unlock-idx-ambiguous.c
new file mode 100644
index 0000000000..081302514b
--- /dev/null
+++ b/tests/regression/13-privatized/93-unlock-idx-ambiguous.c
@@ -0,0 +1,27 @@
+// PARAM: --set ana.base.privatization protection --enable ana.sv-comp.functions
+#include <pthread.h>
+#include <goblint.h>
+extern _Bool __VERIFIER_nondet_bool();
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  pthread_mutex_lock(&m[1]); // so we're unlocking a mutex we definitely hold
+  g++;
+  int r = __VERIFIER_nondet_bool();
+  pthread_mutex_unlock(&m[r]); // TODO NOWARN (definitely held either way)
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}
diff --git a/tests/regression/13-privatized/93-unlock-idx-ambiguous.t b/tests/regression/13-privatized/93-unlock-idx-ambiguous.t
new file mode 100644
index 0000000000..8f24d728bf
--- /dev/null
+++ b/tests/regression/13-privatized/93-unlock-idx-ambiguous.t
@@ -0,0 +1,65 @@
+  $ goblint --set ana.base.privatization protection --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mutex-meet --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization lock --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization write --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mine-nothread --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
diff --git a/tests/regression/13-privatized/94-unlock-unknown.c b/tests/regression/13-privatized/94-unlock-unknown.c
new file mode 100644
index 0000000000..0897c38de8
--- /dev/null
+++ b/tests/regression/13-privatized/94-unlock-unknown.c
@@ -0,0 +1,25 @@
+// PARAM: --set ana.base.privatization protection --enable ana.sv-comp.functions
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  g++;
+  pthread_mutex_t *r; // rand
+  pthread_mutex_unlock(r);
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}
diff --git a/tests/regression/13-privatized/94-unlock-unknown.t b/tests/regression/13-privatized/94-unlock-unknown.t
new file mode 100644
index 0000000000..cc0aa921fe
--- /dev/null
+++ b/tests/regression/13-privatized/94-unlock-unknown.t
@@ -0,0 +1,70 @@
+  $ goblint --set ana.base.privatization protection --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mutex-meet --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization lock --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization write --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mine-nothread --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
diff --git a/tests/regression/13-privatized/95-mm-calloc.c b/tests/regression/13-privatized/95-mm-calloc.c
new file mode 100644
index 0000000000..60a88379fc
--- /dev/null
+++ b/tests/regression/13-privatized/95-mm-calloc.c
@@ -0,0 +1,28 @@
+// PARAM: --set ana.base.privatization mutex-meet
+#include<pthread.h>
+#include<stdlib.h>
+#include<stdio.h>
+struct a {
+  void (*b)();
+};
+
+int g = 0;
+
+struct a* t;
+void m() {
+  // Reachable!
+  g = 1;
+}
+
+void* j(void* arg) {};
+
+void main() {
+  pthread_t tid;
+  pthread_create(&tid, 0, j, NULL);
+  t = calloc(1, sizeof(struct a));
+  t->b = &m;
+  struct a r = *t;
+  r.b();
+
+  __goblint_check(g ==0); //UNKNOWN!
+}
diff --git a/tests/regression/13-privatized/dune b/tests/regression/13-privatized/dune
new file mode 100644
index 0000000000..23c0dd3290
--- /dev/null
+++ b/tests/regression/13-privatized/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))
diff --git a/tests/regression/27-inv_invariants/22-meet-ptrs.c b/tests/regression/27-inv_invariants/22-meet-ptrs.c
new file mode 100644
index 0000000000..33adfa879f
--- /dev/null
+++ b/tests/regression/27-inv_invariants/22-meet-ptrs.c
@@ -0,0 +1,24 @@
+//PARAM:  --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+
+int main() {
+   int arr[20];
+
+   int top;
+
+   int i = 2;
+   if(top) {
+      i = 8;
+   }
+
+   int* imprecise = &arr[i];
+
+   if(imprecise == &arr[2]) {
+      __goblint_check(imprecise == &arr[2]);
+   }
+
+   return 0;
+}
diff --git a/tests/regression/46-apron2/84-relation-extern.c b/tests/regression/46-apron2/84-relation-extern.c
new file mode 100644
index 0000000000..ffd8f9e2ce
--- /dev/null
+++ b/tests/regression/46-apron2/84-relation-extern.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron
+#include <pthread.h>
+#include <goblint.h>
+
+extern int g;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  if (g) // NOWARN
+    __goblint_check(1); // reachable
+  else
+    __goblint_check(1); // reachable
+
+  return 0;
+}
diff --git a/tests/regression/46-apron2/85-fix.c b/tests/regression/46-apron2/85-fix.c
new file mode 100644
index 0000000000..e0d7e8964b
--- /dev/null
+++ b/tests/regression/46-apron2/85-fix.c
@@ -0,0 +1,13 @@
+// SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none
+#include<pthread.h>
+
+int main() {
+  int d = 1;
+  while (d < 6) {
+    if (0)
+      return 0; //FIXPOINT: Earlier this fixpoint was not reached here
+    d++;
+  }
+
+  return 0;
+}
diff --git a/tests/regression/46-apron2/86-escape-cluster12.c b/tests/regression/46-apron2/86-escape-cluster12.c
new file mode 100644
index 0000000000..283e45b728
--- /dev/null
+++ b/tests/regression/46-apron2/86-escape-cluster12.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12
+#include<pthread.h>
+#include<goblint.h>
+void *a;
+
+void* nothing(void* arg) {
+  // Go multithreaded!
+}
+
+void main() {
+  pthread_t t;
+  pthread_create(&t, 0, nothing, 0);
+
+  int d = 5;
+  a = &d;
+
+  if (0)
+    ;
+
+  __goblint_check(1); // Should be reachable!
+}
diff --git a/tests/regression/46-apron2/87-unlock-idx-ambiguous.c b/tests/regression/46-apron2/87-unlock-idx-ambiguous.c
new file mode 100644
index 0000000000..ff6461217e
--- /dev/null
+++ b/tests/regression/46-apron2/87-unlock-idx-ambiguous.c
@@ -0,0 +1,28 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag
+// TODO: why nonterm without threadflag path-sens?
+#include <pthread.h>
+#include <goblint.h>
+extern _Bool __VERIFIER_nondet_bool();
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  pthread_mutex_lock(&m[1]); // so we're unlocking a mutex we definitely hold
+  g++;
+  int r = __VERIFIER_nondet_bool();
+  pthread_mutex_unlock(&m[r]); // TODO NOWARN (definitely held either way)
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/87-unlock-idx-ambiguous.t b/tests/regression/46-apron2/87-unlock-idx-ambiguous.t
new file mode 100644
index 0000000000..abbdd74f00
--- /dev/null
+++ b/tests/regression/46-apron2/87-unlock-idx-ambiguous.t
@@ -0,0 +1,39 @@
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-cluster12 --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
diff --git a/tests/regression/46-apron2/88-unlock-unknown.c b/tests/regression/46-apron2/88-unlock-unknown.c
new file mode 100644
index 0000000000..dbdc4b9f77
--- /dev/null
+++ b/tests/regression/46-apron2/88-unlock-unknown.c
@@ -0,0 +1,25 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  g++;
+  pthread_mutex_t *r; // rand
+  pthread_mutex_unlock(r);
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/88-unlock-unknown.t b/tests/regression/46-apron2/88-unlock-unknown.t
new file mode 100644
index 0000000000..35e4ec4503
--- /dev/null
+++ b/tests/regression/46-apron2/88-unlock-unknown.t
@@ -0,0 +1,42 @@
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions 88-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (88-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (88-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (88-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 88-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (88-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (88-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (88-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-cluster12 --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 88-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (88-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (88-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (88-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
diff --git a/tests/regression/46-apron2/89-malloc.c b/tests/regression/46-apron2/89-malloc.c
new file mode 100644
index 0000000000..8780568748
--- /dev/null
+++ b/tests/regression/46-apron2/89-malloc.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}
diff --git a/tests/regression/46-apron2/90-malloc2.c b/tests/regression/46-apron2/90-malloc2.c
new file mode 100644
index 0000000000..36696956e7
--- /dev/null
+++ b/tests/regression/46-apron2/90-malloc2.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag  --set ana.relation.privatization mutex-meet-tid --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}
diff --git a/tests/regression/46-apron2/91-malloc-atomic.c b/tests/regression/46-apron2/91-malloc-atomic.c
new file mode 100644
index 0000000000..b2f057f6a4
--- /dev/null
+++ b/tests/regression/46-apron2/91-malloc-atomic.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet-atomic --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}
diff --git a/tests/regression/46-apron2/92-wtf2.c b/tests/regression/46-apron2/92-wtf2.c
new file mode 100644
index 0000000000..d3cc38ac57
--- /dev/null
+++ b/tests/regression/46-apron2/92-wtf2.c
@@ -0,0 +1,19 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --sets ana.apron.domain interval
+// Checks that branching over extern or volatile variables does not yield to both branches being dead.
+// This fails unless exp.hide-std-globals is deactivated (which it is by default on this branch)
+#include<pthread.h>
+extern int optind;
+
+void* a(void* arg) {
+  // Just go multi-threaded
+}
+
+void main() {
+  pthread_t t;
+
+  pthread_create(&t, 0, a, 0);
+  if (optind)
+    ;
+
+  // __goblint_check(1); // Reachable
+}
diff --git a/tests/regression/46-apron2/93-wtf.c b/tests/regression/46-apron2/93-wtf.c
new file mode 100644
index 0000000000..97ef8d3097
--- /dev/null
+++ b/tests/regression/46-apron2/93-wtf.c
@@ -0,0 +1,26 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --sets ana.apron.domain interval
+// Checks that branching over extern or volatile variables does not yield to both branches being dead.
+#include<pthread.h>
+#include<goblint.h>
+extern int d;
+volatile int v;
+
+void* g(void* arg) {
+  // Just go multithreaded!
+}
+
+void main() {
+  pthread_t t;
+  pthread_create(&t, 0, g, 0);
+
+  if(v)
+  ;
+
+  __goblint_check(1); // Reachable
+
+  if (d)
+  ;
+
+  __goblint_check(1); // Reachable
+
+}
diff --git a/tests/regression/46-apron2/94-threadflag-ctx-sens.c b/tests/regression/46-apron2/94-threadflag-ctx-sens.c
new file mode 100644
index 0000000000..10fc5f8d1e
--- /dev/null
+++ b/tests/regression/46-apron2/94-threadflag-ctx-sens.c
@@ -0,0 +1,27 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet
+// NOTIMEOUT
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void fn() {
+  // Just do nothing
+  return;
+}
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m);
+  g = g+1;
+  fn();
+  pthread_mutex_unlock(&m);
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  return 0;
+}
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.c b/tests/regression/46-apron2/95-witness-mm-escape.c
new file mode 100644
index 0000000000..e6f2d5d429
--- /dev/null
+++ b/tests/regression/46-apron2/95-witness-mm-escape.c
@@ -0,0 +1,19 @@
+// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+#include <pthread.h>
+#include <goblint.h>
+
+int *b;
+pthread_mutex_t e;
+
+void main() {
+
+    int g = 8;
+    int a;
+    if(a) {
+        g = 10;
+    }
+
+    b = &g;
+
+    pthread_mutex_lock(&e);
+}
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t
new file mode 100644
index 0000000000..047cb15718
--- /dev/null
+++ b/tests/regression/46-apron2/95-witness-mm-escape.t
@@ -0,0 +1,29 @@
+  $ goblint --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml 95-witness-mm-escape.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Success][Witness] invariant confirmed: 0 <= g (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 0 <= *b (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: g <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: *b <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: -8LL + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483648LL + (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483638LL + (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483637LL - (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 10LL - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483647LL - (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483658LL + (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483657LL - (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: b == & g (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: g != 0 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: *b != 0 (95-witness-mm-escape.c:19:1)
+  [Info][Witness] witness validation summary:
+    confirmed: 30
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 30
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.yml b/tests/regression/46-apron2/95-witness-mm-escape.yml
new file mode 100644
index 0000000000..66715bd382
--- /dev/null
+++ b/tests/regression/46-apron2/95-witness-mm-escape.yml
@@ -0,0 +1,621 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: f88caf27-fbfe-4ce8-a15d-463646cca899
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 0 <= g
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 7949534c-6edd-4412-9778-fc58745e7cc5
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 0 <= *b
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: ffe5f8b3-569c-4d42-8e9b-21c48312e6ce
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: g <= 127
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: cad5c137-4373-4431-b8c8-c5d1e537a716
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: '*b <= 127'
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: aa21493b-1338-4004-90b7-046b9e826169
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: -8LL + (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: b640fdf6-abc8-45b9-ad4f-2695e0d66a3d
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 2147483648LL + (long long )a >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: ecc017f2-d045-45c7-a795-d3d16088368d
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483638LL + (long long )a) + (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 52ace953-715d-4d44-9c44-5b40c1124593
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483637LL - (long long )a) + (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 661e7eee-b5c0-4de3-89ed-369f6978ba28
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 10LL - (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 7878f84e-a951-4247-a196-97f9195cf2fb
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 2147483647LL - (long long )a >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: e80582ed-4527-4773-97fd-08631c673c21
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483658LL + (long long )a) - (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 49f62de7-3bfc-45ee-8709-0ff295f23b7a
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483657LL - (long long )a) - (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: cb86dd3a-2ff5-420b-8d49-42240a324a26
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: b == & g
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 2573f907-0386-4098-9b0c-7f1ec86d3f90
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: g != 0
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 15693293-61f1-431b-867e-86add36e4d80
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: '*b != 0'
+    type: assertion
+    format: C
+- entry_type: invariant_set
+  metadata:
+    format_version: "0.1"
+    uuid: 5f4a70a3-8b30-4b5a-a260-56bb341a6283
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 0 <= g
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 0 <= *b
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: g <= 127
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: '*b <= 127'
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: -8LL + (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 2147483648LL + (long long )a >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: (2147483638LL + (long long )a) + (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: (2147483637LL - (long long )a) + (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 10LL - (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 2147483647LL - (long long )a >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: (2147483658LL + (long long )a) - (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: (2147483657LL - (long long )a) - (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: b == & g
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: g != 0
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: '*b != 0'
+      format: c_expression
diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.c b/tests/regression/46-apron2/96-witness-mm-escape2.c
new file mode 100644
index 0000000000..2fa3530679
--- /dev/null
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.c
@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+#include<pthread.h>
+int *b;
+pthread_mutex_t e;
+
+void* other(void* arg) {
+    pthread_mutex_lock(&e);
+    *b = -100;
+    pthread_mutex_unlock(&e);
+
+    return NULL;
+}
+
+void main() {
+    pthread_t t;
+    pthread_create(&t, NULL, other, NULL);
+    int g = 8;
+
+    b = &g;
+
+    pthread_mutex_lock(&e);
+}
diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t
new file mode 100644
index 0000000000..e8e46edc06
--- /dev/null
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.t
@@ -0,0 +1,18 @@
+  $ goblint --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
+  [Info][Witness] witness generation summary:
+    total generation entries: 5
+
+  $ goblint --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
+  [Info][Witness] witness validation summary:
+    confirmed: 8
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 8
+  [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
+  [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)
diff --git a/tests/regression/46-apron2/97-issue-1511.c b/tests/regression/46-apron2/97-issue-1511.c
new file mode 100644
index 0000000000..d1f5aaed7c
--- /dev/null
+++ b/tests/regression/46-apron2/97-issue-1511.c
@@ -0,0 +1,17 @@
+#include<pthread.h>
+pthread_mutex_t c;
+int d, e, f;
+
+void b(void* arg);
+
+
+void main(int argc, char *argv) {
+  pthread_t t;
+
+  e = pthread_create(&t, 0, b, &f);
+
+  pthread_mutex_lock(&c);
+  d=0;
+  pthread_mutex_unlock(&c);
+  pthread_mutex_lock(&c);
+}
diff --git a/tests/regression/46-apron2/97-issue-1511.t b/tests/regression/46-apron2/97-issue-1511.t
new file mode 100644
index 0000000000..3bf5b41334
--- /dev/null
+++ b/tests/regression/46-apron2/97-issue-1511.t
@@ -0,0 +1,26 @@
+  $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 97-issue-1511.c --set witness.yaml.path 97-issue-1511.yml
+  [Info][Witness] witness generation summary:
+    total generation entries: 11
+  [Error][Imprecise][Unsound] Function definition missing
+
+  $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 97-issue-1511.yml 97-issue-1511.c
+  [Info][Witness] witness validation summary:
+    confirmed: 20
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 20
+  [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) - (long long )f >= 0LL (97-issue-1511.c:14:3)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )f >= 0LL (97-issue-1511.c:14:3)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )f >= 0LL (97-issue-1511.c:14:3)
+  [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) + (long long )f >= 0LL (97-issue-1511.c:14:3)
+  [Success][Witness] invariant confirmed: d == 0 (97-issue-1511.c:14:3)
+  [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) - (long long )f >= 0LL (97-issue-1511.c:17:1)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )f >= 0LL (97-issue-1511.c:17:1)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )f >= 0LL (97-issue-1511.c:17:1)
+  [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) + (long long )f >= 0LL (97-issue-1511.c:17:1)
+  [Success][Witness] invariant confirmed: d == 0 (97-issue-1511.c:17:1)
+  [Error][Imprecise][Unsound] Function definition missing
diff --git a/tests/regression/46-apron2/98-issue-1511b.c b/tests/regression/46-apron2/98-issue-1511b.c
new file mode 100644
index 0000000000..6ba233b61b
--- /dev/null
+++ b/tests/regression/46-apron2/98-issue-1511b.c
@@ -0,0 +1,32 @@
+#include<pthread.h>
+int d, j, k;
+
+pthread_mutex_t f;
+
+void nothing() {};
+void nothing2() {};
+
+int top() {
+  int top2;
+  return top2;
+}
+
+void main() {
+  d = top();
+  if (d) {
+    k = 1;
+    pthread_t tid;
+    pthread_create(&tid, 0, &nothing, NULL);
+    pthread_mutex_lock(&f);
+    j = 0; // To ensure something is published
+    pthread_mutex_unlock(&f);
+    pthread_mutex_lock(&f);
+
+    pthread_t tid2;
+    pthread_create(&tid2, 0, &nothing2, NULL);
+    float f = 8.0f;
+  } else {
+    pthread_t tid2;
+    pthread_create(&tid2, 0, &nothing2, NULL);
+  }
+}
diff --git a/tests/regression/46-apron2/98-issue-1511b.t b/tests/regression/46-apron2/98-issue-1511b.t
new file mode 100644
index 0000000000..8add2f3d1c
--- /dev/null
+++ b/tests/regression/46-apron2/98-issue-1511b.t
@@ -0,0 +1,40 @@
+  $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 98-issue-1511b.c --set witness.yaml.path 98-issue-1511b.yml
+  [Info][Witness] witness generation summary:
+    total generation entries: 27
+
+  $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 98-issue-1511b.yml 98-issue-1511b.c
+  [Info][Witness] witness validation summary:
+    confirmed: 52
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 52
+  [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:21:5)
+  [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:26:5)
+  [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:26:5)
diff --git a/tests/regression/46-apron2/dune b/tests/regression/46-apron2/dune
index ca3efec235..b957911e36 100644
--- a/tests/regression/46-apron2/dune
+++ b/tests/regression/46-apron2/dune
@@ -8,3 +8,8 @@
    (glob_files ??-*.c))
  (locks /update_suite)
  (action (chdir ../../.. (run %{update_suite} group apron2))))
+
+(cram
+ (alias runaprontest)
+ (enabled_if %{lib-available:apron})
+ (deps (glob_files *.c) (glob_files *.yml)))
diff --git a/tests/regression/62-abortUnless/05-apron-mutex-meet-abortUnless.c b/tests/regression/62-abortUnless/05-apron-mutex-meet-abortUnless.c
new file mode 100644
index 0000000000..e00c665056
--- /dev/null
+++ b/tests/regression/62-abortUnless/05-apron-mutex-meet-abortUnless.c
@@ -0,0 +1,39 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] abortUnless --set ana.path_sens[+] threadflag
+// Minimized SV-COMP version of our regression test
+// NOTIMEOUT
+#include <assert.h>
+#include <pthread.h>
+
+void reach_error() {
+  assert(0); // NOWARN
+}
+void __VERIFIER_assert(int cond) { // NOWARN
+  if(!(cond)) { ERROR: {reach_error();abort();} }
+}
+
+int glob1 = 5;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+void *t_fun(void *arg) {
+  int t;
+  pthread_mutex_lock(&mutex1);
+  t = glob1;
+  __VERIFIER_assert(t == 5); // NOWARN
+  glob1 = -10;
+  __VERIFIER_assert(glob1 == -10); // NOWARN
+  glob1 = t;
+  pthread_mutex_unlock(&mutex1);
+  return ((void *)0);
+}
+int main(void) {
+  pthread_t id;
+  __VERIFIER_assert(glob1 == 5); // NOWARN
+  pthread_create(&id, ((void *)0), t_fun, ((void *)0));
+  pthread_mutex_lock(&mutex1);
+  glob1++;
+  __VERIFIER_assert(glob1 == 6); // NOWARN
+  glob1--;
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, ((void *)0));
+  return 0;
+}
diff --git a/tests/regression/62-abortUnless/dune b/tests/regression/62-abortUnless/dune
new file mode 100644
index 0000000000..d0f8f1af41
--- /dev/null
+++ b/tests/regression/62-abortUnless/dune
@@ -0,0 +1,14 @@
+(rule
+ (aliases runtest runaprontest)
+ (enabled_if %{lib-available:apron})
+ (deps
+   (package goblint)
+   ../../../goblint ; update_suite calls local goblint
+   (:update_suite ../../../scripts/update_suite.rb)
+   (glob_files ??-*.c))
+ (locks /update_suite)
+ (action
+  (chdir ../../..
+   (progn
+     (run %{update_suite} apron-mutex-meet-abortUnless -q)))))
+