From b3af7989b45b31e8fc6cd85c77a8d0a3b5a7fbdb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Nov 2023 12:48:29 +0200
Subject: [PATCH] Fix unsoundness in per-mutex-tid which is revealed by
 strengthening

---
 src/analyses/apron/relationPriv.apron.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index da7d4a1a3d..5a5dffc606 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -954,6 +954,7 @@ struct
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
     let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
+    let get_mutex_global_g = Cluster.keep_global g get_mutex_global_g in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
       if not inits then