diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 946b8f8cc5..f5173b9445 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -1135,9 +1135,9 @@ struct
     include SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All variables" end)
     let name () = "W"
   end
-  module D = W
+  module D = MapDomain.MapBot (MustLockset) (W)
 
-  let startstate () = W.empty ()
+  let startstate () = D.empty ()
 
   let read_global ask getg (st: BaseComponents (D).t) x =
     let s = current_lockset ask in
@@ -1154,7 +1154,7 @@ struct
     if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then
       sideg (V.global x) (G.create_weak (GWeak.singleton s v));
     let w' = if not invariant then
-        W.add x st.priv
+        D.join st.priv (D.singleton s (W.singleton x))
       else
         st.priv (* No need to add invariant to W because it doesn't matter for reads after invariant, only unlocks. *)
     in
@@ -1173,7 +1173,14 @@ struct
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let s = MustLockset.remove m (current_lockset ask) in
-    let is_in_W x _ = W.mem x st.priv in
+    let w = D.fold (fun s' w acc ->
+        if MustLockset.mem m s' then
+          W.join w acc
+        else
+          acc
+      ) st.priv (W.empty ())
+    in
+    let is_in_W x _ = W.mem x w in
     let side_cpa = CPA.filter is_in_W st.cpa in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
     st
@@ -1194,7 +1201,7 @@ struct
       CPA.fold (fun x v (st: BaseComponents (D).t) ->
           if is_global ask x then (
             sideg (V.global x) (G.create_weak (GWeak.singleton (MustLockset.empty ()) v));
-            {st with priv = W.add x st.priv} (* TODO: is this add necessary? *)
+            {st with priv = D.join st.priv (D.singleton (MustLockset.empty ()) (W.singleton x))} (* TODO: is this add necessary? *)
           )
           else
             st
@@ -1220,6 +1227,12 @@ struct
     let name () = "V"
   end
 
+  module DV2 =
+  struct
+    include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MayVars)
+    let name () = "V2"
+  end
+
   module L =
   struct
     include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MinLocksets)
@@ -1235,7 +1248,7 @@ struct
   open Locksets
 
   open LockCenteredD
-  module D = Lattice.Prod (DV) (L)
+  module D = Lattice.Prod3 (DV) (DV2) (L)
 
   module Wrapper = Wrapper (G)
   module UnwrappedG = G
@@ -1244,7 +1257,7 @@ struct
   let invariant_global ask getg = invariant_global ask (Wrapper.getg ask getg)
   let invariant_vars ask getg = invariant_vars ask (Wrapper.getg ask getg)
 
-  let startstate () = (DV.bot (), L.bot ())
+  let startstate () = (DV.bot (), DV2.bot (), L.bot ())
 
   let lockset_init = MustLockset.all ()
 
@@ -1258,7 +1271,7 @@ struct
   let read_global ask getg (st: BaseComponents (D).t) x =
     let getg = Wrapper.getg ask getg in
     let s = current_lockset ask in
-    let (vv, l) = st.priv in
+    let (vv, vv2, l) = st.priv in
     let d_cpa = CPA.find x st.cpa in
     let d_sync = L.fold (fun m bs acc ->
         if not (MustVars.mem x (DV.find m vv)) then
@@ -1302,10 +1315,11 @@ struct
     let sideg = Wrapper.sideg ask sideg in
     let getg = Wrapper.getg ask getg in
     let s = current_lockset ask in
-    let (vv, l) = st.priv in
-    let v' = L.fold (fun m _ acc ->
-        DV.add m (MustVars.add x (DV.find m acc)) acc
-      ) l vv
+    let (vv, vv2, l) = st.priv in
+    let (v', v2') = L.fold (fun m _ (acc1, acc2) ->
+        DV.add m (MustVars.add x (DV.find m acc1)) acc1,
+        DV2.add m (MayVars.add x (DV2.find m acc2)) acc2
+      ) l (vv, vv2)
     in
     let cpa' = CPA.add x v st.cpa in
     if not invariant && not (!earlyglobs && is_excluded_from_earlyglobs x) then (
@@ -1313,20 +1327,22 @@ struct
       sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton s v))
       (* Unlock after invariant will still side effect refined value from CPA, because cannot distinguish from non-invariant write. *)
     );
-    {st with cpa = cpa'; priv = (v', l)}
+    {st with cpa = cpa'; priv = (v', v2', l)}
 
   let lock ask getg (st: BaseComponents (D).t) m =
     let s = current_lockset ask in
-    let (v, l) = st.priv in
+    let (v, v2, l) = st.priv in
     let v' = DV.add m (MustVars.empty ()) v in
+    let v2' = DV2.add m (MayVars.empty ()) v2 in
     let l' = L.add m (MinLocksets.singleton s) l in
-    {st with priv = (v', l')}
+    {st with priv = (v', v2', l')}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let sideg = Wrapper.sideg ask sideg in
     let getg = Wrapper.getg ask getg in
     let s = MustLockset.remove m (current_lockset ask) in
-    let is_in_G x _ = is_global ask x in
+    let (_, v2, _) = st.priv in
+    let is_in_G x _ = is_global ask x && MayVars.mem x (DV2.find m v2) in
     let side_cpa = CPA.filter is_in_G st.cpa in
     let side_cpa = CPA.mapi (fun x v ->
         let v = distr_init getg x v in
diff --git a/tests/regression/13-privatized/95-mine-W-part-by-S.c b/tests/regression/13-privatized/95-mine-W-part-by-S.c
new file mode 100644
index 0000000000..3c714f1d48
--- /dev/null
+++ b/tests/regression/13-privatized/95-mine-W-part-by-S.c
@@ -0,0 +1,32 @@
+// PARAM: --set ana.base.privatization mine-W-noinit
+#include <pthread.h>
+#include <goblint.h>
+
+int g, h;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&A);
+  g = 5;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&B);
+  // __goblint_check(g == 5); // UNKNOWN! (data race, so weak read)
+  h = 6;
+  pthread_mutex_unlock(&B);
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&A);
+  g = 8;
+  pthread_mutex_lock(&B);
+  __goblint_check(g == 8);
+  pthread_mutex_unlock(&B);
+  pthread_mutex_unlock(&A);
+  return 0;
+}
diff --git a/tests/regression/13-privatized/95-mine-W-part-by-S.t b/tests/regression/13-privatized/95-mine-W-part-by-S.t
new file mode 100644
index 0000000000..4c23b13d91
--- /dev/null
+++ b/tests/regression/13-privatized/95-mine-W-part-by-S.t
@@ -0,0 +1,99 @@
+Miné succeeds:
+
+  $ goblint --set ana.base.privatization mine 95-mine-W-part-by-S.c
+  [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+Miné without thread IDs even succeeds:
+
+  $ goblint --set ana.base.privatization mine-nothread 95-mine-W-part-by-S.c
+  [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+Our Miné with W doesn't succeed with W partitioning due to initialization:
+
+  $ goblint --set ana.base.privatization mine-W 95-mine-W-part-by-S.c
+  [Warning][Assert] Assertion "g == 8" is unknown. (95-mine-W-part-by-S.c:28:3-28:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+But the noinit variant succeeds:
+
+  $ goblint --set ana.base.privatization mine-W-noinit 95-mine-W-part-by-S.c
+  [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+
+
+Protection-Based succeeds:
+
+  $ goblint --set ana.base.privatization protection 95-mine-W-part-by-S.c
+  [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+Write-Centered succeeds:
+
+  $ goblint --set ana.base.privatization write 95-mine-W-part-by-S.c
+  [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
+
+Lock-Centered (with may-V) also succeeds:
+
+  $ goblint --set ana.base.privatization lock 95-mine-W-part-by-S.c
+  [Success][Assert] Assertion "g == 8" will succeed (95-mine-W-part-by-S.c:28:3-28:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 17
+    dead: 0
+    total lines: 17
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2