diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index d484075105..ee994274ca 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -43,6 +43,9 @@ jobs:
       - name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron -s
 
+      - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group apron-mukherjee -s
+
       - name: Build domaintest
         run: ./make.sh domaintest
 
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 3bddd4a454..67d0c00110 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -59,6 +59,10 @@ jobs:
         if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron -s
 
+      - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        if: ${{ matrix.apron }}
+        run: ruby scripts/update_suite.rb group apron-mukherjee -s
+
       - name: Build domaintest
         run: ./make.sh domaintest
 
diff --git a/conf/traces-rel.json b/conf/traces-rel.json
new file mode 100644
index 0000000000..e80e6e0026
--- /dev/null
+++ b/conf/traces-rel.json
@@ -0,0 +1,57 @@
+{
+  "ana": {
+    "int": {
+      "def_exc": true,
+      "interval": false,
+      "enums": true
+    },
+    "exp": {
+
+    }
+  },
+  "sem": {
+    "unknown_function": {
+      "invalidate": {
+        "globals": false
+      },
+      "spawn": true
+    },
+    "builtin_unreachable": {
+      "dead_code": true
+    }
+  },
+  "exp": {
+    "privatization": "mutex-meet",
+    "priv-distr-init": false,
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    },
+    "solver" : {
+      "td3": {
+        "side_widen" : "sides-pp"
+      }
+    }
+  },
+  "dbg" : {
+    "print_tids" : true,
+    "print_wpoints" : true,
+    "print_protection": true
+  }
+}
diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index bf93891fe5..7af2746ece 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -10,7 +10,6 @@ module SpecFunctor (AD: ApronDomain.S2) (Priv: ApronPriv.S) : Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
-
   let name () = "apron"
 
   module Priv = Priv(AD)
@@ -216,6 +215,7 @@ struct
 
   let return ctx e f =
     let st = ctx.local in
+    let ask = Analyses.ask_of_ctx ctx in
     let new_apr =
       if AD.type_tracked (Cilfacade.fundec_return_type f) then (
         let apr' = AD.add_vars st.apr [V.return] in
@@ -235,8 +235,15 @@ struct
       |> List.filter AD.varinfo_tracked
       |> List.map V.local
     in
+
     AD.remove_vars_with new_apr local_vars;
-    {st with apr = new_apr}
+    let st' = {st with apr = new_apr} in
+    begin match ThreadId.get_current ask with
+      | `Lifted tid when ThreadReturn.is_current ask ->
+        Priv.thread_return ask ctx.global ctx.sideg tid st'
+      | _ ->
+        st'
+    end
 
   let combine ctx r fe f args fc fun_st =
     let st = ctx.local in
@@ -288,6 +295,13 @@ struct
       unify_st
 
   let special ctx r f args =
+    let ask = Analyses.ask_of_ctx ctx in
+    let invalidate_one st lv =
+      assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
+          let apr' = AD.forget_vars st.apr [V.local v] in
+          assert_type_bounds apr' v (* re-establish type bounds after forget *)
+        )
+    in
     let st = ctx.local in
     match LibraryFunctions.classify f.vname args with
     (* TODO: assert handling from https://github.com/goblint/analyzer/pull/278 *)
@@ -295,6 +309,14 @@ struct
     | `Unknown "__goblint_check" -> st
     | `Unknown "__goblint_commit" -> st
     | `Unknown "__goblint_assert" -> st
+    | `ThreadJoin (id,retvar) ->
+      (* nothing to invalidate as only arguments that have their AddrOf taken may be invalidated *)
+      (
+        let st' = Priv.thread_join ask ctx.global id st in
+        match r with
+        | Some lv -> invalidate_one st' lv
+        | None -> st'
+      )
     | _ ->
       let ask = Analyses.ask_of_ctx ctx in
       let invalidate_one st lv =
diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
index 077728ddad..58bd2395d2 100644
--- a/src/analyses/apron/apronPriv.apron.ml
+++ b/src/analyses/apron/apronPriv.apron.ml
@@ -36,6 +36,9 @@ module type S =
     val enter_multithreaded: Q.ask -> (varinfo -> G.t) -> (varinfo -> G.t -> unit) -> apron_components_t -> apron_components_t
     val threadenter: Q.ask -> (varinfo -> G.t) -> apron_components_t -> apron_components_t
 
+    val thread_join: Q.ask -> (varinfo -> G.t) -> Cil.exp -> apron_components_t -> apron_components_t
+    val thread_return: Q.ask -> (varinfo -> G.t) -> (varinfo -> G.t -> unit) -> ThreadIdDomain.Thread.t -> apron_components_t -> apron_components_t
+
     val init: unit -> unit
     val finalize: unit -> unit
   end
@@ -56,6 +59,9 @@ struct
   let lock ask getg st m = st
   let unlock ask getg sideg st m = st
 
+  let thread_join ask getg exp st = st
+  let thread_return ask getg sideg tid st = st
+
   let sync ask getg sideg st reason = st
 
   let enter_multithreaded ask getg sideg st = st
@@ -259,6 +265,10 @@ struct
     let apr_local' = AD.meet apr_local (getg (global_varinfo ())) in
     {apr = apr_local'; priv = (p', w')}
 
+
+  let thread_join ask getg exp st = st
+  let thread_return ask getg sideg tid st = st
+
   let sync ask getg sideg (st: apron_components_t) reason =
     match reason with
     | `Return -> (* required for thread return *)
@@ -305,10 +315,32 @@ struct
   let finalize () = ()
 end
 
+module CommonPerMutex = functor(AD: ApronDomain.S2) ->
+struct
+  include Protection
+  module V = ApronDomain.V
+
+  let remove_globals_unprotected_after_unlock ask m oct =
+    let newly_unprot var = match V.find_metadata var with
+      | Some (Global g) -> is_protected_by ask m g && is_unprotected_without ask g m
+      | _ -> false
+    in
+    AD.remove_filter oct newly_unprot
+
+  let keep_only_protected_globals ask m oct =
+    let protected var = match V.find_metadata var with
+      | Some (Global g) -> is_protected_by ask m g
+      | _ -> false
+    in
+    AD.keep_filter oct protected
+
+  let finalize () = ProtectionLogging.dump ()
+end
+
 (** Per-mutex meet. *)
 module PerMutexMeetPriv : S = functor (AD: ApronDomain.S2) ->
 struct
-  open Protection
+  open CommonPerMutex(AD)
   open ExplicitMutexGlobals
 
   module D = Lattice.Unit
@@ -330,12 +362,7 @@ struct
   let get_m_with_mutex_inits ask getg m =
     let get_m = getg (mutex_addr_to_varinfo m) in
     let get_mutex_inits = getg (mutex_inits ()) in
-    let get_mutex_inits' = AD.keep_filter get_mutex_inits (fun var ->
-        match V.find_metadata var with
-        | Some (Global g) -> is_protected_by ask m g
-        | _ -> false
-      )
-    in
+    let get_mutex_inits' = keep_only_protected_globals ask m get_mutex_inits in
     AD.join get_m get_mutex_inits'
 
   let get_mutex_global_g_with_mutex_inits ask getg g =
@@ -387,32 +414,20 @@ struct
     let apr = st.apr in
     let get_m = get_m_with_mutex_inits ask getg m in
     (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let get_m = AD.keep_filter get_m (fun var ->
-        match V.find_metadata var with
-        | Some (Global g) -> is_protected_by ask m g
-        | _ -> false
-      )
-    in
+    let get_m = keep_only_protected_globals ask m get_m in
     let apr' = AD.meet apr get_m in
     {st with apr = apr'}
 
   let unlock ask getg sideg (st: apron_components_t) m: apron_components_t =
     let apr = st.apr in
-    let apr_side = AD.keep_filter apr (fun var ->
-        match V.find_metadata var with
-        | Some (Global g) -> is_protected_by ask m g
-        | _ -> false
-      )
-    in
+    let apr_side = keep_only_protected_globals ask m apr in
     sideg (mutex_addr_to_varinfo m) apr_side;
-    let apr_local = AD.remove_filter apr (fun var ->
-        match V.find_metadata var with
-        | Some (Global g) -> is_protected_by ask m g && is_unprotected_without ask g m
-        | _ -> false
-      )
-    in
+    let apr_local = remove_globals_unprotected_after_unlock ask m apr in
     {st with apr = apr_local}
 
+  let thread_join ask getg exp st = st
+  let thread_return ask getg sideg tid st = st
+
   let sync ask getg sideg (st: apron_components_t) reason =
     match reason with
     | `Return -> (* required for thread return *)
@@ -466,112 +481,557 @@ struct
     {apr = AD.bot (); priv = startstate ()}
 
   let init () = ()
-  let finalize () = ()
+  let finalize () = finalize ()
 end
 
-(** Write-Centered Reading. *)
-(* TODO: uncompleted, only W, P components from basePriv *)
-module WriteCenteredPriv: S = functor (AD: ApronDomain.S2) ->
+(** May written variables. *)
+module W =
 struct
-  open Locksets
-  open WriteCenteredD
+  include MayVars
+  let name () = "W"
+end
 
-  module D = Lattice.Prod (W) (P)
-  module G = AD
+module type ClusterArg = functor (AD: ApronDomain.S2) ->
+sig
+  module LAD: Lattice.S
+
+  val keep_only_protected_globals: Q.ask -> LockDomain.Addr.t -> LAD.t -> LAD.t
+  val keep_global: varinfo -> LAD.t -> LAD.t
+
+  val lock: AD.t -> LAD.t -> LAD.t -> AD.t
+  val unlock: W.t -> AD.t -> LAD.t
+
+  val name: unit -> string
+end
+
+(** No clustering. *)
+module NoCluster:ClusterArg = functor (AD: ApronDomain.S2) ->
+struct
+  module AD = AD
+  open CommonPerMutex(AD)
+  module LAD = AD
+
+  let keep_only_protected_globals = keep_only_protected_globals
+
+  let keep_global g oct =
+    let g_var = V.global g in
+    AD.keep_vars oct [g_var]
+
+  let lock oct local_m get_m =
+    AD.meet oct (AD.join local_m get_m)
+
+  let unlock w oct_side =
+    oct_side
+
+  let name () = "no-clusters"
+end
+
+module type ClusteringArg =
+sig
+  val generate: varinfo list -> varinfo list list
+  val name: unit -> string
+end
+
+(** All clusters of size 1 and 2. *)
+module Clustering12: ClusteringArg =
+struct
+  let generate gs =
+    List.cartesian_product gs gs
+    |> List.filter (fun (g1, g2) -> CilType.Varinfo.compare g1 g2 <= 0) (* filter flipped ordering, keep equals for next step *)
+    |> List.map (fun (g1, g2) -> [g1; g2]) (* if g1 = g2, then we get a singleton cluster *)
+
+  let name () = "cluster12"
+end
+
+(** All clusters of size 2. *)
+module Clustering2: ClusteringArg =
+struct
+  let generate gs =
+    match gs with
+    | [_] -> [gs] (* use clusters of size 1 if only 1 variable *)
+    | _ ->
+      List.cartesian_product gs gs
+      |> List.filter (fun (g1, g2) -> CilType.Varinfo.compare g1 g2 < 0) (* filter flipped ordering, forbid equals for just clusters of size 2 *)
+      |> List.map (fun (g1, g2) -> [g1; g2])
+
+  let name () = "cluster2"
+end
+
+(** All subset clusters. *)
+module ClusteringPower: ClusteringArg =
+struct
+  let generate gs =
+    gs
+    |> List.map (fun _ -> [true; false])
+    |> List.n_cartesian_product (* TODO: exponential! *)
+    |> List.map (fun bs ->
+      (* list globals where omega is true *)
+      List.fold_left2 (fun acc g b ->
+          if b then
+            g :: acc
+          else
+            acc
+        ) [] gs bs
+    )
+
+  let name () = "clusterPow"
+end
+
+(** One maximum cluster. *)
+module ClusteringMax: ClusteringArg =
+struct
+  let generate gs =
+    [gs]
+
+  let name () = "clusterMax"
+end
+
+
+(** Clusters when clustering is downward-closed. *)
+module DownwardClosedCluster (ClusteringArg: ClusteringArg) =  functor (AD: ApronDomain.S2) ->
+struct
+  module AD = AD
+  open CommonPerMutex(AD)
+
+  module VS =
+  struct
+    include Printable.Std
+    include SetDomain.Make (CilType.Varinfo)
+  end
+  module LAD = MapDomain.MapBot (VS) (AD)
+
+  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 *)
+    LAD.filter (fun gs _ ->
+        VS.for_all (is_protected_by ask m) gs
+      ) octs
+
+  let keep_global g octs =
+    let g_var = V.global g in
+    (* normal (strong) mapping: contains only still fully protected *)
+    let g' = VS.singleton g in
+    let oct = LAD.find g' octs in
+    LAD.singleton g' (AD.keep_vars oct [g_var])
+
+  let lock_get_m oct local_m get_m =
+    let joined = LAD.join local_m get_m in
+    if M.tracing then M.traceli "apronpriv" "lock_get_m:\n  get=%a\n  joined=%a\n" LAD.pretty get_m LAD.pretty joined;
+    let r = LAD.fold (fun _ -> AD.meet) joined (AD.bot ()) in (* bot is top with empty env *)
+    if M.tracing then M.trace "apronpriv" "meet=%a\n" AD.pretty r;
+    let r = AD.meet oct r in
+    if M.tracing then M.traceu "apronpriv" "-> %a\n" AD.pretty r;
+    r
+
+  let lock oct local_m get_m =
+    if M.tracing then M.traceli "apronpriv" "cluster lock: local=%a\n" LAD.pretty local_m;
+    let r = lock_get_m oct local_m get_m in
+    (* is_bot check commented out because it's unnecessarily expensive *)
+    (* if AD.is_bot_env r then
+      failwith "DownwardClosedCluster.lock: not downward closed?"; *)
+    if M.tracing then M.traceu "apronpriv" "-> %a\n" AD.pretty r;
+    r
+
+  let unlock w oct_side =
+    let vars = AD.vars oct_side in
+    let gs = List.map (fun var -> match V.find_metadata var with
+        | Some (Global g) -> g
+        | _ -> assert false (* oct_side should only contain (protected) globals *)
+      ) vars
+    in
+    let clusters =
+      ClusteringArg.generate gs
+      |> List.map VS.of_list
+      |> List.filter (VS.exists (fun g -> W.mem g w)) (* cluster intersection w is non-empty *)
+    in
+    let oct_side_cluster gs =
+      AD.keep_vars oct_side (gs |> VS.elements |> List.map V.global)
+    in
+    LAD.add_list_fun clusters oct_side_cluster (LAD.empty ())
+
+  let name = ClusteringArg.name
+end
+
+(** Clusters when clustering is arbitrary (not necessarily downward-closed). *)
+module ArbitraryCluster (ClusteringArg: ClusteringArg): ClusterArg = functor (AD: ApronDomain.S2) ->
+struct
+  module AD = AD
+  module DCCluster = (DownwardClosedCluster(ClusteringArg))(AD)
+
+  open CommonPerMutex(AD)
+
+  module VS = DCCluster.VS
+  module LAD1 = DCCluster.LAD
+  module LAD = Lattice.Prod (LAD1) (LAD1) (* second component is only used between keep_* and lock for additional weak mapping *)
+
+  let name = ClusteringArg.name
+
+  let filter_map' f m =
+    LAD1.fold (fun k v acc ->
+        match f k v with
+        | Some (k', v') ->
+          LAD1.add k' (AD.join (LAD1.find k' acc) v') acc
+        | None ->
+          acc
+      ) m (LAD1.empty ())
+
+  let keep_only_protected_globals ask m (octs, _) =
+    let lad = DCCluster.keep_only_protected_globals ask m octs in
+    let lad_weak =
+      (* backup (weak) mapping: contains any still intersecting with protected, needed for decreasing protecting locksets *)
+      filter_map' (fun gs oct ->
+          (* must filter by protection to avoid later meeting with non-protecting *)
+          let gs' = VS.filter (is_protected_by ask m) gs in
+          if VS.is_empty gs' then
+            None
+          else
+            (* must restrict cluster down to protected (join) *)
+            Some (gs', keep_only_protected_globals ask m oct)
+        ) octs
+    in
+    (lad, lad_weak)
+
+  let keep_global g (octs, _) =
+    let g_var = V.global g in
+    let lad = DCCluster.keep_global g octs in
+    let lad_weak =
+      (* backup (weak) mapping: contains any still intersecting with protected, needed for decreasing protecting locksets *)
+      filter_map' (fun gs oct ->
+          (* must filter by protection to avoid later meeting with non-protecting *)
+          if VS.mem g gs then
+            (* must restrict cluster down to m_g (join) *)
+            Some (VS.singleton g, AD.keep_vars oct [g_var])
+          else
+            None
+        ) octs
+    in
+    (lad, lad_weak)
+
+  let lock oct (local_m, _) (get_m, get_m') =
+    if M.tracing then M.traceli "apronpriv" "cluster lock: local=%a\n" LAD1.pretty local_m;
+    let r =
+      let locked = DCCluster.lock_get_m oct local_m get_m in
+      if AD.is_bot_env locked then (
+        let locked' = DCCluster.lock_get_m oct local_m get_m' in
+        if AD.is_bot_env locked' then
+          raise Deadcode
+        else
+          locked'
+      )
+      else
+        locked
+    in
+    if M.tracing then M.traceu "apronpriv" "-> %a\n" AD.pretty r;
+    r
+
+  let unlock w oct_side =
+    (DCCluster.unlock w oct_side, LAD1.bot ())
+end
+
+(** Per-mutex meet with TIDs. *)
+module PerMutexMeetPrivTID (Cluster: ClusterArg): S  = functor (AD: ApronDomain.S2) ->
+struct
+  open CommonPerMutex(AD)
+  open ExplicitMutexGlobals
+  include ConfCheck.RequireThreadFlagPathSensInit
+
+  module NC = Cluster(AD)
+  module Cluster = NC
+  module LAD = NC.LAD
+
+  (* Map from locks to last written values thread-locally *)
+  module L = MapDomain.MapBot_LiftTop(Locksets.Lock)(LAD)
+
+  module LMust = struct
+    include Locksets.MustLockset
+    let name () = "LMust"
+  end
+
+  module D = Lattice.Prod3 (W) (LMust) (L)
+  module GMutex = MapDomain.MapBot_LiftTop(ThreadIdDomain.ThreadLifted)(LAD)
+  module GThread = Lattice.Prod (LMust) (L)
+  module G = Lattice.Lift2(GMutex)(GThread)(struct let bot_name = "bot" let top_name = "top" end)
+
+  module V = ApronDomain.V
+  module TID = ThreadIdDomain.Thread
+
+  let name () = "PerMutexMeetPrivTID(" ^ (Cluster.name ()) ^ (if GobConfig.get_bool "exp.apron.priv.must-joined" then  ",join"  else "") ^ ")"
+
+  let compatible (ask:Q.ask) current must_joined other =
+    match current, other with
+    | `Lifted current, `Lifted other ->
+      let not_self_read = (not (TID.is_unique current)) || (not (TID.equal current other)) in
+      let may_be_running () =
+        if (not (TID.is_must_parent current other)) then
+          true
+        else
+          let created = ask.f Q.CreatedThreads in
+          let ident_or_may_be_created creator = TID.equal creator other || TID.may_create creator other in
+          if ConcDomain.ThreadSet.is_top created then
+            true
+          else
+            ConcDomain.ThreadSet.exists (ident_or_may_be_created) created
+      in
+      let may_not_be_joined () =
+        try
+          not @@ List.mem other (ConcDomain.ThreadSet.elements must_joined)
+        with _ -> true
+      in
+      not_self_read && (not (GobConfig.get_bool "exp.apron.priv.not-started") || (may_be_running ())) && (not (GobConfig.get_bool "exp.apron.priv.must-joined") || (may_not_be_joined ()))
+    | _ -> true
+
+  let get_relevant_writes (ask:Q.ask) m v =
+    let current = ThreadId.get_current ask in
+    let must_joined = ask.f Queries.MustJoinedThreads in
+    GMutex.fold (fun k v acc ->
+        if compatible ask current must_joined k then
+          LAD.join acc (Cluster.keep_only_protected_globals ask m v)
+        else
+          acc
+      ) v (LAD.bot ())
+
+  let get_relevant_writes_nofilter (ask:Q.ask) v =
+    let current = ThreadId.get_current ask in
+    let must_joined = ask.f Queries.MustJoinedThreads in
+    GMutex.fold (fun k v acc ->
+        if compatible ask current must_joined k then
+          LAD.join acc v
+        else
+          acc
+      ) v (LAD.bot ())
+
+  let merge_all v =
+    GMutex.fold (fun _ v acc -> LAD.join acc v) v (LAD.bot ())
 
   type apron_components_t =  ApronDomain.ApronComponents (AD) (D).t
   let global_varinfo = RichVarinfo.single ~name:"APRON_GLOBAL"
 
-  let name () = "WriteCenteredPriv"
 
-  let startstate () = (W.bot (), P.top ())
+  let startstate () = W.bot (), LMust.top (), L.bot ()
 
   let should_join _ _ = true
 
-  let lockset_init = Lockset.top ()
-
-  (* TODO: distr_init? *)
-
-  let restrict_globals apr =
-    match !MyCFG.current_node with
-    | Some node ->
-      let fd = Node.find_fundec node in
-      if M.tracing then M.trace "apronpriv" "restrict_globals %s\n" fd.svar.vname;
-      (* TODO: avoid *)
-      let vars =
-        foldGlobals !Cilfacade.current_file (fun acc global ->
-            match global with
-            | GVar (vi, _, _) ->
-              vi :: acc
-            (* TODO: what about GVarDecl? *)
-            | _ -> acc
-          ) []
-      in
-      let to_keep = List.map (fun v -> Var.of_string v.vname) vars in
-      AD.keep_vars apr to_keep
-    | None ->
-      (* TODO: when does this happen? *)
-      if M.tracing then M.trace "apronpriv" "restrict_globals -\n";
-      AD.bot ()
+  let mutex_inits = RichVarinfo.single ~name:"MUTEX_INITS"
 
-  let read_global ask getg (st: apron_components_t) g x =
-    (* let s = current_lockset ask in *)
-    (* let (w, p) = st.priv in *)
-    (* let p_g = P.find g p in *)
-    (* TODO: implement *)
-    let apr' = AD.add_vars st.apr [Var.of_string g.vname] in
-    let apr' = A.assign_texpr AD.Man.mgr apr' (Var.of_string x.vname) (Texpr1.var (A.env apr') (Var.of_string g.vname)) None in (* TODO: unsound *)
-    apr'
+  let get_m_with_mutex_inits inits ask getg_mutex m =
+    let vi = mutex_addr_to_varinfo m in
+    let get_m = get_relevant_writes ask m (getg_mutex vi) in
+    if M.tracing then M.traceli "apronpriv" "get_m_with_mutex_inits %a\n  get=%a\n" LockDomain.Addr.pretty m LAD.pretty get_m;
+    let r =
+    if not inits then
+      get_m
+    else
+      let get_mutex_inits = merge_all @@ getg_mutex (mutex_inits ()) in
+      let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in
+      if M.tracing then M.trace "apronpriv" "inits=%a\n  inits'=%a\n" LAD.pretty get_mutex_inits LAD.pretty get_mutex_inits';
+      LAD.join get_m get_mutex_inits'
+    in
+    if M.tracing then M.traceu "apronpriv" "-> %a\n" LAD.pretty r;
+    r
 
-  let write_global ?(invariant=false) ask getg sideg (st: apron_components_t) g x: apron_components_t =
-    let s = current_lockset ask in
-    let (w, p) = st.priv in
-    let w' = W.add g (MinLocksets.singleton s) w in
-    let p' = P.add g (MinLocksets.singleton s) p in
-    let p' = P.map (fun s' -> MinLocksets.add s s') p' in
-    (* TODO: implement *)
-    let apr' = AD.add_vars st.apr [Var.of_string g.vname] in
-    let apr' = A.assign_texpr AD.Man.mgr apr' (Var.of_string g.vname) (Texpr1.var (A.env apr') (Var.of_string x.vname)) None in (* TODO: unsound? *)
-    sideg (global_varinfo ()) (restrict_globals apr');
-    {apr = apr'; priv = (w', p')}
+  let get_mutex_global_g_with_mutex_inits inits ask getg_mutex g =
+    let vi = mutex_global g in
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ getg_mutex vi in
+    if M.tracing then M.traceli "apronpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LAD.pretty get_mutex_global_g;
+    let r =
+    if not inits then
+      get_mutex_global_g
+    else
+      let get_mutex_inits = merge_all @@ getg_mutex (mutex_inits ()) in
+      let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in
+      if M.tracing then M.trace "apronpriv" "inits=%a\n  inits'=%a\n" LAD.pretty get_mutex_inits LAD.pretty get_mutex_inits';
+      LAD.join get_mutex_global_g get_mutex_inits'
+    in
+    if M.tracing then M.traceu "apronpriv" "-> %a\n" LAD.pretty r;
+    r
 
-  let lock ask getg (st: apron_components_t) m = st
+  let read_global ask getg (st: apron_components_t) g x: AD.t =
+    let _,lmust,l = st.priv in
+    let apr = st.apr in
+    let m = Locksets.Lock.from_var (mutex_global g) in
+    (* lock *)
+    let tmp = (get_mutex_global_g_with_mutex_inits (not (LMust.mem m lmust)) ask getg g) in
+    let local_m = BatOption.default (LAD.bot ()) (L.find_opt m l) in
+    (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
+    let apr = Cluster.lock apr local_m tmp in
+    (* read *)
+    let g_var = V.global g in
+    let x_var = Var.of_string x.vname in
+    let apr_local = AD.add_vars apr [g_var] in
+    let apr_local = AD.assign_var apr_local x_var g_var in
+    (* unlock *)
+    let apr_local' =
+      if is_unprotected ask g then
+        AD.remove_vars apr_local [g_var]
+      else
+        apr_local
+    in
+    apr_local'
 
-  let unlock ask getg sideg (st: apron_components_t) m =
-    let s = Lockset.remove m (current_lockset ask) in
-    let (w, p) = st.priv in
-    let p' = P.map (fun s' -> MinLocksets.add s s') p in
-    (* TODO: implement *)
-    sideg (global_varinfo ()) (restrict_globals st.apr);
-    {st with priv = (w, p')}
+  let write_global ?(invariant=false) (ask:Q.ask) getg sideg (st: apron_components_t) g x: apron_components_t =
+    let w,lmust,l = st.priv in
+    let mg = mutex_global g in
+    let m = Locksets.Lock.from_var mg in
+    let apr = st.apr in
+    (* lock *)
+    let tmp = (get_mutex_global_g_with_mutex_inits (not (LMust.mem m lmust)) ask getg g) in
+    let local_m = BatOption.default (LAD.bot ()) (L.find_opt m l) in
+    (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
+    let apr = Cluster.lock apr local_m tmp in
+    (* write *)
+    let g_var = V.global g in
+    let x_var = Var.of_string x.vname in
+    let apr_local = AD.add_vars apr [g_var] in
+    let apr_local = AD.assign_var apr_local g_var x_var in
+    (* unlock *)
+    let apr_side = AD.keep_vars apr_local [g_var] in
+    let apr_side = Cluster.unlock (W.singleton g) apr_side in
+    let tid = ThreadId.get_current ask in
+    let sidev = GMutex.singleton tid apr_side in
+    sideg mg sidev;
+    let l' = L.add m apr_side l in
+    let apr_local' =
+      if is_unprotected ask g then
+        AD.remove_vars apr_local [g_var]
+      else
+        apr_local
+    in
+    {apr = apr_local'; priv = (W.add g w,LMust.add m lmust,l')}
 
-  let sync ask getg sideg (st: apron_components_t) reason =
+  let lock ask getg (st: apron_components_t) m =
+    let apr = st.apr in
+    let _,lmust,l = st.priv in
+    let get_m = get_m_with_mutex_inits (not (LMust.mem m lmust)) ask getg m in
+    let local_m = BatOption.default (LAD.bot ()) (L.find_opt m 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
+    let apr = Cluster.lock apr local_m get_m in
+    {st with apr}
+
+  let unlock ask getg sideg (st: apron_components_t) m: apron_components_t =
+    let apr = st.apr in
+    let w,lmust,l = st.priv in
+    let apr_local = remove_globals_unprotected_after_unlock ask m apr in
+    let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
+    let side_needed = W.exists (fun v -> is_protected_by ask m v) w in
+    if not side_needed then
+      {apr = apr_local; priv = (w',lmust,l)}
+    else
+      let apr_side = keep_only_protected_globals ask m apr in
+      let apr_side = Cluster.unlock w apr_side in
+      let tid = ThreadId.get_current ask in
+      let sidev = GMutex.singleton tid apr_side in
+      sideg (mutex_addr_to_varinfo m) sidev;
+      let l' = L.add m apr_side l in
+      {apr = apr_local; priv = (w',LMust.add m lmust,l')}
+
+  let thread_join (ask:Q.ask) getg exp (st: apron_components_t) =
+    let w,lmust,l = st.priv in
+    let tids = ask.f (Q.EvalThread exp) in
+    if ConcDomain.ThreadSet.is_top tids then
+      st (* TODO: why needed? *)
+    else (
+      (* elements throws if the thread set is top *)
+      let tids = ConcDomain.ThreadSet.elements tids in
+      match tids with
+      | [tid] ->
+        let lmust',l' = getg tid in
+        {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
+      | _ ->
+        (* To match the paper more closely, one would have to join in the non-definite case too *)
+        (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
+        st
+    )
+
+  let thread_return ask getg sideg tid (st: apron_components_t) =
+    let _,lmust,l = st.priv in
+    sideg tid (lmust,l);
+    st
+
+  let sync (ask:Q.ask) getg sideg (st: apron_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
+    | `Return -> st (* TODO: implement? *)
+    | `Join ->
+      if (ask.f Q.MustBeSingleThreaded) then
+        st
+      else
+        let apr = st.apr in
+        (* There can be no branched going multi-threaded here *)
+        (* TODO: Do we need to remove no longer protected variables here? *)
+        (* TODO: Is not potentially even unsound to do so?! *)
+        let apr_local = AD.remove_filter apr (fun var ->
+            match V.find_metadata var with
+            | Some (Global g) -> is_unprotected ask g
+            | _ -> false
+          )
+        in
+        {st with apr = apr_local}
     | `Normal
-    | `Join (* TODO: no problem with branched thread creation here? *)
     | `Init
     | `Thread ->
       st
 
-  let enter_multithreaded ask getg sideg (st: apron_components_t) =
-    (* TODO: implement *)
-    {st with apr = AD.meet st.apr (getg (global_varinfo ()))}
+  let enter_multithreaded (ask:Q.ask) getg sideg (st: apron_components_t): apron_components_t =
+    let apr = st.apr in
+    (* Don't use keep_filter & remove_filter because it would duplicate find_metadata-s. *)
+    let g_vars = List.filter (fun var ->
+        match V.find_metadata var with
+        | Some (Global _) -> true
+        | _ -> false
+      ) (AD.vars apr)
+    in
+    let apr_side = AD.keep_vars apr g_vars in
+    let apr_side = Cluster.unlock (W.top ()) apr_side in (* top W to avoid any filtering *)
+    let tid = ThreadId.get_current ask in
+    let sidev = GMutex.singleton tid apr_side in
+    let vi = mutex_inits () in
+    sideg vi sidev;
+    (* Introduction into local state not needed, will be read via initializer *)
+    (* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *)
+    (* or it will be locally overwitten and in LMust in which case these values are irrelevant anyway *)
+    let apr_local = AD.remove_vars apr g_vars in
+    {st with apr = apr_local}
 
   let threadenter ask getg (st: apron_components_t): apron_components_t =
-    {apr = getg (global_varinfo ()); priv = startstate ()}
+    let _,lmust,l = st.priv in
+    {apr = AD.bot (); priv = (W.bot (),lmust,l)}
 
-  let init () = ()
-  let finalize () = ()
-end
+  let finalize () = finalize ()
+
+  (* All that follows is stupid boilerplate to give each of these functions the getg and sideg that only deals with TIDs or Mutexes *)
+
+  let sideg_mutex (sideg: varinfo -> G.t -> unit) (g:varinfo) (v:GMutex.t):unit =
+    sideg g (`Lifted1 v)
 
+  let sideg_tid (sideg:varinfo -> G.t -> unit) (tid:TID.t) (v:GThread.t):unit =
+    sideg (TID.to_varinfo tid) (`Lifted2 v)
+
+  let getg_mutex getg g = match getg g with
+    | `Lifted1 v -> v
+    | `Bot -> GMutex.bot ()
+    | _ -> failwith "wrong either argument"
+
+  let getg_tid getg tid = match getg (TID.to_varinfo tid) with
+    | `Lifted2 v -> v
+    | `Bot -> GThread.bot ()
+    | _ -> failwith "wrong either argument"
+
+  let patch_getside_mutex fn ask getg sideg = fn ask (getg_mutex getg) (sideg_mutex sideg)
+  let patch_getside_tid fn ask getg sideg = fn ask (getg_tid getg) (sideg_tid sideg)
+
+  let patch_get_mutex fn ask getg = fn ask (getg_mutex getg)
+  let patch_get_tid fn ask getg = fn ask (getg_tid getg)
+
+  let read_global = patch_get_mutex read_global
+  let write_global ?(invariant=false) (ask:Q.ask) getg sideg = write_global ~invariant ask (getg_mutex getg) (sideg_mutex sideg)
+  let lock = patch_get_mutex lock
+  let unlock = patch_getside_mutex unlock
+  let thread_join = patch_get_tid thread_join
+  let thread_return = patch_getside_tid thread_return
+  let sync = patch_getside_mutex sync
+  let enter_multithreaded = patch_getside_mutex enter_multithreaded
+  let threadenter = patch_get_mutex threadenter
+end
 
 module TracingPriv = functor (Priv: S) -> functor (AD: ApronDomain.S2) ->
 struct
@@ -690,8 +1150,12 @@ let priv_module: (module S) Lazy.t =
          | "dummy" -> (module Dummy : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
-         | "mutex-meet" -> (module PerMutexMeetPriv )
-         (* | "write" -> (module WriteCenteredPriv) *)
+         | "mutex-meet" -> (module PerMutexMeetPriv)
+         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster))
+         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12)))
+         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2)))
+         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ArbitraryCluster (ClusteringMax)))
+         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (ClusteringPower)))
          | _ -> failwith "exp.apron.privatization: illegal value"
       )
     in
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 48fab311f2..67154d588a 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -6,6 +6,38 @@ module Q = Queries
 module IdxDom = ValueDomain.IndexDomain
 module VD     = BaseDomain.VD
 
+module ProtectionLogging =
+struct
+  module GM = Hashtbl.Make(ValueDomain.Addr)
+  module VarSet = SetDomain.Make(Basetype.Variables)
+  let gm = GM.create 10
+
+  let record m x =
+    if !GU.postsolving && GobConfig.get_bool "dbg.print_protection" then
+      let old = GM.find_default gm m (VarSet.empty ()) in
+      let n = VarSet.add x old in
+      GM.replace gm m n
+
+  let dump () =
+    if GobConfig.get_bool "dbg.print_protection" then (
+      let max_cluster = ref 0 in
+      let num_mutexes = ref 0 in
+      let sum_protected = ref 0 in
+      Printf.printf "\n\nProtecting mutexes:\n";
+      GM.iter (fun m vs ->
+          let s = VarSet.cardinal vs in
+          max_cluster := max !max_cluster s;
+          sum_protected := !sum_protected + s;
+          incr num_mutexes;
+          Printf.printf "%s -> %s\n" (ValueDomain.Addr.show m) (VarSet.show vs) ) gm;
+      Printf.printf "\nMax number of protected: %i\n" !max_cluster;
+      Printf.printf "Num mutexes: %i\n" !num_mutexes;
+      Printf.printf "Sum protected: %i\n" !sum_protected
+    );
+
+
+end
+
 module Protection =
 struct
   let is_unprotected ask x: bool =
@@ -25,6 +57,11 @@ struct
     not (VD.is_immediate_type x.vtype) &&
     ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true})
 
+  let is_protected_by ask m x =
+    let r = is_protected_by ask m x in
+    if r then ProtectionLogging.record m x;
+    r
+
   let is_atomic ask: bool =
     ask Q.MustBeAtomic
 end
@@ -87,6 +124,8 @@ struct
     let disjoint s t = is_empty (inter s t)
   end
 
+  module MustLockset = SetDomain.Reverse (Lockset)
+
   let rec conv_offset = function
     | `NoOffset -> `NoOffset
     | `Field (f, o) -> `Field (f, conv_offset o)
@@ -104,7 +143,7 @@ struct
         ) ls (Lockset.empty ())
 
   (* TODO: reversed SetDomain.Hoare *)
-  module MinLocksets = HoareDomain.Set_LiftTop (Lattice.Reverse (Lockset)) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
+  module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
 end
 
 module WriteCenteredD =
@@ -149,4 +188,14 @@ struct
       ()
   end
 
+  module RequireThreadFlagPathSensInit =
+  struct
+    let init () =
+      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
+        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
+
 end
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 038ee20e1c..f7f61c9b44 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -45,6 +45,7 @@ struct
     match LibraryFunctions.classify f.vname arglist with
     | `ThreadJoin (id, ret_var) ->
       (* TODO: generalize ThreadJoin like ThreadCreate *)
+      (* TODO: elements might throw an exception *)
       let threads = TS.elements (ctx.ask (Queries.EvalThread id)) in
       let has_clean_exit tid = not (BatTuple.Tuple3.third (ctx.global (T.to_varinfo tid))) in
       let join_thread s tid =
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 568b11dcd2..a56ed776e2 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -28,17 +28,26 @@ struct
   module C = D
   module G = Lattice.Unit
 
+  let tids = ref (Hashtbl.create 20)
+
   let name () = "threadid"
 
   let startstate v = (ThreadLifted.bot (), TD.bot ())
   let exitstate  v = (`Lifted (Thread.threadinit v ~multiple:true), TD.bot ())
 
-  let morphstate v _ = (`Lifted (Thread.threadinit v ~multiple:false), TD.bot ())
+  let morphstate v _ =
+    let tid = Thread.threadinit v ~multiple:false in
+    if GobConfig.get_bool "dbg.print_tids" then
+      Hashtbl.replace !tids tid ();
+    (`Lifted (tid), TD.bot ())
 
   let create_tid (current, td) (node: Node.t) v =
     match current with
     | `Lifted current ->
-      `Lifted (Thread.threadenter (current, td) node v)
+      let tid = Thread.threadenter (current, td) node v in
+      if GobConfig.get_bool "dbg.print_tids" then
+        Hashtbl.replace !tids tid ();
+      `Lifted (tid)
     | _ ->
       `Lifted (Thread.threadinit v ~multiple:true)
 
@@ -77,9 +86,15 @@ struct
     else
       (Access.LSSSet.singleton es, es)
 
+  let created (current, td) =
+    match current with
+    | `Lifted current -> BatOption.map_default (ConcDomain.ThreadSet.of_list) (ConcDomain.ThreadSet.top ()) (Thread.created current td)
+    | _ -> ConcDomain.ThreadSet.top ()
+
   let query (ctx: (D.t, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
     match x with
     | Queries.CurrentThreadId -> fst ctx.local
+    | Queries.CreatedThreads -> created ctx.local
     | Queries.PartAccess {exp; var_opt; write} ->
       part_access ctx exp var_opt write
     | Queries.MustBeUniqueThread ->
@@ -96,12 +111,29 @@ struct
     let (current, td) = ctx.local in
     (current, Thread.threadspawn td ctx.node f)
 
-  type marshal = Thread.marshal
-  let init m =
-    Thread.init m
+  type marshal = Thread.marshal * ((Thread.t,unit) Hashtbl.t)
+  let init (m:marshal option): unit =
+    match m with
+    | Some (x,y) -> Thread.init (Some x); tids := y
+    | None ->  Thread.init None
+
+
+  let print_tid_info () =
+    let tids = Hashtbl.to_list !tids in
+    let uniques = List.filter_map (fun (a,b) -> if Thread.is_unique a then Some a else None) tids in
+    let non_uniques = List.filter_map (fun (a,b) -> if not (Thread.is_unique a) then Some a else None) tids in
+    let uc = List.length uniques in
+    let nc = List.length non_uniques in
+    Printf.printf "Encountered number of thread IDs (unique): %i (%i)\n" (uc+nc) uc;
+    Printf.printf "unique: ";
+    List.iter (fun tid -> Printf.printf " %s " (Thread.show tid)) uniques;
+    Printf.printf "\nnon-unique: ";
+    List.iter (fun tid -> Printf.printf " %s " (Thread.show tid)) non_uniques;
+    Printf.printf "\n"
 
   let finalize () =
-    Thread.finalize ()
+    if GobConfig.get_bool "dbg.print_tids" then print_tid_info ();
+    Thread.finalize (),!tids
 end
 
 let _ =
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index 2ac1ba8427..9ed23eaf3f 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -27,8 +27,12 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     match LibraryFunctions.classify f.vname arglist with
     | `ThreadJoin (id, ret_var) ->
-      (
-        let threads = TIDs.elements (ctx.ask (Queries.EvalThread id)) in
+      let threads = ctx.ask (Queries.EvalThread id) in
+      if TIDs.is_top threads then
+        ctx.local
+      else (
+        (* elements throws if the thread set is top *)
+        let threads = TIDs.elements threads in
         match threads with
         | [tid] when TID.is_unique tid->
           let joined = ctx.global (TID.to_varinfo tid) in
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 6e769345b5..56215351d7 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -15,6 +15,11 @@ module M = Messages
     - C API docs PDF (alternative mathematical descriptions): https://antoinemine.github.io/Apron/doc/api/c/apron.pdf
     - heterogeneous environments: https://link.springer.com/chapter/10.1007%2F978-3-030-17184-1_26 (Section 4.1) *)
 
+let widening_thresholds_apron = lazy (
+  let t = WideningThresholds.thresholds () in
+  let r = List.map (fun x -> Apron.Scalar.of_mpqf @@ Mpqf.of_string @@ Z.to_string x) t in
+  Array.of_list r
+)
 
 module Var =
 struct
@@ -813,7 +818,8 @@ struct
       if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y;
       let j = join x y in
       if M.tracing then M.trace "apron" "j = %a\n" pretty j;
-      let j = strengthening j x y in
+      (* TODO: optimize strengthening, currently disabled because relational traces doesn't join different environments *)
+      (* let j = strengthening j x y in *)
       if M.tracing then M.traceu "apron" "-> %a\n" pretty j;
       j
     )
@@ -836,8 +842,16 @@ struct
   let widen x y =
     let x_env = A.env x in
     let y_env = A.env y in
-    if Environment.equal x_env y_env then
-      A.widening Man.mgr x y (* widen if env didn't increase *)
+    if Environment.equal x_env y_env  then
+      if GobConfig.get_bool "ana.apron.threshold_widening" && Oct.manager_is_oct Man.mgr then
+        let octmgr = Oct.manager_to_oct Man.mgr in
+        let ts = Lazy.force widening_thresholds_apron in
+        let x_oct = Oct.Abstract1.to_oct x in
+        let y_oct = Oct.Abstract1.to_oct y in
+        let r = Oct.widening_thresholds octmgr (Abstract1.abstract0 x_oct) (Abstract1.abstract0 y_oct) ts in
+        Oct.Abstract1.of_oct {x_oct with abstract0 = r}
+      else
+        A.widening Man.mgr x y
     else
       y (* env increased, just use joined value in y, assuming env doesn't increase infinitely *)
 
diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml
index 87f502b037..370b4285c9 100644
--- a/src/cdomains/threadIdDomain.ml
+++ b/src/cdomains/threadIdDomain.ml
@@ -39,6 +39,9 @@ sig
 
   val threadenter: t * D.t -> Node.t -> varinfo -> t
   val threadspawn: D.t -> Node.t -> varinfo -> D.t
+
+  (** If it is possible to get a list of unique thread create thus far, get it *)
+  val created: t -> D.t -> (t list) option
 end
 
 
@@ -94,6 +97,8 @@ struct
 
   let threadenter _ = threadenter
   let threadspawn () _ _ = ()
+
+  let created _ _ = None
 end
 
 module History (Base: Stateless): Stateful =
@@ -112,7 +117,7 @@ struct
   module M = struct
     include Printable.Prod (P) (S)
     (* Varinfos for histories are named using a string representation based on node ids,
-     not locations, for compatibilty with incremental analysis.*)
+     not locations, for compatibility with incremental analysis.*)
     let name_varinfo ((l, s): t): string =
       let list_name = String.concat "," (List.map Base.name_varinfo l) in
       let set_name = String.concat "," (List.map Base.name_varinfo (S.elements s)) in
@@ -166,6 +171,10 @@ struct
     else
       composed
 
+  let created current cs =
+    let els = D.elements cs in
+    Some (List.map (compose current) els)
+
   let threadspawn cs l v =
     S.add (Base.threadenter l v) cs
 
diff --git a/src/domains/setDomain.ml b/src/domains/setDomain.ml
index 2ff3014c4e..caf2bd25fe 100644
--- a/src/domains/setDomain.ml
+++ b/src/domains/setDomain.ml
@@ -1,8 +1,6 @@
 (** Abstract domains representing sets. *)
 open Pretty
 
-module GU = Goblintutil
-
 (* Exception raised when the set domain can not support the requested operation.
  * This will be raised, when trying to iterate a set that has been set to Top *)
 exception Unsupported of string
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index eaa647d0ec..c668215298 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -204,9 +204,10 @@ module WP =
         HM.replace stable y ();
         if not (S.Dom.leq tmp old) then (
           (* if there already was a `side x y d` that changed rho[y] and now again, we make y a wpoint *)
+          let old_sides = HM.find_default sides y VS.empty in
           let sided = match x with
             | Some x ->
-              let sided = VS.mem x (HM.find_default sides y VS.empty) in
+              let sided = VS.mem x old_sides in
               if not sided then add_sides y x;
               sided
             | None -> false
@@ -223,6 +224,13 @@ module WP =
             wpoint_if false
           | "sides" -> (* x caused more than one update to y. >=3 partial context calls will be precise since sides come from different x. TODO this has 8 instead of 5 phases of `solver` for side_cycle.c *)
             wpoint_if sided
+          | "sides-pp" ->
+            (match x with
+            | Some x ->
+              let n = S.Var.node x in
+              let sided = VS.exists (fun v -> Node.equal (S.Var.node v) n) old_sides in
+              wpoint_if sided
+            | None -> ())
           | "cycle" -> (* destabilized a called or start var. Problem: two partial context calls will be precise, but third call will widen the state. *)
             (* if this side destabilized some of the initial unknowns vs, there may be a side-cycle between vs and we should make y a wpoint *)
             let destabilized_vs = destabilize_vs y in
@@ -275,9 +283,9 @@ module WP =
         if GobConfig.get_bool "incremental.reluctant.on" then (
           (* save entries of changed functions in rho for the comparison whether the result has changed after a function specific solve *)
           HM.iter (fun k v -> if Set.mem (S.Var.var_id k) obsolete_ret then ( (* TODO: don't use string-based nodes *)
-            let old_rho = HM.find rho k in
-            let old_infl = HM.find_default infl k VS.empty in
-            Hashtbl.replace old_ret k (old_rho, old_infl))) rho;
+              let old_rho = HM.find rho k in
+              let old_infl = HM.find_default infl k VS.empty in
+              Hashtbl.replace old_ret k (old_rho, old_infl))) rho;
         ) else (
           (* If reluctant destabilization is turned off we need to destabilize all nodes in completely changed functions
              and the primary obsolete nodes of partly changed functions *)
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index e4cd9985a1..c13761c5c1 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -81,6 +81,7 @@ let end_basic_blocks f =
   let thisVisitor = new allBBVisitor in
   visitCilFileSameGlobals thisVisitor f
 
+
 let visitors = ref []
 let register_preprocess name visitor_fun =
   visitors := !visitors @ [name, visitor_fun]
diff --git a/src/util/defaults.ml b/src/util/defaults.ml
index 3865d2456b..622960244a 100644
--- a/src/util/defaults.ml
+++ b/src/util/defaults.ml
@@ -146,6 +146,7 @@ let _ = ()
       ; reg Analyses "ana.apron.context" "true" "Entire relation in function contexts."
       ; reg Analyses "ana.apron.domain" "'octagon'" "Which domain should be used for the Apron analysis. Can be 'octagon', 'interval' or 'polyhedra'"
       ; reg Analyses "ana.context.widen"     "false" "Do widening on contexts. Keeps a map of function to call state; enter will then return the widened local state for recursive calls."
+      ; reg Analyses "ana.apron.threshold_widening" "false" "Use constants appearing in program as threshold for widening"
 
 (* {4 category [Incremental]} *)
 let _ = ()
@@ -179,7 +180,9 @@ let _ = ()
       ; reg Experimental "exp.privatization"     "'protection-read'" "Which privatization to use? none/protection-old/mutex-oplus/mutex-meet/protection/protection-read/protection-vesal/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock"
       ; reg Experimental "exp.priv-prec-dump"    "''"    "File to dump privatization precision data to."
       ; reg Experimental "exp.priv-distr-init"   "false"  "Distribute global initializations to all global invariants for more consistent widening dynamics."
-      ; reg Experimental "exp.apron.privatization" "'mutex-meet'" "Which Apron privatization to use? dummy/protection/protection-path/mutex-meet"
+      ; reg Experimental "exp.apron.privatization" "'mutex-meet'" "Which apron privatization to use? dummy/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power"
+      ; reg Experimental "exp.apron.priv.not-started" "true" "Exclude writes from threads that may not be started yet"
+      ; reg Experimental "exp.apron.priv.must-joined" "true" "Exclude writes from threads that must have been joined"
       ; reg Experimental "exp.apron.prec-dump"    "''"    "File to dump apron precision data to."
       ; reg Experimental "exp.cfgdot"            "false" "Output CFG to dot files"
       ; reg Experimental "exp.mincfg"            "false" "Try to minimize the number of CFG nodes."
@@ -200,7 +203,7 @@ let _ = ()
       ; reg Experimental "exp.no-narrow"         "false" "Overwrite narrow a b = a"
       ; reg Experimental "exp.basic-blocks"      "false" "Only keep values for basic blocks instead of for every node. Should take longer but need less space."
       ; reg Experimental "exp.solver.td3.term"   "true"  "Should the td3 solver use the phased/terminating strategy?"
-      ; reg Experimental "exp.solver.td3.side_widen" "'sides'" "When to widen in side. never: never widen, always: always widen, sides: widen if there are multiple side-effects from the same var resulting in a new value, cycle: widen if a called or a start var get destabilized, unstable_called: widen if any called var gets destabilized, unstable_self: widen if side-effected var gets destabilized."
+      ; reg Experimental "exp.solver.td3.side_widen" "'sides'" "When to widen in side. never: never widen, always: always widen, sides: widen if there are multiple side-effects from the same var resulting in a new value, cycle: widen if a called or a start var get destabilized, unstable_called: widen if any called var gets destabilized, unstable_self: widen if side-effected var gets destabilized, sides-pp: widen if there are multiple side-effects from the same program point resulting in a new value."
       ; reg Experimental "exp.solver.td3.space"  "false" "Should the td3 solver only keep values at widening points?"
       ; reg Experimental "exp.solver.td3.space_cache" "true" "Should the td3-space solver cache values?"
       ; reg Experimental "exp.solver.td3.space_restore" "true" "Should the td3-space solver restore values for non-widening-points? Not needed for generating warnings, but needed for inspecting output!"
@@ -247,7 +250,9 @@ let _ = ()
       ; reg Debugging "dbg.cilcfgdot"       "false" "Output dot files for CIL CFGs."
       ; reg Debugging "dbg.cfg.loop-clusters" "false" "Add loop SCC clusters to CFG .dot output."
       ; reg Debugging "dbg.compare_runs.glob" "true" "Compare GlobConstrSys in compare_runs"
-      ; reg Debugging "dbg.compare_runs.eq" "true" "Compare EqConstrSys in compare_runs"
+      ; reg Debugging "dbg.compare_runs.eq"  "true" "Compare EqConstrSys in compare_runs"
+      ; reg Debugging "dbg.print_tids"       "false" "Should the analysis print information on the encountered TIDs"
+      ; reg Debugging "dbg.print_protection" "false" "Should the analysis print information on which globals are protected by which mutex?"
 
 (* {4 category [Warnings]} *)
 let _ = ()
diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml
index 52397e37eb..8108f0eac8 100644
--- a/src/util/precCompare.ml
+++ b/src/util/precCompare.ml
@@ -45,7 +45,7 @@ end
 module Make (D: Lattice.S) =
 struct
 
-  let compare ?(name1="left") ?(name2="right") v1 v2 =
+  let compare ?(verbose=false) ?(name1="left") ?(name2="right") v1 v2 =
     let c = match D.leq v1 v2, D.leq v2 v1 with
       | true, true -> Comparison.Equal
       | true, false -> Comparison.MorePrecise 1
@@ -57,7 +57,8 @@ struct
       ++
       (if D.leq v2 v1 then nil else dprintf "reverse diff: %a\n" D.pretty_diff (v2, v1))
     in
-    let msg = Pretty.dprintf "%s %s %s\n  @[%s: %a\n%s\n%s: %a\n%t@]" name1 (Comparison.to_string_infix c) name2 name1 D.pretty v1 (Comparison.to_string_infix c) name2 D.pretty v2 diff in
+    let msg = if verbose then Pretty.dprintf "%s %s %s\n  @[%s: %a\n%s\n%s: %a\n%t@]" name1 (Comparison.to_string_infix c) name2 name1 D.pretty v1 (Comparison.to_string_infix c) name2 D.pretty v2 diff
+      else Pretty.nil in
     (c, msg)
 end
 
@@ -66,7 +67,7 @@ struct
 
   module CompareD = Make (D)
 
-  let compare ?(name1="left") ?(name2="right") kh1 kh2 =
+  let compare ?(verbose=false) ?(name1="left") ?(name2="right") kh1 kh2 =
     let kh = KH.merge (fun k v1 v2 -> Some (v1, v2)) kh1 kh2 in
     let compared = KH.map (fun k (v1, v2) ->
         let v1 = v1 |? D.bot () in
@@ -78,7 +79,7 @@ struct
         match c with
         | Comparison.Equal -> ()
         | _ ->
-          ignore (Pretty.printf "%a: %t\n" K.pretty k (fun () -> msg))
+          if verbose then ignore (Pretty.printf "%a: %t\n" K.pretty k (fun () -> msg))
       ) compared;
     let c = KH.fold (fun _ (c, _) acc -> Comparison.aggregate_same c acc) compared Comparison.Equal in
     let (m, l) = Comparison.counts c in
diff --git a/src/util/wideningThresholds.ml b/src/util/wideningThresholds.ml
new file mode 100644
index 0000000000..9bbf6e30f0
--- /dev/null
+++ b/src/util/wideningThresholds.ml
@@ -0,0 +1,30 @@
+open Cil
+module Thresholds = Set.Make(Z)
+
+
+class extractConstantsVisitor(widening_thresholds) = object
+  inherit nopCilVisitor
+
+  method! vexpr e =
+    match e with
+    | Const (CInt64(i,ik,str)) ->
+      let bi = match str with
+        | Some t -> Z.of_string t
+        | None -> Z.of_int64 i
+      in
+      widening_thresholds := Thresholds.add bi !widening_thresholds;
+      (* Adding double value of all constants so that we can establish for single variables that they are <= const*)
+      (* This is only needed for Apron, one might want to remove it later *)
+      widening_thresholds := Thresholds.add (Z.mul (Z.of_int 2) bi) !widening_thresholds;
+      DoChildren
+    | _ -> DoChildren
+end
+
+let widening_thresholds = lazy (
+  let set = ref Thresholds.empty in
+  let thisVisitor = new extractConstantsVisitor(set) in
+  visitCilFileSameGlobals thisVisitor (!Cilfacade.current_file);
+  Thresholds.elements !set)
+
+let thresholds () =
+  Lazy.force widening_thresholds
diff --git a/src/util/wideningThresholds.mli b/src/util/wideningThresholds.mli
new file mode 100644
index 0000000000..832b4e7389
--- /dev/null
+++ b/src/util/wideningThresholds.mli
@@ -0,0 +1 @@
+val thresholds : unit -> Z.t list
diff --git a/tests/regression/02-base/04-branched_thread_creation.c b/tests/regression/02-base/04-branched_thread_creation.c
index 053fec27cd..429bd4c394 100644
--- a/tests/regression/02-base/04-branched_thread_creation.c
+++ b/tests/regression/02-base/04-branched_thread_creation.c
@@ -10,22 +10,31 @@ int glob2 = 9;
 
 int main() {
   int k;
+  int mt=0;
   pthread_t id;
 
-  if (k)
+  if (k) {
+    mt=1;
     pthread_create(&id, NULL, t_fun, NULL);
-  else
+  }
+  else {
     glob1 = 4;
+  }
 
   // We need to side-effect glob1=4 upon the join here;
   // otherwise, the global invariant will still have glob1=3.
 
   k = glob1;
-  assert(k == 3); // UNKNOWN!
+  if(!mt) {
+    // If we are not multi-threaded, or are not sure if we are
+    if(k==3) {} else {
+      // This must be reachable
+      assert(1);
+    }
+  }
 
   k = glob2;
   assert(k == 9);
 
   return 0;
 }
-
diff --git a/tests/regression/02-base/45-branched_thread_creation_return.c b/tests/regression/02-base/45-branched_thread_creation_return.c
index 2c03908aa8..18cffae4d2 100644
--- a/tests/regression/02-base/45-branched_thread_creation_return.c
+++ b/tests/regression/02-base/45-branched_thread_creation_return.c
@@ -10,18 +10,28 @@ int glob2 = 9;
 
 int main() {
   int k;
+  int mt = 0;
   pthread_t id;
 
-  if (k)
+  if (k) {
+    mt = 1;
     pthread_create(&id, NULL, t_fun, NULL);
-  else
+  } else {
     glob1 = 4;
+  }
+
 
   // We need to side-effect glob1=4 upon the join here;
   // otherwise, the global invariant will still have glob1=3.
 
   k = glob1;
-  assert(k == 3); // UNKNOWN!
+  if(!mt) {
+    // If we are not multi-threaded, or are not sure if we are
+    if(k==3) {} else {
+      // This must be reachable
+      assert(1);
+    }
+  }
 
   k = glob2;
   assert(k == 9);
@@ -32,4 +42,3 @@ int main() {
 
   return 0;
 }
-
diff --git a/tests/regression/04-mutex/59-testfive-intervals.c b/tests/regression/04-mutex/59-testfive-intervals.c
new file mode 100644
index 0000000000..01d5963069
--- /dev/null
+++ b/tests/regression/04-mutex/59-testfive-intervals.c
@@ -0,0 +1,33 @@
+// PARAM: --enable ana.int.interval
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void lock() {
+  pthread_mutex_lock(&mutex);
+}
+
+void unlock() {
+  pthread_mutex_unlock(&mutex);
+}
+
+
+void *t_fun(void *arg) {
+  lock();
+  myglobal++; // NORACE
+  unlock();
+  return NULL;
+}
+
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  lock();
+  myglobal++; // NORACE
+  unlock();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/36-apron/01-octagon_simple.c b/tests/regression/36-apron/01-octagon_simple.c
index 1b19621696..3ea04d9aed 100644
--- a/tests/regression/36-apron/01-octagon_simple.c
+++ b/tests/regression/36-apron/01-octagon_simple.c
@@ -16,7 +16,7 @@ void main(void) {
     N = 8;
   } else {
     // is dead code but if that is detected or not depends on what we do in branch
-    // currenlty we can't detect this
+    // currently we can't detect this
     N = 42;
   }
 }
diff --git a/tests/regression/36-apron/09-branch.c b/tests/regression/36-apron/09-branch.c
index 05f4bf6a3d..ae4fb0c4d4 100644
--- a/tests/regression/36-apron/09-branch.c
+++ b/tests/regression/36-apron/09-branch.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 // Based on 01/35.
 extern int __VERIFIER_nondet_int();
 
diff --git a/tests/regression/36-apron/10-float.c b/tests/regression/36-apron/10-float.c
index 9fe7eacc7a..fcbe2e4cb7 100644
--- a/tests/regression/36-apron/10-float.c
+++ b/tests/regression/36-apron/10-float.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 // Copied from 01/45 for apron.
 #include <assert.h>
 
diff --git a/tests/regression/36-apron/11-traces-max-simple.c b/tests/regression/36-apron/11-traces-max-simple.c
index 818aa92929..820bb21fc9 100644
--- a/tests/regression/36-apron/11-traces-max-simple.c
+++ b/tests/regression/36-apron/11-traces-max-simple.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.c b/tests/regression/36-apron/12-traces-min-rpb1.c
index feee63e36d..8e338fde29 100644
--- a/tests/regression/36-apron/12-traces-min-rpb1.c
+++ b/tests/regression/36-apron/12-traces-min-rpb1.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/13-traces-min-rpb2.c b/tests/regression/36-apron/13-traces-min-rpb2.c
index 1e63e9e77b..e87f1fb5e0 100644
--- a/tests/regression/36-apron/13-traces-min-rpb2.c
+++ b/tests/regression/36-apron/13-traces-min-rpb2.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/14-traces-unprot.c b/tests/regression/36-apron/14-traces-unprot.c
index a541b39316..6ceaf806e1 100644
--- a/tests/regression/36-apron/14-traces-unprot.c
+++ b/tests/regression/36-apron/14-traces-unprot.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/15-globals-st.c b/tests/regression/36-apron/15-globals-st.c
index 6b94243e85..51aafeb62f 100644
--- a/tests/regression/36-apron/15-globals-st.c
+++ b/tests/regression/36-apron/15-globals-st.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --disable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --disable ana.int.interval
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/16-traces-unprot2.c b/tests/regression/36-apron/16-traces-unprot2.c
index 3090e2e0a4..d6c8b168d9 100644
--- a/tests/regression/36-apron/16-traces-unprot2.c
+++ b/tests/regression/36-apron/16-traces-unprot2.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/17-traces-rpb-litmus.c b/tests/regression/36-apron/17-traces-rpb-litmus.c
index c59fabc5f3..da565dedd5 100644
--- a/tests/regression/36-apron/17-traces-rpb-litmus.c
+++ b/tests/regression/36-apron/17-traces-rpb-litmus.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/18-branch2.c b/tests/regression/36-apron/18-branch2.c
index f7694a4223..dc87b31826 100644
--- a/tests/regression/36-apron/18-branch2.c
+++ b/tests/regression/36-apron/18-branch2.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 // Based on 36/09.
 extern int __VERIFIER_nondet_int();
 
diff --git a/tests/regression/36-apron/19-traces-other-rpb.c b/tests/regression/36-apron/19-traces-other-rpb.c
index 8991fc5d6b..34b173cbed 100644
--- a/tests/regression/36-apron/19-traces-other-rpb.c
+++ b/tests/regression/36-apron/19-traces-other-rpb.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/36-apron/20-traces-even-more-rpb.c b/tests/regression/36-apron/20-traces-even-more-rpb.c
index c65465dbef..c64f226817 100644
--- a/tests/regression/36-apron/20-traces-even-more-rpb.c
+++ b/tests/regression/36-apron/20-traces-even-more-rpb.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/21-traces-cluster-based.c b/tests/regression/36-apron/21-traces-cluster-based.c
index 9a9e670585..3b1d7b4a01 100644
--- a/tests/regression/36-apron/21-traces-cluster-based.c
+++ b/tests/regression/36-apron/21-traces-cluster-based.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c b/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c
index 14a334003a..ee782f7ef0 100644
--- a/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c
+++ b/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/23-traces-write-centered-problem.c b/tests/regression/36-apron/23-traces-write-centered-problem.c
index 1daf4eb620..cff838f2db 100644
--- a/tests/regression/36-apron/23-traces-write-centered-problem.c
+++ b/tests/regression/36-apron/23-traces-write-centered-problem.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/24-combine-no-lval.c b/tests/regression/36-apron/24-combine-no-lval.c
index 58fb7ef5c6..890da92adb 100644
--- a/tests/regression/36-apron/24-combine-no-lval.c
+++ b/tests/regression/36-apron/24-combine-no-lval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/25-combine-global.c b/tests/regression/36-apron/25-combine-global.c
index 5dcea56f39..886e6ef38c 100644
--- a/tests/regression/36-apron/25-combine-global.c
+++ b/tests/regression/36-apron/25-combine-global.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/26-combine-forget-local-lval.c b/tests/regression/36-apron/26-combine-forget-local-lval.c
index 0da0bf492f..b286947e31 100644
--- a/tests/regression/36-apron/26-combine-forget-local-lval.c
+++ b/tests/regression/36-apron/26-combine-forget-local-lval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 #include <assert.h>
 
 int f(int x) {
diff --git a/tests/regression/36-apron/27-combine-forget-fun-lval.c b/tests/regression/36-apron/27-combine-forget-fun-lval.c
index a8f61ded18..cf0e55fa4f 100644
--- a/tests/regression/36-apron/27-combine-forget-fun-lval.c
+++ b/tests/regression/36-apron/27-combine-forget-fun-lval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 #include <assert.h>
 
 int f(int x) {
diff --git a/tests/regression/36-apron/28-combine-forget-fun-lval-imprecise.c b/tests/regression/36-apron/28-combine-forget-fun-lval-imprecise.c
index 87101539b9..3620185dfa 100644
--- a/tests/regression/36-apron/28-combine-forget-fun-lval-imprecise.c
+++ b/tests/regression/36-apron/28-combine-forget-fun-lval-imprecise.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/29-combine-arg-var-conflict.c b/tests/regression/36-apron/29-combine-arg-var-conflict.c
index 33080b9069..20bb42e6e6 100644
--- a/tests/regression/36-apron/29-combine-arg-var-conflict.c
+++ b/tests/regression/36-apron/29-combine-arg-var-conflict.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/30-return-global.c b/tests/regression/36-apron/30-return-global.c
index 41906aacd6..a43785c546 100644
--- a/tests/regression/36-apron/30-return-global.c
+++ b/tests/regression/36-apron/30-return-global.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/31-combine-global-lval.c b/tests/regression/36-apron/31-combine-global-lval.c
index f0c2cf8eae..c2fd156628 100644
--- a/tests/regression/36-apron/31-combine-global-lval.c
+++ b/tests/regression/36-apron/31-combine-global-lval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/32-typedef.c b/tests/regression/36-apron/32-typedef.c
index e53ef8c3e9..9cce8e1b5a 100644
--- a/tests/regression/36-apron/32-typedef.c
+++ b/tests/regression/36-apron/32-typedef.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 // extracted from sv-benchmarks float-newlib/double_req_bl_0210.c
 #include <assert.h>
 
diff --git a/tests/regression/36-apron/33-large-int64.c b/tests/regression/36-apron/33-large-int64.c
index c880fb6779..1fbc5b548f 100644
--- a/tests/regression/36-apron/33-large-int64.c
+++ b/tests/regression/36-apron/33-large-int64.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 #include <assert.h>
 
 void main() {
diff --git a/tests/regression/36-apron/34-large-bigint.c b/tests/regression/36-apron/34-large-bigint.c
index aa759c1b96..a27b05ba2d 100644
--- a/tests/regression/36-apron/34-large-bigint.c
+++ b/tests/regression/36-apron/34-large-bigint.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 #include <assert.h>
 
 void main() {
diff --git a/tests/regression/36-apron/35-rational-value.c b/tests/regression/36-apron/35-rational-value.c
index 369497ee65..4340af3618 100644
--- a/tests/regression/36-apron/35-rational-value.c
+++ b/tests/regression/36-apron/35-rational-value.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/36-special-unknown-globals.c b/tests/regression/36-apron/36-special-unknown-globals.c
index 2fdae17a65..db1af9c710 100644
--- a/tests/regression/36-apron/36-special-unknown-globals.c
+++ b/tests/regression/36-apron/36-special-unknown-globals.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/37-special-unknown-lval.c b/tests/regression/36-apron/37-special-unknown-lval.c
index 976b4dcedb..1e2d239f80 100644
--- a/tests/regression/36-apron/37-special-unknown-lval.c
+++ b/tests/regression/36-apron/37-special-unknown-lval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/38-branch-global.c b/tests/regression/36-apron/38-branch-global.c
index 5ed81bfc53..cda8e26183 100644
--- a/tests/regression/36-apron/38-branch-global.c
+++ b/tests/regression/36-apron/38-branch-global.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval
 int ARR_SIZE ;
 
 int main() {
@@ -7,4 +7,4 @@ int main() {
         count++;
     }
     return 0 ;
-}
\ No newline at end of file
+}
diff --git a/tests/regression/36-apron/39-enter-global-arg.c b/tests/regression/36-apron/39-enter-global-arg.c
index e29873f932..1cae0a40f6 100644
--- a/tests/regression/36-apron/39-enter-global-arg.c
+++ b/tests/regression/36-apron/39-enter-global-arg.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/40-rational-bounds.c b/tests/regression/36-apron/40-rational-bounds.c
index cf912a3d06..aee625c62d 100644
--- a/tests/regression/36-apron/40-rational-bounds.c
+++ b/tests/regression/36-apron/40-rational-bounds.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/41-threadenter-no-locals.c b/tests/regression/36-apron/41-threadenter-no-locals.c
index 7be6f0bb01..37e42659cf 100644
--- a/tests/regression/36-apron/41-threadenter-no-locals.c
+++ b/tests/regression/36-apron/41-threadenter-no-locals.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/42-threadenter-arg.c b/tests/regression/36-apron/42-threadenter-arg.c
index 570fb5d758..a47f348d0a 100644
--- a/tests/regression/36-apron/42-threadenter-arg.c
+++ b/tests/regression/36-apron/42-threadenter-arg.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/36-apron/45-context.c b/tests/regression/36-apron/45-context.c
index 5b78acccfe..04d2a35414 100644
--- a/tests/regression/36-apron/45-context.c
+++ b/tests/regression/36-apron/45-context.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval --enable ana.apron.context
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.apron.context
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
@@ -22,4 +22,4 @@ void main() {
   }
 
   res = oct(x, y);
-}
\ No newline at end of file
+}
diff --git a/tests/regression/36-apron/46-no-context.c b/tests/regression/36-apron/46-no-context.c
index a3f555a153..4792f78a77 100644
--- a/tests/regression/36-apron/46-no-context.c
+++ b/tests/regression/36-apron/46-no-context.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval --disable ana.apron.context
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.apron.context
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
@@ -22,4 +22,4 @@ void main() {
   }
 
   res = oct(x, y);
-}
\ No newline at end of file
+}
diff --git a/tests/regression/36-apron/47-no-context-attribute.c b/tests/regression/36-apron/47-no-context-attribute.c
index 81832e84b0..724e0407ed 100644
--- a/tests/regression/36-apron/47-no-context-attribute.c
+++ b/tests/regression/36-apron/47-no-context-attribute.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval --enable ana.apron.context
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.apron.context
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
@@ -23,4 +23,4 @@ void main() {
   }
 
   res = oct(x, y);
-}
\ No newline at end of file
+}
diff --git a/tests/regression/36-apron/48-context-attribute.c b/tests/regression/36-apron/48-context-attribute.c
index 421403b409..7b70b23074 100644
--- a/tests/regression/36-apron/48-context-attribute.c
+++ b/tests/regression/36-apron/48-context-attribute.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval --disable ana.apron.context
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.apron.context
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
@@ -23,4 +23,4 @@ void main() {
   }
 
   res = oct(x, y);
-}
\ No newline at end of file
+}
diff --git a/tests/regression/36-apron/50-evalint.c b/tests/regression/36-apron/50-evalint.c
index 9251358c6b..37dc546e03 100644
--- a/tests/regression/36-apron/50-evalint.c
+++ b/tests/regression/36-apron/50-evalint.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/60-evalint-interval.c b/tests/regression/36-apron/60-evalint-interval.c
index 8ae347edc3..8b12453478 100644
--- a/tests/regression/36-apron/60-evalint-interval.c
+++ b/tests/regression/36-apron/60-evalint-interval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval
 extern int __VERIFIER_nondet_int();
 
 #include <assert.h>
diff --git a/tests/regression/36-apron/61-branched.c b/tests/regression/36-apron/61-branched.c
index ffe825107b..bdce6042dc 100644
--- a/tests/regression/36-apron/61-branched.c
+++ b/tests/regression/36-apron/61-branched.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>
diff --git a/tests/regression/36-apron/62-branched_intricate.c b/tests/regression/36-apron/62-branched_intricate.c
index 435d40754f..6f6b4043a9 100644
--- a/tests/regression/36-apron/62-branched_intricate.c
+++ b/tests/regression/36-apron/62-branched_intricate.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>
@@ -14,15 +14,22 @@ int main(void)
 {
     pthread_t t;
     int i = __VERIFIER_nondet_int(); //rand
+    int mt = 0;
 
     if(i < 1) {
         pthread_create(&t, ((void *)0), t_fun, ((void *)0));
         assert(global == 0); //UNKNOWN!
         i++;
+        mt=1;
     } else {
         global = 17;
     }
 
-    assert(global <= 5); //UNKNOWN!
+    if(!mt) {
+        if(global<=5) {} else {
+            assert(1); // There must be a path that reaches this
+        }
+    }
+
     return 0;
 }
diff --git a/tests/regression/36-apron/63-branched-not-too-brutal.c b/tests/regression/36-apron/63-branched-not-too-brutal.c
index e029d3c5dd..647783316f 100644
--- a/tests/regression/36-apron/63-branched-not-too-brutal.c
+++ b/tests/regression/36-apron/63-branched-not-too-brutal.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
diff --git a/tests/regression/36-apron/69-evalint-overflow.c b/tests/regression/36-apron/69-evalint-overflow.c
index c10c23ac58..c03d947898 100644
--- a/tests/regression/36-apron/69-evalint-overflow.c
+++ b/tests/regression/36-apron/69-evalint-overflow.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval
 int main(void) {
   unsigned int x = 10;
 
diff --git a/tests/regression/36-apron/70-signed-overflows.c b/tests/regression/36-apron/70-signed-overflows.c
index 04e12c05ac..39459031b6 100644
--- a/tests/regression/36-apron/70-signed-overflows.c
+++ b/tests/regression/36-apron/70-signed-overflows.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none --disable ana.int.interval
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --disable ana.int.interval
 // copied from signed-overflows/intervals for apron
 int main(void) {
     int x = 0;
diff --git a/tests/regression/36-apron/71-tid-toy1.c b/tests/regression/36-apron/71-tid-toy1.c
new file mode 100644
index 0000000000..8ccf8973f5
--- /dev/null
+++ b/tests/regression/36-apron/71-tid-toy1.c
@@ -0,0 +1,43 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int t, r; // rand
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  g = 31;
+  h = 17;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); // t_fun always has the invariant it only is violated in main temporarily
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/72-tid-toy2.c b/tests/regression/36-apron/72-tid-toy2.c
new file mode 100644
index 0000000000..202af5d782
--- /dev/null
+++ b/tests/regression/36-apron/72-tid-toy2.c
@@ -0,0 +1,44 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int t; // rand
+  pthread_mutex_lock(&A);
+  g = 31;
+  h = 17;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN! This thread is multiple and needs to read from itself
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id[10];
+  for(int i = 0; i < 10;i++){
+    pthread_create(&id[i], NULL, t_fun, NULL);
+  }
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/73-tid-toy3.c b/tests/regression/36-apron/73-tid-toy3.c
new file mode 100644
index 0000000000..1b13913a52
--- /dev/null
+++ b/tests/regression/36-apron/73-tid-toy3.c
@@ -0,0 +1,43 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  g = 12;
+  h = 14;
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //FAIL
+  pthread_mutex_unlock(&A);
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //FAIL
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/74-tid-curious.c b/tests/regression/36-apron/74-tid-curious.c
new file mode 100644
index 0000000000..9d09ccea63
--- /dev/null
+++ b/tests/regression/36-apron/74-tid-curious.c
@@ -0,0 +1,29 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  // Missing unlock(!)
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //This succeeds as it can only be entered before t_fun grabs &A and never releases it again
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/75-tid-toy5.c b/tests/regression/36-apron/75-tid-toy5.c
new file mode 100644
index 0000000000..45a19423bf
--- /dev/null
+++ b/tests/regression/36-apron/75-tid-toy5.c
@@ -0,0 +1,54 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_benign(void *arg) {
+  return NULL;
+}
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //FAIL
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/76-tid-toy6.c b/tests/regression/36-apron/76-tid-toy6.c
new file mode 100644
index 0000000000..84c303e335
--- /dev/null
+++ b/tests/regression/36-apron/76-tid-toy6.c
@@ -0,0 +1,65 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_benign(void *arg) {
+  return NULL;
+}
+
+void *t_more(void *arg) {
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_fun(void *arg) {
+  pthread_t more;
+  pthread_create(&more, NULL, t_more, NULL);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //FAIL
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/77-tid-toy7.c b/tests/regression/36-apron/77-tid-toy7.c
new file mode 100644
index 0000000000..86226b124a
--- /dev/null
+++ b/tests/regression/36-apron/77-tid-toy7.c
@@ -0,0 +1,76 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_benign(void *arg) {
+  return NULL;
+}
+
+void *t_more(void *arg) {
+  // t_more is started multiple times, assert does not need to hold
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_fun(void *arg) {
+  // t_more has not been started yet
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  pthread_t more[10];
+
+  for(int i = 0; i <10;i++) {
+    pthread_create(&more[i], NULL, t_more, NULL);
+    pthread_mutex_lock(&A);
+    assert(g == h); //UNKNOWN!
+    pthread_mutex_unlock(&A);
+  }
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/78-tid-toy8.c b/tests/regression/36-apron/78-tid-toy8.c
new file mode 100644
index 0000000000..a48b35b8a1
--- /dev/null
+++ b/tests/regression/36-apron/78-tid-toy8.c
@@ -0,0 +1,66 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_benign(void *arg) {
+  return NULL;
+}
+
+
+void *t_more(void *arg) {
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_fun(void *arg) {
+  // t_more may be started by the main thread!
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+
+  pthread_mutex_lock(&A);
+  g = t;
+  h = t;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_more, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/79-tid-toy9.c b/tests/regression/36-apron/79-tid-toy9.c
new file mode 100644
index 0000000000..8420048f6f
--- /dev/null
+++ b/tests/regression/36-apron/79-tid-toy9.c
@@ -0,0 +1,36 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_benign(void *arg) {
+  pthread_mutex_lock(&A);
+  g = 10;
+  h = 10;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+  pthread_join(id2, NULL);
+
+  // This one succeeds despite what is described in the paper, and even without the must-join analysis :)
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/80-tid-toy10.c b/tests/regression/36-apron/80-tid-toy10.c
new file mode 100644
index 0000000000..b1eefcb67c
--- /dev/null
+++ b/tests/regression/36-apron/80-tid-toy10.c
@@ -0,0 +1,45 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_benign(void *arg) {
+  pthread_mutex_lock(&A);
+  g = 10;
+  h = 10;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  pthread_join(id2, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //FAIL
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/81-tid-toy11.c b/tests/regression/36-apron/81-tid-toy11.c
new file mode 100644
index 0000000000..884912b9ff
--- /dev/null
+++ b/tests/regression/36-apron/81-tid-toy11.c
@@ -0,0 +1,77 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+pthread_t other_t;
+
+void *t_fun(void *arg) {
+  int x;
+  int y;
+
+  pthread_mutex_lock(&A);
+  g = x;
+  h = y;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = x;
+  h = x;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  // Without this, it would even succeed without the must joined analysis.
+  // With it, that is required!
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  pthread_create(&other_t, NULL, t_fun, NULL);
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = 10;
+  h = 10;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_join(id2, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); // UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  pthread_join(other_t, NULL);
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/82-tid-toy12.c b/tests/regression/36-apron/82-tid-toy12.c
new file mode 100644
index 0000000000..14ca64dc97
--- /dev/null
+++ b/tests/regression/36-apron/82-tid-toy12.c
@@ -0,0 +1,79 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+pthread_t other_t;
+
+void *t_fun(void *arg) {
+  int x;
+  int y;
+
+  pthread_mutex_lock(&A);
+  g = x;
+  h = y;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = x;
+  h = x;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  // Without this, it would even succeed without the must joined analysis.
+  // With it, that is required!
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  pthread_create(&other_t, NULL, t_fun, NULL);
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = 10;
+  h = 10;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  pthread_t id3;
+  pthread_create(&id2, NULL, t_benign, NULL);
+  pthread_create(&id3, NULL, t_benign, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_join(id2, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); // UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  pthread_join(other_t, NULL);
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); // UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/83-tid-toy13.c b/tests/regression/36-apron/83-tid-toy13.c
new file mode 100644
index 0000000000..b64a7731ff
--- /dev/null
+++ b/tests/regression/36-apron/83-tid-toy13.c
@@ -0,0 +1,79 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+pthread_t other_t;
+
+void *t_fun(void *arg) {
+  int x;
+  int y;
+
+  pthread_mutex_lock(&A);
+  g = x;
+  h = y;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = x;
+  h = x;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  // Without this, it would even succeed without the must joined analysis.
+  // With it, that is required!
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  pthread_create(&other_t, NULL, t_fun, NULL);
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  g = 10;
+  h = 10;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_mutex_lock(&A);
+  g = 12;
+  h = 14;
+  pthread_mutex_unlock(&A);
+
+  // Force multi-threaded handling
+  pthread_t id2;
+  for(int i = 0; i < 10;i++) {
+    pthread_create(&id2, NULL, t_benign, NULL);
+  }
+
+  pthread_mutex_lock(&A);
+  assert(g == h); //UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_join(id2, NULL);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); // UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  pthread_join(other_t, NULL);
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h); // UNKNOWN!
+  pthread_mutex_unlock(&A);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/84-problem-0402.c b/tests/regression/36-apron/84-problem-0402.c
new file mode 100644
index 0000000000..6023ab6470
--- /dev/null
+++ b/tests/regression/36-apron/84-problem-0402.c
@@ -0,0 +1,24 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins
+// fixed with issue 389
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return 0;
+}
diff --git a/tests/regression/36-apron/85-problem-0405.c b/tests/regression/36-apron/85-problem-0405.c
new file mode 100644
index 0000000000..c132a48629
--- /dev/null
+++ b/tests/regression/36-apron/85-problem-0405.c
@@ -0,0 +1,33 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins --set exp.solver.td3.side_widen sides-pp
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void lock() {
+  pthread_mutex_lock(&mutex);
+}
+
+void unlock() {
+  pthread_mutex_unlock(&mutex);
+}
+
+
+void *t_fun(void *arg) {
+  lock();
+  myglobal++; // NORACE
+  unlock();
+  return NULL;
+}
+
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  lock();
+  myglobal++; // NORACE
+  unlock();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/36-apron/86-branched-thread-creation.c b/tests/regression/36-apron/86-branched-thread-creation.c
new file mode 100644
index 0000000000..2ed80ebf9c
--- /dev/null
+++ b/tests/regression/36-apron/86-branched-thread-creation.c
@@ -0,0 +1,48 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+int h;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int t;
+
+  pthread_mutex_lock(&mutex);
+  g=t;
+  h=t;
+  pthread_mutex_unlock(&mutex);
+  return NULL;
+}
+
+
+int main(void) {
+  int top;
+  int mt = 0;
+
+  if(top) {
+
+    g = 8;
+    h = 7;
+
+  } else {
+    pthread_t id;
+    pthread_create(&id, NULL, t_fun, NULL);
+
+    pthread_mutex_lock(&mutex);
+    g=top;
+    h=top;
+    pthread_mutex_unlock(&mutex);
+    mt=1;
+  }
+
+  if(!mt) {
+    pthread_mutex_lock(&mutex);
+    assert(g==h); //MAYFAIL
+    pthread_mutex_unlock(&mutex);
+  }
+
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/87-sync.c b/tests/regression/36-apron/87-sync.c
new file mode 100644
index 0000000000..c53c4c6e90
--- /dev/null
+++ b/tests/regression/36-apron/87-sync.c
@@ -0,0 +1,39 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins --sets exp.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+int h;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex);
+  assert(g==h);
+  pthread_mutex_unlock(&mutex);
+  return NULL;
+}
+
+
+int main(void) {
+  int top, top2;
+
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&mutex);
+  if(top2) {
+    g=34;
+    h=77;
+  }
+
+  g=top;
+  h=top;
+  pthread_mutex_unlock(&mutex);
+
+  pthread_mutex_lock(&mutex);
+  assert(g==h);
+  pthread_mutex_unlock(&mutex);
+
+  return 0;
+}
diff --git a/tests/regression/36-apron/88-mine14-no-threshhold.c b/tests/regression/36-apron/88-mine14-no-threshhold.c
new file mode 100644
index 0000000000..37a0d2ee74
--- /dev/null
+++ b/tests/regression/36-apron/88-mine14-no-threshhold.c
@@ -0,0 +1,33 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins
+#include <pthread.h>
+#include <stdio.h>
+
+int x;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x<100) {
+      x++;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+
+int main(void) {
+  int top, top2;
+
+
+  pthread_t id;
+  pthread_t id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex);
+  assert(x <= 100); // TODO
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/36-apron/89-mine14.c b/tests/regression/36-apron/89-mine14.c
new file mode 100644
index 0000000000..e1f70b2344
--- /dev/null
+++ b/tests/regression/36-apron/89-mine14.c
@@ -0,0 +1,34 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins --enable ana.apron.threshold_widening
+// Fig 5a from Miné 2014
+#include <pthread.h>
+#include <stdio.h>
+
+int x;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x<100) {
+      x++;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+
+int main(void) {
+  int top, top2;
+
+
+  pthread_t id;
+  pthread_t id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex);
+  assert(x <= 100);
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/36-apron/90-mine14-5b.c b/tests/regression/36-apron/90-mine14-5b.c
new file mode 100644
index 0000000000..281d1b87c8
--- /dev/null
+++ b/tests/regression/36-apron/90-mine14-5b.c
@@ -0,0 +1,50 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins --enable ana.apron.threshold_widening
+// Fig 5 from Miné 2014
+#include <pthread.h>
+#include <stdio.h>
+
+int x;
+int y;
+int hundred = 100;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x>0) {
+      x = x-1;
+      y = y-1;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+void *t_fun2(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x<10) {
+      x = x+1;
+      y = y+1;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+
+int main(void) {
+  int top, top2;
+
+
+  pthread_t id;
+  pthread_t id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun2, NULL);
+  pthread_mutex_lock(&mutex);
+  assert(x==y);
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/36-apron/91-mine14-5b-no-threshhold.c b/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
new file mode 100644
index 0000000000..5a2ee01822
--- /dev/null
+++ b/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
@@ -0,0 +1,51 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] threadJoins --disable ana.apron.threshold_widening
+// Fig 5 from Miné 2014
+// This only succeeds if we use a different widening strategy (no widening :())
+#include <pthread.h>
+#include <stdio.h>
+
+int x;
+int y;
+int hundred = 100;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x>0) {
+      x = x-1;
+      y = y-1;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+void *t_fun2(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x<10) {
+      x = x+1;
+      y = y+1;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+
+int main(void) {
+  int top, top2;
+
+
+  pthread_t id;
+  pthread_t id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun2, NULL);
+  pthread_mutex_lock(&mutex);
+  assert(x==y); //TODO
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}
diff --git a/tests/regression/36-apron/92-traces-mutex-meet-cluster2.c b/tests/regression/36-apron/92-traces-mutex-meet-cluster2.c
new file mode 100644
index 0000000000..d9b6cfd070
--- /dev/null
+++ b/tests/regression/36-apron/92-traces-mutex-meet-cluster2.c
@@ -0,0 +1,44 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid-cluster12
+extern int __VERIFIER_nondet_int();
+
+#include <pthread.h>
+#include <assert.h>
+
+int g = 0;
+int h = 0;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&A);
+  g = 16;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+void *t_fun2(void *arg) {
+  pthread_mutex_lock(&A);
+  h = __VERIFIER_nondet_int();
+  h = 12;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun2, NULL);
+
+  pthread_mutex_lock(&A);
+  h = 31;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  h = 12;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  int z = h;
+  assert(z != 31);
+  pthread_mutex_unlock(&A);
+  return 0;
+}
diff --git a/tests/regression/36-apron/93-traces-mutex-meet-cluster12.c b/tests/regression/36-apron/93-traces-mutex-meet-cluster12.c
new file mode 100644
index 0000000000..31c44ee083
--- /dev/null
+++ b/tests/regression/36-apron/93-traces-mutex-meet-cluster12.c
@@ -0,0 +1,43 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --sets exp.apron.privatization mutex-meet-tid-cluster12
+extern int __VERIFIER_nondet_int();
+
+#include <pthread.h>
+#include <assert.h>
+
+int g = 0;
+int h = 0;
+int i = 0;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int x;
+  pthread_mutex_lock(&A);
+  x = h;
+  i = x;
+  pthread_mutex_unlock(&A);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  g = __VERIFIER_nondet_int();
+  h = __VERIFIER_nondet_int();
+  i = __VERIFIER_nondet_int();
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  int y = __VERIFIER_nondet_int();
+  g = y;
+  h = y;
+  i = y;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  assert(g == h);
+  assert(h == i);
+  pthread_mutex_unlock(&A);
+  return 0;
+}
diff --git a/tests/regression/36-apron/71-simple-apron-interval.c b/tests/regression/36-apron/94-simple-apron-interval.c
similarity index 100%
rename from tests/regression/36-apron/71-simple-apron-interval.c
rename to tests/regression/36-apron/94-simple-apron-interval.c
diff --git a/tests/regression/36-apron/72-simple-polyhedra.c b/tests/regression/36-apron/95-simple-polyhedra.c
similarity index 100%
rename from tests/regression/36-apron/72-simple-polyhedra.c
rename to tests/regression/36-apron/95-simple-polyhedra.c
diff --git a/tests/regression/37-congruence/07-refinements-o.c b/tests/regression/37-congruence/07-refinements-o.c
index 10a440c5e9..bd4a931b36 100644
--- a/tests/regression/37-congruence/07-refinements-o.c
+++ b/tests/regression/37-congruence/07-refinements-o.c
@@ -21,6 +21,7 @@ void unsignedCase() {
     assert(i == 0);
 
     if(top % 3 == 17) {
+        // This is unreachable in the concrete!
         assert(top%17 == 3); //UNKNOWN!
     }
 }
@@ -47,6 +48,7 @@ int main() {
     assert(i == 0);
 
     if(top % 3 == 17) {
+        // This is unreachable in the concrete!
         assert(top%17 == 3); //UNKNOWN!
     }
 
diff --git a/tests/regression/52-apron-mukherjee/01-mukherjee_reorder_2.c b/tests/regression/52-apron-mukherjee/01-mukherjee_reorder_2.c
new file mode 100644
index 0000000000..1b79d17e0c
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/01-mukherjee_reorder_2.c
@@ -0,0 +1,70 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+
+static int a = 0;
+static int b = 0;
+
+pthread_mutex_t mut_lock = PTHREAD_MUTEX_INITIALIZER;
+
+void *iSet_1(void *param);
+void *iSet_2(void *param);
+void *iCheck_1(void *param);
+void *iCheck_2(void *param);
+
+int main(int argc, char *argv[]) {
+    int i, err;
+
+    pthread_t t1;
+    pthread_t t2;
+    pthread_t t3;
+    pthread_t t4;
+
+    pthread_create(&t1, NULL, &iSet_1, NULL);
+    pthread_create(&t2, NULL, &iSet_2, NULL);
+    pthread_create(&t3, NULL, &iCheck_1, NULL);
+    pthread_create(&t4, NULL, &iCheck_2, NULL);
+
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+    pthread_join(t3, NULL);
+    pthread_join(t4, NULL);
+
+
+    return 0;
+}
+
+void *iSet_1(void *param) {
+    pthread_mutex_lock(&mut_lock);
+    a = 1;
+    b = -1;
+    pthread_mutex_unlock(&mut_lock);
+    return NULL;
+}
+
+void *iSet_2(void *param) {
+    pthread_mutex_lock(&mut_lock);
+    a = 1;
+    b = -1;
+    pthread_mutex_unlock(&mut_lock);
+    return NULL;
+}
+
+void *iCheck_1(void *param) {
+    pthread_mutex_lock(&mut_lock);
+    assert(a + b == 0);
+    pthread_mutex_unlock(&mut_lock);
+
+    return NULL;
+}
+
+void *iCheck_2(void *param) {
+    pthread_mutex_lock(&mut_lock);
+    assert(a + b == 0);
+    pthread_mutex_unlock(&mut_lock);
+
+    return NULL;
+}
diff --git a/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c b/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
new file mode 100644
index 0000000000..2d17d7ee99
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
@@ -0,0 +1,143 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets exp.apron.privatization mutex-meet-tid
+
+#include <stdlib.h>
+#include <pthread.h>
+#include <string.h>
+#include <assert.h>
+
+const int SIGMA = 4;
+
+int array_0, array_1, array_2, array_3;
+int array_index;
+
+pthread_mutex_t mut_lock = PTHREAD_MUTEX_INITIALIZER;
+
+void *thread1(void * arg)
+{
+    assert(array_index <= 4);
+    pthread_mutex_lock(&mut_lock);
+	switch (array_index) {
+        case 0:
+            array_0 = 1;
+            break;
+        case 1:
+            array_1 = 1;
+            break;
+        case 2:
+            array_2 = 1;
+            break;
+        case 3:
+            array_3 = 1;
+            break;
+    }
+    pthread_mutex_unlock(&mut_lock);
+	return 0;
+}
+
+void *thread2(void * arg)
+{
+    assert(array_index <= 4);
+    pthread_mutex_lock(&mut_lock);
+	switch (array_index) {
+        case 0:
+            array_0 = 1;
+            break;
+        case 1:
+            array_1 = 1;
+            break;
+        case 2:
+            array_2 = 1;
+            break;
+        case 3:
+            array_3 = 1;
+            break;
+    }
+    pthread_mutex_unlock(&mut_lock);
+	return 0;
+}
+
+void *thread3(void * arg)
+{
+    assert(array_index <= 4);
+    pthread_mutex_lock(&mut_lock);
+	switch (array_index) {
+        case 0:
+            array_0 = 1;
+            break;
+        case 1:
+            array_1 = 1;
+            break;
+        case 2:
+            array_2 = 1;
+            break;
+        case 3:
+            array_3 = 1;
+            break;
+    }
+    pthread_mutex_unlock(&mut_lock);
+	return 0;
+}
+
+void *thread4(void * arg)
+{
+    assert(array_index <= 4);
+    pthread_mutex_lock(&mut_lock);
+	switch (array_index) {
+        case 0:
+            array_0 = 1;
+            break;
+        case 1:
+            array_1 = 1;
+            break;
+        case 2:
+            array_2 = 1;
+            break;
+        case 3:
+            array_3 = 1;
+            break;
+    }
+    pthread_mutex_unlock(&mut_lock);
+	return 0;
+}
+
+
+int main()
+{
+	int sum;
+
+	pthread_t t1;
+    pthread_t t2;
+    pthread_t t3;
+    pthread_t t4;
+
+    pthread_create(&t1, 0, thread1, 0);
+    pthread_mutex_lock(&mut_lock);
+    array_index++;
+    pthread_mutex_unlock(&mut_lock);
+
+    pthread_create(&t2, 0, thread2, 0);
+    pthread_mutex_lock(&mut_lock);
+    array_index++;
+    pthread_mutex_unlock(&mut_lock);
+
+    pthread_create(&t3, 0, thread3, 0);
+    pthread_mutex_lock(&mut_lock);
+    array_index++;
+    pthread_mutex_unlock(&mut_lock);
+
+    pthread_create(&t4, 0, thread4, 0);
+    pthread_mutex_lock(&mut_lock);
+    array_index++;
+    pthread_mutex_unlock(&mut_lock);
+
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    pthread_join(t3, 0);
+    pthread_join(t4, 0);
+
+	sum = array_0 + array_1 + array_2 + array_3;
+
+	assert(sum == SIGMA);  //UNKNOWN! <-- wrong, different threads might use the same array offset when writing
+
+	return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/03-mukherjee_sssc12.c b/tests/regression/52-apron-mukherjee/03-mukherjee_sssc12.c
new file mode 100644
index 0000000000..3320835be1
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/03-mukherjee_sssc12.c
@@ -0,0 +1,68 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set sem.int.signed_overflow assume_none
+
+#include <pthread.h>
+#include <assert.h>
+
+volatile int len;
+volatile int next;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* thr1(void* arg) {
+    int c, end, temp;
+    c = 0;
+    end = 0;
+    pthread_mutex_lock(&lock);
+    temp = len;
+
+    if(next + 10 <= len) {
+        c = next;
+        end = next + 10;
+        next = next + 10;
+    }
+    pthread_mutex_unlock(&lock);
+
+    while(c < end) {
+        assert(c >= 0);
+        assert(c <= temp);
+        c = c +1;
+    }
+    return NULL;
+}
+
+void* thr2(void* arg) {
+    int c, end, temp;
+    c = 0;
+    end = 0;
+    pthread_mutex_lock(&lock);
+    temp = len;
+
+    if(next + 10 <= len) {
+        c = next;
+        end = next + 10;
+        next = next + 10;
+    }
+    pthread_mutex_unlock(&lock);
+
+    while(c < end) {
+        assert(c >= 0);
+        assert(c <= temp);
+        c = c +1;
+    }
+    return NULL;
+}
+
+int main(int argc, char* argv[]) {
+    pthread_t t1;
+    pthread_t t2;
+    next = 0;
+    int t;
+    len = t;
+    if (len > 0) {
+	    pthread_create(&t1, 0, thr1, 0);
+	    pthread_create(&t2, 0, thr2, 0);
+        pthread_join(t1, 0);
+        pthread_join(t2, 0);
+    }
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/04-mukherjee_spin2003.c b/tests/regression/52-apron-mukherjee/04-mukherjee_spin2003.c
new file mode 100644
index 0000000000..c878ec5aeb
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/04-mukherjee_spin2003.c
@@ -0,0 +1,39 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+
+#include <pthread.h>
+#include <assert.h>
+
+unsigned int x;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_Spin(void* arg){
+    pthread_mutex_lock(&lock);
+    x = 0;
+    x = 1;
+
+    assert(x >= 1);
+    pthread_mutex_unlock(&lock);
+    return NULL;
+}
+
+void* T2_Spin(void* arg){
+    pthread_mutex_lock(&lock);
+    x = 0;
+    x = 1;
+
+    assert(x >= 1);
+    pthread_mutex_unlock(&lock);
+    return NULL;
+}
+
+int main(){
+    x = 1;
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_Spin, 0);
+    pthread_create(&t2, 0, T2_Spin, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/05-mukherjee_simpleLoop.c b/tests/regression/52-apron-mukherjee/05-mukherjee_simpleLoop.c
new file mode 100644
index 0000000000..79a5d69552
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/05-mukherjee_simpleLoop.c
@@ -0,0 +1,52 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set sem.int.signed_overflow assume_none
+
+#include <pthread.h>
+#include <assert.h>
+
+unsigned int x, y, z;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_SL(void* arg){
+    int i = 0, j = 0, k = 0;
+
+    for(i = 0; i < x; i++) {
+        for(j = i + 1; j < y; j++) {
+            for(k = j; k < z; k++) {
+                pthread_mutex_lock(&lock);
+                assert(k > i);
+                pthread_mutex_unlock(&lock);
+            }
+        }
+    }
+    return NULL;
+}
+
+void* T2_SL(void* arg){
+    int i = 0, j = 0, k = 0;
+
+    for(i = 0; i < x; i++) {
+        for(j = i + 1; j < y; j++) {
+            for(k = j; k < z; k++) {
+                pthread_mutex_lock(&lock);
+                assert(k > i);
+                pthread_mutex_unlock(&lock);
+            }
+        }
+    }
+    return NULL;
+}
+
+int main(){
+    int top1, top2, top3;
+    x = top1;
+    y = top2;
+    z = top3;
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_SL, 0);
+    pthread_create(&t2, 0, T2_SL, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/06-mukherjee_simpleLoop5.c b/tests/regression/52-apron-mukherjee/06-mukherjee_simpleLoop5.c
new file mode 100644
index 0000000000..42e9e649ef
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/06-mukherjee_simpleLoop5.c
@@ -0,0 +1,57 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins  --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+unsigned int a, b, c;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_SL5(void* arg){
+    while(1) {
+        pthread_mutex_lock(&lock);
+        assert(a != b); //TODO   requires disjunctions
+        pthread_mutex_unlock(&lock);
+    }
+    return NULL;
+}
+
+void* T2_SL5(void* arg){
+    while(1) {
+        pthread_mutex_lock(&lock);
+        int temp = a;
+        a = b;
+        b = c;
+        c = temp;
+        pthread_mutex_unlock(&lock);
+    }
+    return NULL;
+}
+
+void* T3_SL5(void* arg){
+    while(1) {
+        pthread_mutex_lock(&lock);
+        int temp = a;
+        a = b;
+        b = c;
+        c = temp;
+        pthread_mutex_unlock(&lock);
+    }
+    return NULL;
+}
+
+int main(){
+    a = 1;
+    b = 2;
+    c = 3;
+    pthread_t t1;
+    pthread_t t2;
+    pthread_t t3;
+    pthread_create(&t1, 0, T1_SL5, 0);
+    pthread_create(&t2, 0, T2_SL5, 0);
+    pthread_create(&t3, 0, T3_SL5, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    pthread_join(t3, 0);
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/07-mukherjee_DoubleLock_P3.c b/tests/regression/52-apron-mukherjee/07-mukherjee_DoubleLock_P3.c
new file mode 100644
index 0000000000..384bccd89b
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/07-mukherjee_DoubleLock_P3.c
@@ -0,0 +1,40 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+
+#include <pthread.h>
+#include <assert.h>
+
+int count;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_DLP3(void* arg){
+    pthread_mutex_lock(&lock);
+    count++;
+    count--;
+    pthread_mutex_unlock(&lock);
+
+    pthread_mutex_lock(&lock);
+    count--;
+    count++;
+    pthread_mutex_unlock(&lock);
+    return NULL;
+}
+
+void* T2_DLP3(void* arg){
+    pthread_mutex_lock(&lock);
+    assert(count >= -1);
+    pthread_mutex_unlock(&lock);
+    return NULL;
+}
+
+int main(){
+    count = 0;
+
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_DLP3, 0);
+    pthread_create(&t2, 0, T2_DLP3, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/08-mukherjee_unverif.c b/tests/regression/52-apron-mukherjee/08-mukherjee_unverif.c
new file mode 100644
index 0000000000..a888419547
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/08-mukherjee_unverif.c
@@ -0,0 +1,53 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+unsigned int r = 0;
+unsigned int s = 0;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* thr1(void* arg){
+    pthread_mutex_lock(&lock);
+    r = r + 1;
+    pthread_mutex_unlock(&lock);
+    unsigned int l = 0;
+
+    pthread_mutex_lock(&lock);
+    if(r == 1){
+        s = s + 1;
+        l = l + 1;
+        assert(s == l); // TODO
+    }
+    pthread_mutex_unlock(&lock);
+
+    return 0;
+}
+
+void* thr2(void* arg){
+    pthread_mutex_lock(&lock);
+    r = r + 1;
+    pthread_mutex_unlock(&lock);
+    unsigned int l = 0;
+
+    pthread_mutex_lock(&lock);
+    if(r == 1){
+        s = s + 1;
+        l = l + 1;
+        assert(s == l);  // TODO
+    }
+    pthread_mutex_unlock(&lock);
+
+    return 0;
+}
+
+int main() {
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, thr1, 0);
+    pthread_create(&t2, 0, thr2, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/09-mukherjee_fib_Bench.c b/tests/regression/52-apron-mukherjee/09-mukherjee_fib_Bench.c
new file mode 100644
index 0000000000..06e81c1c1c
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/09-mukherjee_fib_Bench.c
@@ -0,0 +1,46 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+int i, j, NUM;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* W1_Fib_Bench_False_Unreach_Call(void* arg){
+    for(int k = 0; k < NUM; k++) {
+        pthread_mutex_lock(&lock);
+        i += j;
+        pthread_mutex_unlock(&lock);
+    }
+    return 0;
+}
+
+void* W2_Fib_Bench_False_Unreach_Call(void* arg){
+    for(int k = 0; k < NUM; k++) {
+        pthread_mutex_lock(&lock);
+        j += i;
+        pthread_mutex_unlock(&lock);
+    }
+    return 0;
+}
+
+
+int main() {
+    i = 1;
+    j = 1;
+
+    NUM = 5;
+
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, W1_Fib_Bench_False_Unreach_Call, 0);
+    pthread_create(&t2, 0, W2_Fib_Bench_False_Unreach_Call, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    assert(i < 144); //TODO
+    assert(j < 144); //TODO
+
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/10-mukherjee_fib_Bench_Longer.c b/tests/regression/52-apron-mukherjee/10-mukherjee_fib_Bench_Longer.c
new file mode 100644
index 0000000000..0da5a88ce9
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/10-mukherjee_fib_Bench_Longer.c
@@ -0,0 +1,46 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+int i, j, NUM;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* W1_Fib_Bench_False_Unreach_Call(void* arg){
+    for(int k = 0; k < NUM; k++) {
+        pthread_mutex_lock(&lock);
+        i += j;
+        pthread_mutex_unlock(&lock);
+    }
+    return 0;
+}
+
+void* W2_Fib_Bench_False_Unreach_Call(void* arg){
+    for(int k = 0; k < NUM; k++) {
+        pthread_mutex_lock(&lock);
+        j += i;
+        pthread_mutex_unlock(&lock);
+    }
+    return 0;
+}
+
+
+int main() {
+    i = 1;
+    j = 1;
+
+    NUM = 6;
+
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, W1_Fib_Bench_False_Unreach_Call, 0);
+    pthread_create(&t2, 0, W2_Fib_Bench_False_Unreach_Call, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    assert(i < 377); //TODO
+    assert(j < 377); //TODO
+
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/11-mukherjee_indexer.c b/tests/regression/52-apron-mukherjee/11-mukherjee_indexer.c
new file mode 100644
index 0000000000..ac7f984441
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/11-mukherjee_indexer.c
@@ -0,0 +1,78 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+
+#include <pthread.h>
+#include <assert.h>
+
+int MAX, SIZE, array;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* W1_Indexer(void* arg){
+    int m = 0;
+    int w = 0;
+    int h = 0, rv = 0;
+
+    while(m < MAX) {
+        w = (++m) * 12;
+        h = (w*7) % SIZE;
+
+        assert(h>=0);
+
+        rv = 0;
+        h = rv + 1;
+
+        while(rv == 0) {
+            pthread_mutex_lock(&lock);
+            if(array == 0) {
+                array = h;
+                rv = 1;
+            }
+            else
+                h = (h + 1) % SIZE;
+            pthread_mutex_unlock(&lock);
+        }
+    }
+    return 0;
+}
+
+void* W2_Indexer(void* arg){
+    int m = 0;
+    int w = 0;
+    int h = 0, rv = 0;
+
+    while(m < MAX) {
+        w = (++m) * 12;
+        h = (w*7) % SIZE;
+
+        assert(h>=0);
+
+        rv = 0;
+        h = rv + 1;
+
+        while(rv == 0) {
+            pthread_mutex_lock(&lock);
+            if(array == 0) {
+                array = h;
+                rv = 1;
+            }
+            else
+                h = (h + 1) % SIZE;
+            pthread_mutex_unlock(&lock);
+        }
+    }
+    return 0;
+}
+
+int main() {
+    SIZE = 128;
+    MAX = 4;
+    array = 0;
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, W1_Indexer, 0);
+    pthread_create(&t2, 0, W2_Indexer, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/12-mukherjee_twostage_3.c b/tests/regression/52-apron-mukherjee/12-mukherjee_twostage_3.c
new file mode 100644
index 0000000000..03d2f0862b
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/12-mukherjee_twostage_3.c
@@ -0,0 +1,64 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+int data1value = 0;
+int data2value = 0;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* iTThread_1(void* arg){
+    pthread_mutex_lock(&lock);
+    data1value = 1;
+    pthread_mutex_unlock(&lock);
+
+    pthread_mutex_lock(&lock);
+    data2value = data1value + 1;
+    pthread_mutex_unlock(&lock);
+    return 0;
+}
+
+void* iTThread_2(void* arg){
+    pthread_mutex_lock(&lock);
+    data1value = 1;
+    pthread_mutex_unlock(&lock);
+
+    pthread_mutex_lock(&lock);
+    data2value = data1value + 1;
+    pthread_mutex_unlock(&lock);
+	return 0;
+}
+
+void* iRThread_1(void* arg){
+	int t1 = -1;
+	int t2 = -1;
+
+	pthread_mutex_lock(&lock);
+	t1 = data1value;
+	t2 = data2value;
+	pthread_mutex_unlock(&lock);
+
+	if(t1 != 0) {
+		assert(t2 != (t1+1)); //UNKNOWN!
+		assert(t2 == (t1+1)); //UNKNOWN!
+	}
+	return 0;
+}
+
+int main() {
+	data1value = 0;
+	data2value = 0;
+
+	pthread_t t1;
+    pthread_t t2;
+    pthread_t t3;
+    pthread_create(&t1, 0, iTThread_1, 0);
+    pthread_create(&t2, 0, iTThread_2, 0);
+    pthread_create(&t3, 0, iRThread_1, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    pthread_join(t3, 0);
+
+	return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/13-mukherjee_singleton_with_uninit.c b/tests/regression/52-apron-mukherjee/13-mukherjee_singleton_with_uninit.c
new file mode 100644
index 0000000000..caa497aab0
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/13-mukherjee_singleton_with_uninit.c
@@ -0,0 +1,34 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+
+#include <pthread.h>
+#include <assert.h>
+
+int x = 0;
+
+pthread_mutex_t lock = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_Singleton_With_Uninit(void* arg){
+	pthread_mutex_lock(&lock);
+	x = 3;
+	pthread_mutex_unlock(&lock);
+	return NULL;
+}
+
+void* T2_Singleton_With_Uninit(void* arg){
+	pthread_mutex_lock(&lock);
+	x = 5;
+	pthread_mutex_unlock(&lock);
+	return NULL;
+}
+
+int main() {
+	pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_Singleton_With_Uninit, 0);
+    pthread_create(&t2, 0, T2_Singleton_With_Uninit, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+	assert(x <= 5);
+	return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/14-mukherjee_stack.c b/tests/regression/52-apron-mukherjee/14-mukherjee_stack.c
new file mode 100644
index 0000000000..78b4a98dbb
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/14-mukherjee_stack.c
@@ -0,0 +1,59 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins  --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+int SIZE = 2;
+int OVERFLOW  = -1;
+int top = 0;
+int flag = 0;
+int arr1;
+int arr2;
+
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_Stack(void* arg) {
+    int i;
+    int j;
+    pthread_mutex_lock(&m);
+    j = SIZE;
+    pthread_mutex_unlock(&m);
+    for(i=0; i<j; i++) {
+        pthread_mutex_lock(&m);
+        assert(top < SIZE); //TODO
+
+        if (top < SIZE) {
+            top++;
+        }
+        flag = 1;
+        pthread_mutex_unlock(&m);
+    }
+    return NULL;
+}
+
+void* T2_Stack(void* arg) {
+    int i;
+    int j;
+    pthread_mutex_lock(&m);
+    j = SIZE;
+    pthread_mutex_unlock(&m);
+    for(i=0; i<j; i++) {
+    pthread_mutex_lock(&m);
+    if (flag == 1) {
+        if (top != 0)
+            top--;
+    }
+    pthread_mutex_unlock(&m);
+    }
+    return NULL;
+}
+
+int main() {
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_Stack, 0);
+    pthread_create(&t2, 0, T2_Stack, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+	return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/15-mukherjee_Stack_Longer.c b/tests/regression/52-apron-mukherjee/15-mukherjee_Stack_Longer.c
new file mode 100644
index 0000000000..b65d064e70
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/15-mukherjee_Stack_Longer.c
@@ -0,0 +1,49 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+int SIZE = 400;
+int top = 0;
+int flag = 0;
+
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_Stack_Longer(void* arg) {
+	int i;
+	for(i=0; i<SIZE; i++) {
+		pthread_mutex_lock(&m);
+		assert(top != SIZE); //TODO
+
+		if (top != SIZE) {
+			top++;
+		}
+		flag = 1;
+		pthread_mutex_unlock(&m);
+	}
+	return NULL;
+}
+
+void* T2_Stack_Longer(void* arg) {
+	int i;
+	for(i=0; i<SIZE; i++) {
+		pthread_mutex_lock(&m);
+		if (flag == 1) {
+			assert(top != 0); //TODO
+			if (top != 0)
+				top--;
+		}
+		pthread_mutex_unlock(&m);
+	}
+	return NULL;
+}
+
+int main() {
+	pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_Stack_Longer, 0);
+    pthread_create(&t2, 0, T2_Stack_Longer, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+	return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/16-mukherjee_Stack_Longest.c b/tests/regression/52-apron-mukherjee/16-mukherjee_Stack_Longest.c
new file mode 100644
index 0000000000..5e7ca865bd
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/16-mukherjee_Stack_Longest.c
@@ -0,0 +1,49 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+int SIZE = 800;
+int top = 0;
+int flag = 0;
+
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_Stack_Longest(void* arg) {
+    int i;
+    for(i=0; i<SIZE; i++) {
+        pthread_mutex_lock(&m);
+        assert(top != SIZE); //TODO
+
+        if (top != SIZE) {
+            top++;
+        }
+        flag = 1;
+        pthread_mutex_unlock(&m);
+    }
+    return NULL;
+}
+
+void* T2_Stack_Longest(void* arg) {
+    int i;
+    for(i=0; i<SIZE; i++) {
+        pthread_mutex_lock(&m);
+        if (flag == 1) {
+            assert(top != 0); //TODO
+            if (top != 0)
+                top--;
+        }
+        pthread_mutex_unlock(&m);
+    }
+    return NULL;
+}
+
+int main() {
+	pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_Stack_Longest, 0);
+    pthread_create(&t2, 0, T2_Stack_Longest, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/17-mukherjee_sync01.c b/tests/regression/52-apron-mukherjee/17-mukherjee_sync01.c
new file mode 100644
index 0000000000..769c182b69
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/17-mukherjee_sync01.c
@@ -0,0 +1,39 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening
+
+#include <pthread.h>
+#include <assert.h>
+
+int num = 1;
+
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_Sync01(void* arg) {
+    pthread_mutex_lock(&m);
+    while(num > 0)
+        num++; // Here num overflows
+    pthread_mutex_unlock(&m);
+    return NULL;
+}
+
+void* T2_Sync01(void* arg) {
+    pthread_mutex_lock(&m);
+    while(num == 0)
+        num--; // This never happens
+    pthread_mutex_unlock(&m);
+    return NULL;
+}
+
+int main() {
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1_Sync01, 0);
+    pthread_create(&t2, 0, T2_Sync01, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    assert(num >= 0); // UNKNOWN!
+
+    assert(num <= 1); // UNKNOWN!
+
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c b/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
new file mode 100644
index 0000000000..05053541d5
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
@@ -0,0 +1,66 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening --sets exp.apron.privatization mutex-meet-tid
+
+#include <pthread.h>
+#include <assert.h>
+
+int pendingIo, stoppingEvent, stopped, status;
+int conjunct_flag;
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1_QW2004(void* arg) {
+    int pending;
+    pthread_mutex_lock(&m);
+    pendingIo--;
+    pending = pendingIo;
+    if (pending == 0) {
+        stoppingEvent = 1;
+        stopped = 0;
+    }
+    else
+        stopped--;
+
+    assert(pendingIo == stopped);
+    pthread_mutex_unlock(&m);
+    return NULL;
+}
+
+int main() {
+    int status, pending;
+    pendingIo = 1;
+    stoppingEvent = 0;
+    stopped = 1;
+
+    status = 0;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, T1_QW2004, 0);
+
+    pthread_mutex_lock(&m);
+        if (stopped==0)
+            status = -1;
+        else {
+            pendingIo++;
+            stopped++;
+            status = 0;
+        }
+        assert(pendingIo == stopped);
+    pthread_mutex_unlock(&m);
+
+    pthread_mutex_lock(&m);
+    if (status == 0)
+        assert(pendingIo == stopped);
+    pthread_mutex_unlock(&m);
+
+    pthread_mutex_lock(&m);
+    if (pendingIo > 0) {
+        pendingIo--;
+        stopped--;
+    }
+    pending = pendingIo;
+    if (pending == 0)
+        stoppingEvent = 1;
+
+    assert(pendingIo == stopped);
+    pthread_mutex_unlock(&m);
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/19-mukherjee_fig_3_11.c b/tests/regression/52-apron-mukherjee/19-mukherjee_fig_3_11.c
new file mode 100644
index 0000000000..393d171020
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/19-mukherjee_fig_3_11.c
@@ -0,0 +1,44 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins
+
+#include <pthread.h>
+#include <assert.h>
+
+int x;
+int y;
+
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void* T1(void* arg) {
+    while(0 == 0) {
+        pthread_mutex_lock(&m);
+        if (x > 0) {
+            x = x - 1;
+            y = y - 1;
+        }
+        pthread_mutex_unlock(&m);
+    }
+    return NULL;
+}
+
+void* T2(void* arg) {
+    while(0 == 0) {
+        pthread_mutex_lock(&m);
+        if (x < 10) {
+            x = x + 1;
+            y = y + 1;
+        }
+        pthread_mutex_unlock(&m);
+    }
+    return NULL;
+}
+
+int main() {
+    pthread_t t1;
+    pthread_t t2;
+    pthread_create(&t1, 0, T1, 0);
+    pthread_create(&t2, 0, T2, 0);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    return 0;
+}
diff --git a/tests/regression/52-apron-mukherjee/README.txt b/tests/regression/52-apron-mukherjee/README.txt
new file mode 100644
index 0000000000..30f6fd0ce4
--- /dev/null
+++ b/tests/regression/52-apron-mukherjee/README.txt
@@ -0,0 +1,7 @@
+Benchmarks from https://doi.org/10.1007/978-3-319-66706-5_13
+
+Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky: Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Program
+
+Originally translated to Java from SV-COMP and modified (e.g. introduction of locks) by Mukherjee et al.
+
+Translated back to C by us.