diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 72b91d71b7..a42d78d71a 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -772,7 +772,7 @@ struct
       PCU.RH.replace results ctx.node new_value;
     end;
     WideningTokens.with_local_side_tokens (fun () ->
-        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `Return | `Init | `Thread])
+        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread])
       )
 
   let init marshal =
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 61da6ddc42..3ecfb713d7 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -36,7 +36,7 @@ module type S =
     val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
     val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
 
-    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `Return | `Init | `Thread] -> relation_components_t
+    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> relation_components_t
 
     val escape: Node.t -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> EscapeDomain.EscapedVars.t -> relation_components_t
     val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> relation_components_t
@@ -96,8 +96,7 @@ struct
     { st with rel = rel_local }
 
   let sync (ask: Q.ask) getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Join when ConfCheck.branched_thread_creation () ->
+    let branched_sync () =
       if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
         st
       else
@@ -110,7 +109,14 @@ struct
           )
         in
         {st with rel = rel_local}
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
     | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread
@@ -337,17 +343,8 @@ struct
   let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
-  let sync ask getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Return -> (* required for thread return *)
-      (* TODO: implement? *)
-      begin match ThreadId.get_current ask with
-        | `Lifted x (* when CPA.mem x st.cpa *) ->
-          st
-        | _ ->
-          st
-      end
-    | `Join when ConfCheck.branched_thread_creation () ->
+  let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
+    let branched_sync () =
       if ask.f (Q.MustBeSingleThreaded { since_start= true }) then
         st
       else
@@ -376,7 +373,22 @@ struct
            let rel_local' = RD.meet rel_local (getg ()) in
            {st with rel = rel_local'} *)
         st
+    in
+    match reason with
+    | `Return -> (* required for thread return *)
+      (* TODO: implement? *)
+      begin match ThreadId.get_current ask with
+        | `Lifted x (* when CPA.mem x st.cpa *) ->
+          st
+        | _ ->
+          st
+      end
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+      branched_sync ()
     | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread ->
@@ -626,17 +638,8 @@ struct
   let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
-  let sync ask getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Return -> (* required for thread return *)
-      (* TODO: implement? *)
-      begin match ThreadId.get_current ask with
-        | `Lifted x (* when CPA.mem x st.cpa *) ->
-          st
-        | _ ->
-          st
-      end
-    | `Join when ConfCheck.branched_thread_creation () ->
+  let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
+    let branched_sync () =
       if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
         st
       else
@@ -659,7 +662,22 @@ struct
           )
         in
         {st with rel = rel_local}
+    in
+    match reason with
+    | `Return -> (* required for thread return *)
+      (* TODO: implement? *)
+      begin match ThreadId.get_current ask with
+        | `Lifted x (* when CPA.mem x st.cpa *) ->
+          st
+        | _ ->
+          st
+      end
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+      branched_sync ()
     | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread ->
@@ -1192,9 +1210,7 @@ struct
     st
 
   let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
-    match reason with
-    | `Return -> st (* TODO: implement? *)
-    | `Join when ConfCheck.branched_thread_creation () ->
+    let branched_sync () =
       if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
         st
       else
@@ -1209,7 +1225,15 @@ struct
           )
         in
         {st with rel = rel_local}
+    in
+    match reason with
+    | `Return -> st (* TODO: implement? *)
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+      branched_sync ()
     | `Join
+    | `JoinCall
     | `Normal
     | `Init
     | `Thread ->
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index b80ac59d7f..102e22b5a7 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -451,7 +451,7 @@ struct
     else
       ctx.local
 
-  let sync ctx reason = sync' (reason :> [`Normal | `Join | `Return | `Init | `Thread]) ctx
+  let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) ctx
 
   let publish_all ctx reason =
     ignore (sync' reason ctx)
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index cecc838b9e..efa0575bf4 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -31,7 +31,7 @@ sig
   val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
   val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
 
-  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseComponents (D).t
+  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseComponents (D).t
 
   val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t
   val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
@@ -306,8 +306,8 @@ struct
     st
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
-    match reason with
-    | `Join when ConfCheck.branched_thread_creation () -> (* required for branched thread creation *)
+    let branched_sync () =
+      (* required for branched thread creation *)
       let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in
       sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *)
       (* TODO: this makes mutex-oplus less precise in 28-race_reach/10-ptrmunge_racefree and 28-race_reach/trylock2_racefree, why? *)
@@ -318,7 +318,14 @@ struct
             sideg (V.global x) (CPA.singleton x v)
         ) st.cpa;
       st
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+      branched_sync ()
     | `Join
+    | `JoinCall
     | `Return
     | `Normal
     | `Init
@@ -404,8 +411,8 @@ struct
     {st with cpa = cpa'}
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
-    match reason with
-    | `Join when ConfCheck.branched_thread_creation () -> (* required for branched thread creation *)
+    let branched_sync () =
+      (* required for branched thread creation *)
       let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in
       sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *)
 
@@ -422,7 +429,14 @@ struct
         ) st.cpa st.cpa
       in
       {st with cpa = cpa'}
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+      branched_sync ()
     | `Join
+    | `JoinCall
     | `Return
     | `Normal
     | `Init
@@ -772,9 +786,9 @@ struct
       ) st.cpa st
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
-    let sideg = Wrapper.sideg ask sideg in
-    match reason with
-    | `Join when ConfCheck.branched_thread_creation () -> (* required for branched thread creation *)
+    let branched_sync () =
+      (* required for branched thread creation *)
+      let sideg = Wrapper.sideg ask sideg in
       CPA.fold (fun x v (st: BaseComponents (D).t) ->
           if is_global ask x && is_unprotected ask x then (
             sideg (V.unprotected x) v;
@@ -784,7 +798,14 @@ struct
           else
             st
         ) st.cpa st
+    in
+    match reason with
+    | `Join when ConfCheck.branched_thread_creation () ->
+      branched_sync ()
+    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+      branched_sync ()
     | `Join
+    | `JoinCall
     | `Return
     | `Normal
     | `Init
@@ -1034,6 +1055,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1089,6 +1111,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1160,6 +1183,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1318,6 +1342,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1496,6 +1521,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
@@ -1678,6 +1704,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
+    | `JoinCall
     | `Init
     | `Thread ->
       st
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
index e176a450fa..87b17e5ad0 100644
--- a/src/analyses/basePriv.mli
+++ b/src/analyses/basePriv.mli
@@ -20,7 +20,7 @@ sig
   val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
   val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
 
-  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
+  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
 
   val escape: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseDomain.BaseComponents (D).t
   val enter_multithreaded: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index fb5d0db142..1ece8dcc60 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -59,6 +59,24 @@ struct
       not threadflag_path_sens
     else
       true
+
+  (** Whether branched thread creation at start nodes of procedures needs to be handled by [sync `JoinCall] of privatization. *)
+  let branched_thread_creation_at_call (ask:Queries.ask) =
+    let threadflag_active = List.mem "threadflag" (GobConfig.get_string_list "ana.activated") in
+    if threadflag_active then
+      let sens = GobConfig.get_string_list "ana.ctx_sens" in
+      let threadflag_ctx_sens = match sens with
+        | [] -> (* use values of "ana.ctx_insens" (blacklist) *)
+          not (List.mem "threadflag" @@ GobConfig.get_string_list "ana.ctx_insens")
+        | sens -> (* use values of "ana.ctx_sens" (whitelist) *)
+          List.mem "threadflag" sens
+      in
+      if not threadflag_ctx_sens then
+        true
+      else
+        ask.f (Queries.GasExhausted)
+    else
+      true
 end
 
 module Protection =
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 71c887dda5..e4c0e261e4 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -318,6 +318,13 @@ struct
              f (Result.top ()) (!base_id, spec !base_id, assoc !base_id ctx.local) *)
           | Queries.DYojson ->
             `Lifted (D.to_yojson ctx.local)
+          | Queries.GasExhausted ->
+            if (get_int "ana.context.gas_value" >= 0) then
+              (* There is a lifter above this that will answer it, save to ask *)
+              ctx.ask (Queries.GasExhausted)
+            else
+              (* Abort to avoid infinite recursion *)
+              false
           | _ ->
             let r = fold_left (f ~q) (Result.top ()) @@ spec_list ctx.local in
             do_sideg ctx !sides;
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 488fc494b0..acf85abed9 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -980,7 +980,7 @@
             },
             "gas_value": {
               "title": "ana.context.gas_value",
-              "description": "Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitve analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.",
+              "description": "Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitive analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.",
               "type": "integer",
               "default": -1
             },
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index a904f696eb..1ceb91ef1d 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -126,6 +126,7 @@ type _ t =
   | IsEverMultiThreaded: MayBool.t t
   | TmpSpecial:  Mval.Exp.t -> ML.t t
   | MaySignedOverflow: exp -> MayBool.t t
+  | GasExhausted: MustBool.t t
 
 type 'a result = 'a
 
@@ -196,6 +197,7 @@ struct
     | IsEverMultiThreaded -> (module MayBool)
     | TmpSpecial _ -> (module ML)
     | MaySignedOverflow  _ -> (module MayBool)
+    | GasExhausted -> (module MustBool)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -265,6 +267,7 @@ struct
     | IsEverMultiThreaded -> MayBool.top ()
     | TmpSpecial _ -> ML.top ()
     | MaySignedOverflow _ -> MayBool.top ()
+    | GasExhausted -> MustBool.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -331,6 +334,7 @@ struct
     | Any (TmpSpecial _) -> 56
     | Any (IsAllocVar _) -> 57
     | Any (MaySignedOverflow _) -> 58
+    | Any GasExhausted -> 59
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -490,6 +494,7 @@ struct
     | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
     | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e
+    | Any GasExhausted -> Pretty.dprintf "GasExhausted"
 end
 
 let to_value_domain_ask (ask: ask) =
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 4ef98358f4..1ea01c99fb 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -209,7 +209,7 @@ sig
   val context: (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t -> C.t
   val startcontext: unit -> C.t
 
-  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `Return] -> D.t
+  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall | `Return] -> D.t
   val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result
 
   (** A transfer function which handles the assignment of a rval to a lval, i.e.,
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 07180d54dd..e0e36801ed 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -575,8 +575,14 @@ struct
     let liftmap f = List.map (fun (x) -> (x, max 0 (cg_val ctx - 1))) f in
     liftmap (S.threadenter (conv ctx) ~multiple lval f args)
 
+  let query ctx (type a) (q: a Queries.t):a Queries.result =
+    match q with
+    | Queries.GasExhausted ->
+      let (d,i) = ctx.local in
+      (i <= 0)
+    | _ -> S.query (conv ctx) q
+
   let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
-  let query ctx q                                 = S.query (conv ctx) q
   let assign ctx lval expr                        = S.assign (conv ctx) lval expr, cg_val ctx
   let vdecl ctx v                                 = S.vdecl (conv ctx) v, cg_val ctx
   let body ctx fundec                             = S.body (conv ctx) fundec, cg_val ctx
@@ -624,9 +630,10 @@ struct
 
   let sync ctx =
     match ctx.prev_node, Cfg.prev ctx.prev_node with
-    | _, _ :: _ :: _ (* Join in CFG. *)
-    | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+    | _, _ :: _ :: _ -> (* Join in CFG. *)
       S.sync ctx `Join
+    | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+      S.sync ctx `JoinCall
     | _, _ -> S.sync ctx `Normal
 
   let side_context sideg f c =
diff --git a/tests/regression/46-apron2/89-flag-ctx-sens.c b/tests/regression/46-apron2/89-flag-ctx-sens.c
new file mode 100644
index 0000000000..41e4f02520
--- /dev/null
+++ b/tests/regression/46-apron2/89-flag-ctx-sens.c
@@ -0,0 +1,28 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet
+// NOTIMEOUT
+// See https://github.com/goblint/analyzer/pull/1508
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void fn() {
+  // Just do nothing
+  return;
+}
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m);
+  g = g+1;
+  fn();
+  pthread_mutex_unlock(&m);
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  return 0;
+}
diff --git a/tests/regression/80-context_gas/21-sync.c b/tests/regression/80-context_gas/21-sync.c
new file mode 100644
index 0000000000..33edf254e5
--- /dev/null
+++ b/tests/regression/80-context_gas/21-sync.c
@@ -0,0 +1,35 @@
+// PARAM: --set ana.context.gas_value 1
+// Like 00/35 but with gas this time!
+// Misbehaves for gas <= 3
+#include <goblint.h>
+#include <pthread.h>
+
+int g = 1;
+
+void foo() {
+  // Single-threaded: g = 1 in local state
+  // Multi-threaded: g = 2 in global unprotected invariant
+  // Joined contexts: g is unprotected, so read g = 2 from global unprotected invariant (only)
+  // Was soundly claiming that check will succeed!
+  int x = g;
+  __goblint_check(x == 2); // UNKNOWN!
+}
+
+void *t_fun(void *arg) {
+  foo();
+}
+
+int do_stuff() {
+  foo();
+  g = 2;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  return 0;
+}
+
+int main() {
+  do_stuff();
+  return 0;
+}
diff --git a/tests/regression/80-context_gas/22-sync-precision.c b/tests/regression/80-context_gas/22-sync-precision.c
new file mode 100644
index 0000000000..8fc1dd7779
--- /dev/null
+++ b/tests/regression/80-context_gas/22-sync-precision.c
@@ -0,0 +1,36 @@
+// PARAM: --set ana.context.gas_value 4
+// Like 00/35 but with gas this time!
+// Misbehaves for gas <= 3
+#include <goblint.h>
+#include <pthread.h>
+
+int g = 1;
+
+void foo() {
+  // Check that we don't lose precision due to JoinCall
+  int x = g;
+  int x2 = g;
+  // A hack: In both contexts g has a single possible value, so we check that x = x2
+  // to verify there is no precision loss
+
+  __goblint_check(x == x2);
+}
+
+void *t_fun(void *arg) {
+  foo();
+}
+
+int do_stuff() {
+  foo();
+  g = 2;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  return 0;
+}
+
+int main() {
+  do_stuff();
+  return 0;
+}