From 08d56aa0d8e6e13b1ff87fd11d3bdffc8218611a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 24 Sep 2023 16:51:17 +0200
Subject: [PATCH 1/6] Add argument to `threadenter`

---
 src/analyses/abortUnless.ml                  |  2 +-
 src/analyses/accessAnalysis.ml               |  2 +-
 src/analyses/activeLongjmp.ml                |  2 +-
 src/analyses/activeSetjmp.ml                 |  2 +-
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/base.ml                         |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/expsplit.ml                     |  2 +-
 src/analyses/extractPthread.ml               |  2 +-
 src/analyses/fileUse.ml                      |  2 +-
 src/analyses/locksetAnalysis.ml              |  2 +-
 src/analyses/mCP.ml                          | 12 ++++-----
 src/analyses/mallocFresh.ml                  |  2 +-
 src/analyses/malloc_null.ml                  |  2 +-
 src/analyses/modifiedSinceLongjmp.ml         |  2 +-
 src/analyses/mutexTypeAnalysis.ml            |  2 +-
 src/analyses/poisonVariables.ml              |  2 +-
 src/analyses/pthreadSignals.ml               |  2 +-
 src/analyses/region.ml                       |  2 +-
 src/analyses/spec.ml                         |  2 +-
 src/analyses/stackTrace.ml                   |  4 +--
 src/analyses/symbLocks.ml                    |  2 +-
 src/analyses/taintPartialContexts.ml         |  2 +-
 src/analyses/termination.ml                  |  2 +-
 src/analyses/threadAnalysis.ml               |  2 +-
 src/analyses/threadEscape.ml                 |  2 +-
 src/analyses/threadFlag.ml                   |  2 +-
 src/analyses/threadId.ml                     |  8 +++---
 src/analyses/threadReturn.ml                 |  2 +-
 src/analyses/tmpSpecial.ml                   |  2 +-
 src/analyses/tutorials/taint.ml              |  2 +-
 src/analyses/tutorials/unitAnalysis.ml       |  2 +-
 src/analyses/uninit.ml                       |  2 +-
 src/analyses/useAfterFree.ml                 |  4 +--
 src/analyses/varEq.ml                        |  2 +-
 src/analyses/vla.ml                          |  2 +-
 src/analyses/wrapperFunctionAnalysis.ml      |  2 +-
 src/framework/analyses.ml                    |  6 ++---
 src/framework/constraints.ml                 | 27 ++++++++++----------
 src/framework/control.ml                     |  6 ++---
 src/framework/resultQuery.ml                 |  6 ++---
 src/util/wideningTokens.ml                   |  2 +-
 src/witness/observerAnalysis.ml              |  2 +-
 src/witness/witnessConstraints.ml            |  4 +--
 44 files changed, 74 insertions(+), 73 deletions(-)

diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 813d999ac3..1c77803c7e 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -65,7 +65,7 @@ struct
     false
 
   let startstate v = false
-  let threadenter ctx lval f args = [false]
+  let threadenter ?(multiple=false) ctx lval f args = [false]
   let threadspawn ctx lval f args fctx = false
   let exitstate v = false
 end
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index e99aefa0e5..bd1ca528a7 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -54,7 +54,7 @@ struct
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
-  let threadenter ctx lval f args = [()]
+  let threadenter ?(multiple=false) ctx lval f args = [()]
   let exitstate  v = ()
   let context fd d = ()
 
diff --git a/src/analyses/activeLongjmp.ml b/src/analyses/activeLongjmp.ml
index 9c9868e32f..43da8c6512 100644
--- a/src/analyses/activeLongjmp.ml
+++ b/src/analyses/activeLongjmp.ml
@@ -26,7 +26,7 @@ struct
 
   (* Initial values don't really matter: overwritten at longjmp call. *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml
index 069111d3ba..a69bf4db95 100644
--- a/src/analyses/activeSetjmp.ml
+++ b/src/analyses/activeSetjmp.ml
@@ -25,7 +25,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 46c620f390..d56064a42f 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -647,7 +647,7 @@ struct
 
   (* Thread transfer functions. *)
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let st = ctx.local in
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 71e2661997..cb29cbc0ab 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2503,7 +2503,7 @@ struct
     in
     combine_one ctx.local after
 
-  let threadenter ctx (lval: lval option) (f: varinfo) (args: exp list): D.t list =
+  let threadenter ?(multiple=false) ctx (lval: lval option) (f: varinfo) (args: exp list): D.t list =
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
       [make_entry ~thread:true ctx fd args]
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 04b148dd02..3a2cc5798d 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -155,7 +155,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index f121d0380e..9c610a96bf 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -84,7 +84,7 @@ struct
     in
     emit_splits ctx d
 
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
 
   let threadspawn ctx lval f args fctx =
     emit_splits_ctx ctx
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index 60e389fedf..591704cc70 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -1238,7 +1238,7 @@ module Spec : Analyses.MCPSpec = struct
       (Ctx.top ())
 
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let d : D.t = ctx.local in
     let tasks = ctx.global tasks_var in
     (* TODO: optimize finding *)
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index a9088a4bb2..b12953c71c 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -287,7 +287,7 @@ struct
     | _ -> m
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 2e9e08f03d..56fe960a47 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -18,7 +18,7 @@ struct
   module C = D
 
   let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
   let exitstate  v = D.empty ()
 end
 
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 1b6a7e5a1d..e305e9c7f6 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -140,9 +140,9 @@ struct
         f ((k,v::a')::a) b
     in f [] xs
 
-  let do_spawns ctx (xs:(varinfo * (lval option * exp list)) list) =
+  let do_spawns ctx (xs:(varinfo * (lval option * exp list * bool)) list) =
     let spawn_one v d =
-      List.iter (fun (lval, args) -> ctx.spawn lval v args) d
+      List.iter (fun (lval, args, multiple) -> ctx.spawn ~multiple lval v args) d
     in
     if not (get_bool "exp.single-threaded") then
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
@@ -322,8 +322,8 @@ struct
 
   and outer_ctx tfname ?spawns ?sides ?emits ctx =
     let spawn = match spawns with
-      | Some spawns -> (fun l v a  -> spawns := (v,(l,a)) :: !spawns)
-      | None -> (fun v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
+      | Some spawns -> (fun ?(multiple=false) l v a  -> spawns := (v,(l,a,multiple)) :: !spawns)
+      | None -> (fun ?(multiple=false) v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
     in
     let sideg = match sides with
       | Some sides -> (fun v g    -> sides  := (v, (!WideningTokens.side_tokens, g)) :: !sides)
@@ -565,13 +565,13 @@ struct
     let d = do_emits ctx !emits d q in
     if q then raise Deadcode else d
 
-  let threadenter (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
+  let threadenter ?(multiple=false) (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "threadenter" ~sides ~emits ctx in
     let f (n,(module S:MCPSpec),d) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "threadenter" ctx'' n d in
-      map (fun d -> (n, repr d)) @@ S.threadenter ctx' lval f a
+      map (fun d -> (n, repr d)) @@ (S.threadenter ~multiple) ctx' lval f a
     in
     let css = map f @@ spec_list ctx.local in
     do_sideg ctx !sides;
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 2c2b99a075..861e4958bd 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -52,7 +52,7 @@ struct
       | None -> ctx.local
       | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.empty ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 4d5871cb80..2d90112636 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -215,7 +215,7 @@ struct
   let name () = "malloc_null"
 
   let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index 0375bd3f74..d9c8f5102c 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -63,7 +63,7 @@ struct
       ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 806c35f464..7051173bd0 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -65,7 +65,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 1bd4b6d544..8c79626cc9 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -61,7 +61,7 @@ struct
     VS.join au ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let event ctx e octx =
diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
index 0b776282e8..83455965ec 100644
--- a/src/analyses/pthreadSignals.ml
+++ b/src/analyses/pthreadSignals.ml
@@ -73,7 +73,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = Signals.empty ()
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
   let exitstate  v = Signals.empty ()
 end
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 6d2ae246c3..9d68221fcd 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -175,7 +175,7 @@ struct
   let startstate v =
     `Lifted (RegMap.bot ())
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [`Lifted (RegMap.bot ())]
   let threadspawn ctx lval f args fctx = ctx.local
 
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index 54ffcd2697..e5434eb264 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -487,7 +487,7 @@ struct
 
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml
index 4dc62f1873..3d70c50856 100644
--- a/src/analyses/stackTrace.ml
+++ b/src/analyses/stackTrace.ml
@@ -21,7 +21,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 end
 
@@ -45,7 +45,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.top ()
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.push !Tracing.current_loc ctx.local]
 end
 
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index d8cebf51d2..b99ef93039 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -29,7 +29,7 @@ struct
   let name () = "symb_locks"
 
   let startstate v = D.top ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index d053cd103b..25e981dcbf 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -101,7 +101,7 @@ struct
     d
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.bot ()]
   let threadspawn ctx lval f args fctx =
     match lval with
diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml
index 6da9225d3f..5e5e0d36f1 100644
--- a/src/analyses/termination.ml
+++ b/src/analyses/termination.ml
@@ -217,7 +217,7 @@ struct
   (* | _ -> ctx.local *)
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 1e679a4707..26e6702c25 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -84,7 +84,7 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx =
     let creator = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx fctx) in
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 9ed62e7422..0674ebf3d1 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -150,7 +150,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.bot ()
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.bot ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index f2ebf82be1..f3b132918a 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -58,7 +58,7 @@ struct
   let access ctx _ =
     is_currently_multi (Analyses.ask_of_ctx ctx)
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
       ctx.emit Events.EnterMultiThreaded;
     [create_tid f]
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 4acf88a7ef..f1de1dfdcb 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -56,9 +56,9 @@ struct
       Hashtbl.replace !tids tid ();
     (N.bot (), `Lifted (tid), (TD.bot (), TD.bot ()))
 
-  let create_tid (_, current, (td, _)) ((node, index): Node.t * int option) v =
+  let create_tid ?(multiple=false) (_, current, (td, _)) ((node, index): Node.t * int option) v =
     match current with
-    | `Lifted current ->
+    | `Lifted current when not multiple ->
       let+ tid = Thread.threadenter (current, td) node index v in
       if GobConfig.get_bool "dbg.print_tids" then
         Hashtbl.replace !tids tid ();
@@ -133,9 +133,9 @@ struct
     | `Lifted node, count -> node, Some count
     | (`Bot | `Top), _ -> ctx.prev_node, None
 
-  let threadenter ctx lval f args:D.t list =
+  let threadenter ?(multiple=false) ctx lval f args:D.t list =
     let n, i = indexed_node_for_ctx ctx in
-    let+ tid = create_tid ctx.local (n, i) f in
+    let+ tid = create_tid ~multiple ctx.local (n, i) f in
     (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
index 470c4ceaa8..176a4d3465 100644
--- a/src/analyses/threadReturn.ml
+++ b/src/analyses/threadReturn.ml
@@ -28,7 +28,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = true
-  let threadenter ctx lval f args = [true]
+  let threadenter ?(multiple=false) ctx lval f args = [true]
   let exitstate  v = D.top ()
 
   let query (ctx: (D.t, _, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index 2d38972d7a..f3d092e59e 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -88,7 +88,7 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 3067449e31..166ce2c3f6 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -129,7 +129,7 @@ struct
 
   (* You may leave these alone *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index d3b8c69bfd..b5fb4d6367 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -39,7 +39,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index f8759d9134..abdcd67aaa 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -25,7 +25,7 @@ struct
   let name () = "uninit"
 
   let startstate v : D.t = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 0aafbd1ad4..6033c689e1 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -196,7 +196,7 @@ struct
       end
     | _ -> state
 
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 
   let startstate v = D.bot ()
@@ -205,4 +205,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 634a684c7c..7bd3453b8a 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -43,7 +43,7 @@ struct
   let name () = "var_eq"
 
   let startstate v = D.top ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/vla.ml b/src/analyses/vla.ml
index 865f22b20a..8bd0168de0 100644
--- a/src/analyses/vla.ml
+++ b/src/analyses/vla.ml
@@ -33,7 +33,7 @@ struct
     ctx.local || Cilfacade.isVLAType v.vtype
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
index d9bbdb6197..89242e044e 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -87,7 +87,7 @@ struct
 
   let startstate v = D.bot ()
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     (* The new thread receives a fresh counter *)
     [D.bot ()]
 
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index df3346af93..54a3a18f1a 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -342,7 +342,7 @@ type ('d,'g,'c,'v) ctx =
   ; edge     : MyCFG.edge
   ; local    : 'd
   ; global   : 'v -> 'g
-  ; spawn    : lval option -> varinfo -> exp list -> unit
+  ; spawn    : ?multiple:bool -> lval option -> varinfo -> exp list -> unit
   ; split    : 'd -> Events.t list -> unit
   ; sideg    : 'v -> 'g -> unit
   }
@@ -444,7 +444,7 @@ sig
   val paths_as_set : (D.t, G.t, C.t, V.t) ctx -> D.t list
 
   (** Returns initial state for created thread. *)
-  val threadenter : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t list
+  val threadenter : ?multiple:bool -> (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t list
 
   (** Updates the local state of the creator thread using initial state of created thread. *)
   val threadspawn : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
@@ -696,7 +696,7 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
     ctx.local
 
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 end
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 740d1f85a9..a7683fb6b3 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -83,8 +83,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     D.lift @@ S.combine_assign (conv ctx) r fe f args fc (D.unlift es) f_ask
 
-  let threadenter ctx lval f args =
-    List.map D.lift @@ S.threadenter (conv ctx) lval f args
+  let threadenter ?(multiple=false) ctx lval f args =
+    List.map D.lift @@ (S.threadenter ~multiple) (conv ctx) lval f args
 
   let threadspawn ctx lval f args fctx =
     D.lift @@ S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -167,8 +167,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     S.combine_assign (conv ctx) r fe f args (Option.map C.unlift fc) es f_ask
 
-  let threadenter ctx lval f args =
-    S.threadenter (conv ctx) lval f args
+  let threadenter ?(multiple=false) ctx lval f args =
+    S.threadenter ~multiple (conv ctx) lval f args
 
   let threadspawn ctx lval f args fctx =
     S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -249,7 +249,7 @@ struct
   let combine_env' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
 
-  let threadenter ctx lval f args = lift_fun ctx (List.map lift_start_level) S.threadenter ((|>) args % (|>) f % (|>) lval)
+  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
   let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let leq0 = function
@@ -394,7 +394,7 @@ struct
 
   let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
 
-  let threadenter ctx lval f args = S.threadenter (conv ctx) lval f args |> List.map (fun d -> (d, snd ctx.local))
+  let threadenter ?(multiple=false) ctx lval f args = S.threadenter ~multiple (conv ctx) lval f args |> List.map (fun d -> (d, snd ctx.local))
   let threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let enter ctx r f args =
@@ -485,7 +485,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
 
-  let threadenter ctx lval f args = lift_fun ctx (List.map D.lift) S.threadenter ((|>) args % (|>) f % (|>) lval) []
+  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
   let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
 
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
@@ -581,7 +581,7 @@ struct
       ; split   = (fun (d:D.t) es -> assert (List.is_empty es); r := d::!r)
       ; sideg   = (fun g d -> sideg (GVar.spec g) (G.create_spec d))
       }
-    and spawn lval f args =
+    and spawn ?(multiple=false) lval f args =
       (* TODO: adjust ctx node/edge? *)
       (* TODO: don't repeat for all paths that spawn same *)
       let ds = S.threadenter ctx lval f args in
@@ -898,7 +898,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = S.startstate Cil.dummyFunDec.svar (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *)
       ; global = (fun g -> G.spec (getg (GVar.spec g)))
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
+      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in query context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
       }
@@ -1262,9 +1262,10 @@ struct
     let fd1 = D.choose octx.local in
     map ctx Spec.event (fun h -> h e (conv octx fd1))
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let g xs ys = (List.map (fun y -> D.singleton y) ys) @ xs in
-    fold' ctx Spec.threadenter (fun h -> h lval f args) g []
+    fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
+
   let threadspawn ctx lval f args fctx =
     let fd1 = D.choose fctx.local in
     map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))
@@ -1448,7 +1449,7 @@ struct
   let combine_env ctx = S.combine_env (conv ctx)
   let combine_assign ctx = S.combine_assign (conv ctx)
   let special ctx = S.special (conv ctx)
-  let threadenter ctx = S.threadenter (conv ctx)
+  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
@@ -1684,7 +1685,7 @@ struct
       List.iter handle_path (S.paths_as_set conv_ctx);
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
-  let threadenter ctx = S.threadenter (conv ctx)
+  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5cefc1a7de..72890be4b4 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -280,7 +280,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = Spec.D.top ()
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun _ -> failwith "Global initializers should never spawn threads. What is going on?")
+        ; spawn   = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
         ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
@@ -385,7 +385,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = st
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+        ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
@@ -417,7 +417,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = st
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+        ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
diff --git a/src/framework/resultQuery.ml b/src/framework/resultQuery.ml
index ce5839ef30..c676c41c14 100644
--- a/src/framework/resultQuery.ml
+++ b/src/framework/resultQuery.ml
@@ -18,7 +18,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = local
       ; global = (fun g -> try EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g)) with Not_found -> Spec.G.bot ()) (* see 29/29 on why fallback is needed *)
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in witness context.")
+      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in witness context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
       }
@@ -37,7 +37,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = local
       ; global = (fun g -> try EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g)) with Not_found -> Spec.G.bot ()) (* TODO: how can be missing? *)
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in witness context.")
+      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in witness context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
       }
@@ -57,7 +57,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = Spec.startstate GoblintCil.dummyFunDec.svar (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *) (* TODO: is this startstate bad? *)
       ; global = (fun v -> EQSys.G.spec (try GHT.find gh (EQSys.GVar.spec v) with Not_found -> EQSys.G.bot ())) (* TODO: how can be missing? *)
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
+      ; spawn  = (fun ?(multiple=false) v d   -> failwith "Cannot \"spawn\" in query context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
       }
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 75f0e4f81d..c88f3f00c1 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -179,7 +179,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
 
-  let threadenter ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) S.threadenter ((|>) args % (|>) f % (|>) lval)
+  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
   let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
   let event ctx e octx = lift_fun ctx lift' S.event ((|>) (conv octx) % (|>) e)
 end
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index c8d8563909..3c702d199f 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -76,7 +76,7 @@ struct
     step_ctx ctx
 
   let startstate v = `Lifted Automaton.initial
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 2ce16a5997..ad32713fa8 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -199,7 +199,7 @@ struct
     let r = Dom.bindings a in
     List.map (fun (x,v) -> (Dom.singleton x v, b)) r
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let g xs x' ys =
       let ys' = List.map (fun y ->
           let yr = step ctx.prev_node (ctx.context ()) x' (ThreadEntry (lval, f, args)) (nosync x') in (* threadenter called on before-sync state *)
@@ -208,7 +208,7 @@ struct
       in
       ys' @ xs
     in
-    fold' ctx Spec.threadenter (fun h -> h lval f args) g []
+    fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
   let threadspawn ctx lval f args fctx =
     let fd1 = Dom.choose_key (fst fctx.local) in
     map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))

From a32513936348d54c724697aba3943c409585f46a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 24 Sep 2023 17:28:01 +0200
Subject: [PATCH 2/6] Spawn non-unique threads

---
 src/analyses/base.ml                             | 14 +++++++-------
 src/analyses/threadAnalysis.ml                   |  8 +++++++-
 src/framework/constraints.ml                     |  2 +-
 tests/regression/40-threadid/09-multiple.c       | 15 +++++++++++++++
 .../regression/40-threadid/10-multiple-thread.c  | 16 ++++++++++++++++
 5 files changed, 46 insertions(+), 9 deletions(-)
 create mode 100644 tests/regression/40-threadid/09-multiple.c
 create mode 100644 tests/regression/40-threadid/10-multiple-thread.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index cb29cbc0ab..3b6be2eff8 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1902,7 +1902,7 @@ struct
 
 
 
-  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list =
+  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list * bool =
     let create_thread lval arg v =
       try
         (* try to get function declaration *)
@@ -1943,7 +1943,7 @@ struct
           else
             start_funvars
         in
-        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
+        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown, false
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
@@ -1956,9 +1956,9 @@ struct
       let deep_flist = collect_invalidate ~deep:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local deep_args in
       let flist = shallow_flist @ deep_flist in
       let addrs = List.concat_map AD.to_var_may flist in
-      if addrs <> [] then M.debug ~category:Analyzer "Spawning functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
-      List.filter_map (create_thread None None) addrs
-    | _, _ -> []
+      if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
+      List.filter_map (create_thread None None) addrs, true
+    | _, _ -> [], false
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
@@ -2024,9 +2024,9 @@ struct
       let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
       (addr, AD.type_of addr)
     in
-    let forks = forkfun ctx lv f args in
+    let forks, multiple = forkfun ctx lv f args in
     if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple3.second forks);
-    List.iter (BatTuple.Tuple3.uncurry ctx.spawn) forks;
+    List.iter (BatTuple.Tuple3.uncurry (ctx.spawn ~multiple)) forks;
     let st: store = ctx.local in
     let gs = ctx.global in
     let desc = LF.find f in
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 26e6702c25..740cca3a53 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -84,7 +84,13 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+
+  let threadenter ?(multiple=false) ctx lval f args =
+    if multiple then
+      (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
+       ctx.sideg tid (true, TS.bot (), false));
+    [D.bot ()]
+
   let threadspawn ctx lval f args fctx =
     let creator = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx fctx) in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index a7683fb6b3..62b8d46efa 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -584,7 +584,7 @@ struct
     and spawn ?(multiple=false) lval f args =
       (* TODO: adjust ctx node/edge? *)
       (* TODO: don't repeat for all paths that spawn same *)
-      let ds = S.threadenter ctx lval f args in
+      let ds = S.threadenter ~multiple ctx lval f args in
       List.iter (fun d ->
           spawns := (lval, f, args, d) :: !spawns;
           match Cilfacade.find_varinfo_fundec f with
diff --git a/tests/regression/40-threadid/09-multiple.c b/tests/regression/40-threadid/09-multiple.c
new file mode 100644
index 0000000000..5510e5ae07
--- /dev/null
+++ b/tests/regression/40-threadid/09-multiple.c
@@ -0,0 +1,15 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+int main(void) {
+  // This should spawn a non-unique thread
+  unknown(t_fun);
+  return 0;
+}
diff --git a/tests/regression/40-threadid/10-multiple-thread.c b/tests/regression/40-threadid/10-multiple-thread.c
new file mode 100644
index 0000000000..0024d268ec
--- /dev/null
+++ b/tests/regression/40-threadid/10-multiple-thread.c
@@ -0,0 +1,16 @@
+// PARAM: --set ana.activated[+] thread
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+int main(void) {
+  // This should spawn a non-unique thread
+  unknown(t_fun);
+  return 0;
+}

From ccaffc592932a7c6ca219aadc28d6f7b74188fcf Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 25 Sep 2023 13:07:31 +0200
Subject: [PATCH 3/6] Turn optional argument into named argument

---
 src/analyses/abortUnless.ml                  |  2 +-
 src/analyses/accessAnalysis.ml               |  2 +-
 src/analyses/activeLongjmp.ml                |  2 +-
 src/analyses/activeSetjmp.ml                 |  2 +-
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/base.ml                         |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/expsplit.ml                     |  2 +-
 src/analyses/extractPthread.ml               |  2 +-
 src/analyses/fileUse.ml                      |  2 +-
 src/analyses/locksetAnalysis.ml              |  2 +-
 src/analyses/mCP.ml                          |  2 +-
 src/analyses/mallocFresh.ml                  |  2 +-
 src/analyses/malloc_null.ml                  |  2 +-
 src/analyses/modifiedSinceLongjmp.ml         |  2 +-
 src/analyses/mutexTypeAnalysis.ml            |  2 +-
 src/analyses/poisonVariables.ml              |  2 +-
 src/analyses/pthreadSignals.ml               |  2 +-
 src/analyses/region.ml                       |  2 +-
 src/analyses/spec.ml                         |  2 +-
 src/analyses/stackTrace.ml                   |  4 ++--
 src/analyses/symbLocks.ml                    |  2 +-
 src/analyses/taintPartialContexts.ml         |  2 +-
 src/analyses/termination.ml                  |  2 +-
 src/analyses/threadAnalysis.ml               |  2 +-
 src/analyses/threadEscape.ml                 |  2 +-
 src/analyses/threadFlag.ml                   |  2 +-
 src/analyses/threadId.ml                     |  2 +-
 src/analyses/threadReturn.ml                 |  2 +-
 src/analyses/tmpSpecial.ml                   |  2 +-
 src/analyses/tutorials/taint.ml              |  2 +-
 src/analyses/tutorials/unitAnalysis.ml       |  2 +-
 src/analyses/uninit.ml                       |  2 +-
 src/analyses/useAfterFree.ml                 |  2 +-
 src/analyses/varEq.ml                        |  2 +-
 src/analyses/vla.ml                          |  2 +-
 src/analyses/wrapperFunctionAnalysis.ml      |  2 +-
 src/framework/analyses.ml                    |  4 ++--
 src/framework/constraints.ml                 | 20 ++++++++++----------
 src/framework/control.ml                     |  2 +-
 src/util/wideningTokens.ml                   |  2 +-
 src/witness/observerAnalysis.ml              |  2 +-
 src/witness/witnessConstraints.ml            |  2 +-
 43 files changed, 54 insertions(+), 54 deletions(-)

diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 1c77803c7e..5c24e61f7c 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -65,7 +65,7 @@ struct
     false
 
   let startstate v = false
-  let threadenter ?(multiple=false) ctx lval f args = [false]
+  let threadenter ctx ~multiple lval f args = [false]
   let threadspawn ctx lval f args fctx = false
   let exitstate v = false
 end
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index bd1ca528a7..f0025c2f1c 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -54,7 +54,7 @@ struct
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
-  let threadenter ?(multiple=false) ctx lval f args = [()]
+  let threadenter ctx ~multiple lval f args = [()]
   let exitstate  v = ()
   let context fd d = ()
 
diff --git a/src/analyses/activeLongjmp.ml b/src/analyses/activeLongjmp.ml
index 43da8c6512..9baa601ddc 100644
--- a/src/analyses/activeLongjmp.ml
+++ b/src/analyses/activeLongjmp.ml
@@ -26,7 +26,7 @@ struct
 
   (* Initial values don't really matter: overwritten at longjmp call. *)
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml
index a69bf4db95..be13489993 100644
--- a/src/analyses/activeSetjmp.ml
+++ b/src/analyses/activeSetjmp.ml
@@ -25,7 +25,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index d56064a42f..c232ccae9b 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -647,7 +647,7 @@ struct
 
   (* Thread transfer functions. *)
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let st = ctx.local in
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 3b6be2eff8..e824fac013 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2503,7 +2503,7 @@ struct
     in
     combine_one ctx.local after
 
-  let threadenter ?(multiple=false) ctx (lval: lval option) (f: varinfo) (args: exp list): D.t list =
+  let threadenter ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list): D.t list =
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
       [make_entry ~thread:true ctx fd args]
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 3a2cc5798d..820ff69efa 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -155,7 +155,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index 9c610a96bf..141a04283b 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -84,7 +84,7 @@ struct
     in
     emit_splits ctx d
 
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
 
   let threadspawn ctx lval f args fctx =
     emit_splits_ctx ctx
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index 591704cc70..f72f72c1fe 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -1238,7 +1238,7 @@ module Spec : Analyses.MCPSpec = struct
       (Ctx.top ())
 
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let d : D.t = ctx.local in
     let tasks = ctx.global tasks_var in
     (* TODO: optimize finding *)
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index b12953c71c..b8e7fd78f5 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -287,7 +287,7 @@ struct
     | _ -> m
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 56fe960a47..6a816b9e6c 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -18,7 +18,7 @@ struct
   module C = D
 
   let startstate v = D.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let exitstate  v = D.empty ()
 end
 
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index e305e9c7f6..5259bdb6c7 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -565,7 +565,7 @@ struct
     let d = do_emits ctx !emits d q in
     if q then raise Deadcode else d
 
-  let threadenter ?(multiple=false) (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
+  let threadenter (ctx:(D.t, G.t, C.t, V.t) ctx) ~multiple lval f a =
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "threadenter" ~sides ~emits ctx in
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 861e4958bd..e171ad4ea1 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -52,7 +52,7 @@ struct
       | None -> ctx.local
       | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.empty ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 2d90112636..41c251dfce 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -215,7 +215,7 @@ struct
   let name () = "malloc_null"
 
   let startstate v = D.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index d9c8f5102c..7da0030b9a 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -63,7 +63,7 @@ struct
       ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 7051173bd0..66e60aede1 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -65,7 +65,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 8c79626cc9..87dddd1e54 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -61,7 +61,7 @@ struct
     VS.join au ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let event ctx e octx =
diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
index 83455965ec..70f1624922 100644
--- a/src/analyses/pthreadSignals.ml
+++ b/src/analyses/pthreadSignals.ml
@@ -73,7 +73,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = Signals.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
   let exitstate  v = Signals.empty ()
 end
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 9d68221fcd..86cad5684b 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -175,7 +175,7 @@ struct
   let startstate v =
     `Lifted (RegMap.bot ())
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [`Lifted (RegMap.bot ())]
   let threadspawn ctx lval f args fctx = ctx.local
 
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index e5434eb264..c44edd6c87 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -487,7 +487,7 @@ struct
 
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml
index 3d70c50856..3c3bd56640 100644
--- a/src/analyses/stackTrace.ml
+++ b/src/analyses/stackTrace.ml
@@ -21,7 +21,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 end
 
@@ -45,7 +45,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.top ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.push !Tracing.current_loc ctx.local]
 end
 
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index b99ef93039..32be32f73d 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -29,7 +29,7 @@ struct
   let name () = "symb_locks"
 
   let startstate v = D.top ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 25e981dcbf..b45ea54877 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -101,7 +101,7 @@ struct
     d
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.bot ()]
   let threadspawn ctx lval f args fctx =
     match lval with
diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml
index 5e5e0d36f1..0563730fb2 100644
--- a/src/analyses/termination.ml
+++ b/src/analyses/termination.ml
@@ -217,7 +217,7 @@ struct
   (* | _ -> ctx.local *)
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 740cca3a53..ff4b4d5c63 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -85,7 +85,7 @@ struct
 
   let startstate v = D.bot ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     if multiple then
       (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
        ctx.sideg tid (true, TS.bot (), false));
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 0674ebf3d1..0948a3976d 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -150,7 +150,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.bot ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.bot ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index f3b132918a..81e05af679 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -58,7 +58,7 @@ struct
   let access ctx _ =
     is_currently_multi (Analyses.ask_of_ctx ctx)
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
       ctx.emit Events.EnterMultiThreaded;
     [create_tid f]
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index f1de1dfdcb..a9f3fa35f7 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -133,7 +133,7 @@ struct
     | `Lifted node, count -> node, Some count
     | (`Bot | `Top), _ -> ctx.prev_node, None
 
-  let threadenter ?(multiple=false) ctx lval f args:D.t list =
+  let threadenter ctx ~multiple lval f args:D.t list =
     let n, i = indexed_node_for_ctx ctx in
     let+ tid = create_tid ~multiple ctx.local (n, i) f in
     (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
index 176a4d3465..0aed06851a 100644
--- a/src/analyses/threadReturn.ml
+++ b/src/analyses/threadReturn.ml
@@ -28,7 +28,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = true
-  let threadenter ?(multiple=false) ctx lval f args = [true]
+  let threadenter ctx ~multiple lval f args = [true]
   let exitstate  v = D.top ()
 
   let query (ctx: (D.t, _, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index f3d092e59e..046345e627 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -88,7 +88,7 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 166ce2c3f6..7fc3fd7343 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -129,7 +129,7 @@ struct
 
   (* You may leave these alone *)
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index b5fb4d6367..3ecddc2bc0 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -39,7 +39,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index abdcd67aaa..2b388d1190 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -25,7 +25,7 @@ struct
   let name () = "uninit"
 
   let startstate v : D.t = D.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 6033c689e1..0c7a46c35f 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -196,7 +196,7 @@ struct
       end
     | _ -> state
 
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 
   let startstate v = D.bot ()
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 7bd3453b8a..3aaef95265 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -43,7 +43,7 @@ struct
   let name () = "var_eq"
 
   let startstate v = D.top ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/vla.ml b/src/analyses/vla.ml
index 8bd0168de0..665612aa99 100644
--- a/src/analyses/vla.ml
+++ b/src/analyses/vla.ml
@@ -33,7 +33,7 @@ struct
     ctx.local || Cilfacade.isVLAType v.vtype
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
index 89242e044e..a1bec69a8c 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -87,7 +87,7 @@ struct
 
   let startstate v = D.bot ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     (* The new thread receives a fresh counter *)
     [D.bot ()]
 
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 54a3a18f1a..3bb88a6ead 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -444,7 +444,7 @@ sig
   val paths_as_set : (D.t, G.t, C.t, V.t) ctx -> D.t list
 
   (** Returns initial state for created thread. *)
-  val threadenter : ?multiple:bool -> (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t list
+  val threadenter : (D.t, G.t, C.t, V.t) ctx -> multiple:bool -> lval option -> varinfo -> exp list -> D.t list
 
   (** Updates the local state of the creator thread using initial state of created thread. *)
   val threadspawn : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
@@ -696,7 +696,7 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
     ctx.local
 
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 end
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 62b8d46efa..ed492f4237 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -83,8 +83,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     D.lift @@ S.combine_assign (conv ctx) r fe f args fc (D.unlift es) f_ask
 
-  let threadenter ?(multiple=false) ctx lval f args =
-    List.map D.lift @@ (S.threadenter ~multiple) (conv ctx) lval f args
+  let threadenter ctx ~multiple lval f args =
+    List.map D.lift @@ S.threadenter (conv ctx) ~multiple lval f args
 
   let threadspawn ctx lval f args fctx =
     D.lift @@ S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -167,8 +167,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     S.combine_assign (conv ctx) r fe f args (Option.map C.unlift fc) es f_ask
 
-  let threadenter ?(multiple=false) ctx lval f args =
-    S.threadenter ~multiple (conv ctx) lval f args
+  let threadenter ctx ~multiple lval f args =
+    S.threadenter (conv ctx) ~multiple lval f args
 
   let threadspawn ctx lval f args fctx =
     S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -249,7 +249,7 @@ struct
   let combine_env' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
 
-  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
   let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let leq0 = function
@@ -394,7 +394,7 @@ struct
 
   let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
 
-  let threadenter ?(multiple=false) ctx lval f args = S.threadenter ~multiple (conv ctx) lval f args |> List.map (fun d -> (d, snd ctx.local))
+  let threadenter ctx ~multiple lval f args = S.threadenter (conv ctx) ~multiple lval f args |> List.map (fun d -> (d, snd ctx.local))
   let threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let enter ctx r f args =
@@ -485,7 +485,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
 
-  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
   let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
 
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
@@ -1262,7 +1262,7 @@ struct
     let fd1 = D.choose octx.local in
     map ctx Spec.event (fun h -> h e (conv octx fd1))
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let g xs ys = (List.map (fun y -> D.singleton y) ys) @ xs in
     fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
 
@@ -1449,7 +1449,7 @@ struct
   let combine_env ctx = S.combine_env (conv ctx)
   let combine_assign ctx = S.combine_assign (conv ctx)
   let special ctx = S.special (conv ctx)
-  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
+  let threadenter ctx = S.threadenter (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
@@ -1685,7 +1685,7 @@ struct
       List.iter handle_path (S.paths_as_set conv_ctx);
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
-  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
+  let threadenter ctx = S.threadenter (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 72890be4b4..3ec428014b 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -423,7 +423,7 @@ struct
         }
       in
       (* TODO: don't hd *)
-      List.hd (Spec.threadenter ctx None v [])
+      List.hd (Spec.threadenter ctx ~multiple:false None v [])
       (* TODO: do threadspawn to mainfuns? *)
     in
     let prestartstate = Spec.startstate MyCFG.dummy_func.svar in (* like in do_extern_inits *)
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index c88f3f00c1..73c160e3bb 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -179,7 +179,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
 
-  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
+  let threadenter ctx  ~multiple lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
   let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
   let event ctx e octx = lift_fun ctx lift' S.event ((|>) (conv octx) % (|>) e)
 end
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index 3c702d199f..45a547c471 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -76,7 +76,7 @@ struct
     step_ctx ctx
 
   let startstate v = `Lifted Automaton.initial
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index ad32713fa8..1bf6294020 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -199,7 +199,7 @@ struct
     let r = Dom.bindings a in
     List.map (fun (x,v) -> (Dom.singleton x v, b)) r
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let g xs x' ys =
       let ys' = List.map (fun y ->
           let yr = step ctx.prev_node (ctx.context ()) x' (ThreadEntry (lval, f, args)) (nosync x') in (* threadenter called on before-sync state *)

From 7ebddbc89f20e16927eafb6abafa3e79abde2fe8 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Sep 2023 13:48:47 +0200
Subject: [PATCH 4/6] Also pass to threadspawn for history TID + uniqueness

---
 src/analyses/abortUnless.ml                  |  2 +-
 src/analyses/accessAnalysis.ml               |  2 +-
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/base.ml                         |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/expsplit.ml                     |  2 +-
 src/analyses/extractPthread.ml               |  2 +-
 src/analyses/fileUse.ml                      |  2 +-
 src/analyses/mCP.ml                          |  4 +-
 src/analyses/mallocFresh.ml                  |  2 +-
 src/analyses/malloc_null.ml                  |  2 +-
 src/analyses/mutexTypeAnalysis.ml            |  2 +-
 src/analyses/region.ml                       |  2 +-
 src/analyses/spec.ml                         |  2 +-
 src/analyses/symbLocks.ml                    |  2 +-
 src/analyses/taintPartialContexts.ml         |  2 +-
 src/analyses/threadAnalysis.ml               |  2 +-
 src/analyses/threadEscape.ml                 |  2 +-
 src/analyses/threadFlag.ml                   |  2 +-
 src/analyses/threadId.ml                     |  8 +--
 src/analyses/threadJoins.ml                  |  2 +-
 src/analyses/tmpSpecial.ml                   |  2 +-
 src/analyses/tutorials/taint.ml              |  2 +-
 src/analyses/tutorials/unitAnalysis.ml       |  2 +-
 src/analyses/uninit.ml                       |  2 +-
 src/analyses/useAfterFree.ml                 |  2 +-
 src/analyses/varEq.ml                        |  2 +-
 src/cdomains/threadIdDomain.ml               | 55 ++++++++++----------
 src/framework/analyses.ml                    |  4 +-
 src/framework/constraints.ml                 | 30 +++++------
 src/util/wideningTokens.ml                   |  2 +-
 src/witness/observerAnalysis.ml              |  2 +-
 src/witness/witnessConstraints.ml            |  4 +-
 33 files changed, 80 insertions(+), 79 deletions(-)

diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 5c24e61f7c..ee4db69820 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -66,7 +66,7 @@ struct
 
   let startstate v = false
   let threadenter ctx ~multiple lval f args = [false]
-  let threadspawn ctx lval f args fctx = false
+  let threadspawn ctx ~multiple lval f args fctx = false
   let exitstate v = false
 end
 
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index f0025c2f1c..b181a1c70e 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -121,7 +121,7 @@ struct
     ctx.local
 
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx  ~multiple lval f args fctx =
     (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
     begin match lval with
       | None -> ()
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index c232ccae9b..13f549fc44 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -665,7 +665,7 @@ struct
       (* TODO: do something like base? *)
       failwith "relation.threadenter: unknown function"
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     ctx.local
 
   let event ctx e octx =
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index e824fac013..01646a54cf 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2513,7 +2513,7 @@ struct
       let st = special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) ctx.global st f args in
       [st]
 
-  let threadspawn ctx (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
+  let threadspawn ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
     begin match lval with
       | Some lval ->
         begin match ThreadId.get_current (Analyses.ask_of_ctx fctx) with
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 820ff69efa..3b23dc03fc 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -156,7 +156,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index 141a04283b..fef3d9ff9f 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -86,7 +86,7 @@ struct
 
   let threadenter ctx ~multiple lval f args = [ctx.local]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     emit_splits_ctx ctx
 
   let event ctx (event: Events.t) octx =
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index f72f72c1fe..f084a21edb 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -1254,7 +1254,7 @@ module Spec : Analyses.MCPSpec = struct
     [ { f_d with pred = d.pred } ]
 
 
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 
   let exitstate v = D.top ()
 
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index b8e7fd78f5..58257b7843 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -288,7 +288,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 5259bdb6c7..7a7e787ad7 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -578,7 +578,7 @@ struct
     (* TODO: this do_emits is now different from everything else *)
     map (fun d -> do_emits ctx !emits d false) @@ map topo_sort_an @@ n_cartesian_product css
 
-  let threadspawn (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a fctx =
+  let threadspawn (ctx:(D.t, G.t, C.t, V.t) ctx) ~multiple lval f a fctx =
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "threadspawn" ~sides ~emits ctx in
@@ -586,7 +586,7 @@ struct
     let f post_all (n,(module S:MCPSpec),(d,fd)) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "threadspawn" ~post_all ctx'' n d in
       let fctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "threadspawn" ~post_all fctx'' n fd in
-      n, repr @@ S.threadspawn ctx' lval f a fctx'
+      n, repr @@ S.threadspawn ~multiple ctx' lval f a fctx'
     in
     let d, q = map_deadcode f @@ spec_list2 ctx.local fctx.local in
     do_sideg ctx !sides;
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index e171ad4ea1..b45573a801 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -55,7 +55,7 @@ struct
   let threadenter ctx ~multiple lval f args =
     [D.empty ()]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     D.empty ()
 
   module A =
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 41c251dfce..f993db0c6e 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -216,7 +216,7 @@ struct
 
   let startstate v = D.empty ()
   let threadenter ctx ~multiple lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
   let init marshal =
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 66e60aede1..e640a261cd 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -66,7 +66,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 86cad5684b..652526543c 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -177,7 +177,7 @@ struct
 
   let threadenter ctx ~multiple lval f args =
     [`Lifted (RegMap.bot ())]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 
   let exitstate v = `Lifted (RegMap.bot ())
 
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index c44edd6c87..2f754f6160 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -488,7 +488,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 32be32f73d..f6fdd96c2e 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -30,7 +30,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let branch ctx exp tv = ctx.local
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index b45ea54877..88cf532ab2 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -103,7 +103,7 @@ struct
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args =
     [D.bot ()]
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     match lval with
     | Some lv -> taint_lval ctx lv
     | None -> ctx.local
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index ff4b4d5c63..f51e9395db 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -91,7 +91,7 @@ struct
        ctx.sideg tid (true, TS.bot (), false));
     [D.bot ()]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let creator = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx fctx) in
     let repeated = D.mem tid ctx.local in
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 0948a3976d..21a8b69c93 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -153,7 +153,7 @@ struct
   let threadenter ctx ~multiple lval f args =
     [D.bot ()]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     D.join ctx.local @@
     match args with
     | [ptc_arg] ->
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 81e05af679..6bd466caef 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -63,7 +63,7 @@ struct
       ctx.emit Events.EnterMultiThreaded;
     [create_tid f]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
       ctx.emit Events.EnterMultiThreaded;
     D.join ctx.local (Flag.get_main ())
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index a9f3fa35f7..900870a676 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -58,8 +58,8 @@ struct
 
   let create_tid ?(multiple=false) (_, current, (td, _)) ((node, index): Node.t * int option) v =
     match current with
-    | `Lifted current when not multiple ->
-      let+ tid = Thread.threadenter (current, td) node index v in
+    | `Lifted current ->
+      let+ tid = Thread.threadenter ~multiple (current, td) node index v in
       if GobConfig.get_bool "dbg.print_tids" then
         Hashtbl.replace !tids tid ();
       `Lifted tid
@@ -138,10 +138,10 @@ struct
     let+ tid = create_tid ~multiple ctx.local (n, i) f in
     (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let (current_n, current, (td,tdl)) = ctx.local in
     let v, n, i = match fctx.local with `Lifted vni, _, _ -> vni | _ -> failwith "ThreadId.threadspawn" in
-    (current_n, current, (Thread.threadspawn td n i v, Thread.threadspawn tdl n i v))
+    (current_n, current, (Thread.threadspawn ~multiple td n i v, Thread.threadspawn ~multiple tdl n i v))
 
   type marshal = (Thread.t,unit) Hashtbl.t (* TODO: don't use polymorphic Hashtbl *)
   let init (m:marshal option): unit =
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index f2cd36619f..862711073c 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -81,7 +81,7 @@ struct
       )
     | _, _ -> ctx.local
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     if D.is_bot ctx.local then ( (* bot is All threads *)
       M.info ~category:Imprecise "Thread created while ALL threads must-joined, continuing with no threads joined.";
       D.top () (* top is no threads *)
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index 046345e627..9ed6da7c60 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -89,7 +89,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 7fc3fd7343..a978d0faf4 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -130,7 +130,7 @@ struct
   (* You may leave these alone *)
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index 3ecddc2bc0..dc377cdd97 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -40,7 +40,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 2b388d1190..8693599a4d 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -26,7 +26,7 @@ struct
 
   let startstate v : D.t = D.empty ()
   let threadenter ctx ~multiple lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
   let access_address (ask: Queries.ask) write lv =
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 0c7a46c35f..683ddbdcc2 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -197,7 +197,7 @@ struct
     | _ -> state
 
   let threadenter ctx ~multiple lval f args = [ctx.local]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 
   let startstate v = D.bot ()
   let exitstate v = D.top ()
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 3aaef95265..3f5a65516f 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -44,7 +44,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let typ_equal = CilType.Typ.equal (* TODO: Used to have equality checking, which ignores attributes. Is that needed? *)
diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml
index 7193552048..a9646cffd2 100644
--- a/src/cdomains/threadIdDomain.ml
+++ b/src/cdomains/threadIdDomain.ml
@@ -23,7 +23,7 @@ module type Stateless =
 sig
   include S
 
-  val threadenter: Node.t -> int option -> varinfo -> t
+  val threadenter: multiple:bool -> Node.t -> int option -> varinfo -> t
 end
 
 module type Stateful =
@@ -32,8 +32,8 @@ sig
 
   module D: Lattice.S
 
-  val threadenter: t * D.t -> Node.t -> int option -> varinfo -> t list
-  val threadspawn: D.t -> Node.t -> int option -> varinfo -> D.t
+  val threadenter: multiple:bool -> t * D.t -> Node.t -> int option -> varinfo -> t list
+  val threadspawn: multiple:bool -> D.t -> Node.t -> int option -> varinfo -> D.t
 
   (** If it is possible to get a list of threads created thus far, get it *)
   val created: t -> D.t -> (t list) option
@@ -71,9 +71,10 @@ struct
 
   let threadinit v ~multiple: t = (v, None)
 
-  let threadenter l i v: t =
+  let threadenter ~multiple l i v: t =
     if GobConfig.get_bool "ana.thread.include-node" then
-      (v, Some (l, i))
+      let counter = Option.map (fun x -> if multiple then WrapperFunctionAnalysis0.ThreadCreateUniqueCount.top () else x) i in
+      (v, Some (l, counter))
     else
       (v, None)
 
@@ -93,8 +94,8 @@ struct
 
   module D = Lattice.Unit
 
-  let threadenter _ n i v = [threadenter n i v]
-  let threadspawn () _ _ _ = ()
+  let threadenter ~multiple _ n i v = [threadenter ~multiple n i v]
+  let threadspawn ~multiple () _ _ _ = ()
 
   let created _ _ = None
 end
@@ -162,10 +163,10 @@ struct
     else
       ([base_tid], S.empty ())
 
-  let threadenter ((p, _ ) as current, (cs,_)) (n: Node.t) i v =
-    let ni = Base.threadenter n i v in
+  let threadenter ~multiple ((p, _ ) as current, (cs,_)) (n: Node.t) i v =
+    let ni = Base.threadenter ~multiple n i v in
     let ((p', s') as composed) = compose current ni in
-    if is_unique composed && S.mem ni cs then
+    if is_unique composed && (S.mem ni cs || multiple) then
       [(p, S.singleton ni); composed] (* also respawn unique version of the thread to keep it reachable while thread ID sets refer to it *)
     else
       [composed]
@@ -182,12 +183,12 @@ struct
     in
     Some (List.concat_map map_one els)
 
-  let threadspawn (cs,cms) l i v =
-    let e = Base.threadenter l i v in
+  let threadspawn ~multiple (cs,cms) l i v =
+    let e = Base.threadenter ~multiple l i v in
     if S.mem e cs then
       (cs, S.add e cms)
     else
-      (S.add e cs, cms)
+      (S.add e cs, if multiple then S.add e cms else cms)
 
   let is_main = function
     | ([fl], s) when S.is_empty s && Base.is_main fl -> true
@@ -257,24 +258,24 @@ struct
     | (None, Some x'), `Top -> liftp x' (P.D.top ())
     | _ -> None
 
-  let threadenter x n i v =
+  let threadenter ~multiple x n i v =
     match x with
-    | ((Some x', None), `Lifted1 d) -> H.threadenter (x',d) n i v |> List.map (fun t -> (Some t, None))
-    | ((Some x', None), `Bot) -> H.threadenter (x',H.D.bot ()) n i v |> List.map (fun t -> (Some t, None))
-    | ((Some x', None), `Top) -> H.threadenter (x',H.D.top ()) n i v |> List.map (fun t -> (Some t, None))
-    | ((None, Some x'), `Lifted2 d) -> P.threadenter (x',d) n i v |> List.map (fun t -> (None, Some t))
-    | ((None, Some x'), `Bot) -> P.threadenter (x',P.D.bot ()) n i v |> List.map (fun t -> (None, Some t))
-    | ((None, Some x'), `Top) -> P.threadenter (x',P.D.top ()) n i v |> List.map (fun t -> (None, Some t))
+    | ((Some x', None), `Lifted1 d) -> H.threadenter ~multiple (x',d) n i v |> List.map (fun t -> (Some t, None))
+    | ((Some x', None), `Bot) -> H.threadenter ~multiple (x',H.D.bot ()) n i v |> List.map (fun t -> (Some t, None))
+    | ((Some x', None), `Top) -> H.threadenter ~multiple (x',H.D.top ()) n i v |> List.map (fun t -> (Some t, None))
+    | ((None, Some x'), `Lifted2 d) -> P.threadenter ~multiple (x',d) n i v |> List.map (fun t -> (None, Some t))
+    | ((None, Some x'), `Bot) -> P.threadenter ~multiple (x',P.D.bot ()) n i v |> List.map (fun t -> (None, Some t))
+    | ((None, Some x'), `Top) -> P.threadenter ~multiple (x',P.D.top ()) n i v |> List.map (fun t -> (None, Some t))
     | _ -> failwith "FlagConfiguredTID received a value where not exactly one component is set"
 
-  let threadspawn x n i v =
+  let threadspawn ~multiple x n i v =
     match x with
-    | `Lifted1 x' -> `Lifted1 (H.threadspawn x' n i v)
-    | `Lifted2 x' -> `Lifted2 (P.threadspawn x' n i v)
-    | `Bot when history_enabled () -> `Lifted1 (H.threadspawn (H.D.bot ()) n i v)
-    | `Bot  -> `Lifted2 (P.threadspawn (P.D.bot ()) n i v)
-    | `Top when history_enabled () -> `Lifted1 (H.threadspawn (H.D.top ()) n i v)
-    | `Top  -> `Lifted2 (P.threadspawn (P.D.top ()) n i v)
+    | `Lifted1 x' -> `Lifted1 (H.threadspawn ~multiple x' n i v)
+    | `Lifted2 x' -> `Lifted2 (P.threadspawn ~multiple x' n i v)
+    | `Bot when history_enabled () -> `Lifted1 (H.threadspawn  ~multiple (H.D.bot ()) n i v)
+    | `Bot  -> `Lifted2 (P.threadspawn  ~multiple (P.D.bot ()) n i v)
+    | `Top when history_enabled () -> `Lifted1 (H.threadspawn ~multiple (H.D.top ()) n i v)
+    | `Top  -> `Lifted2 (P.threadspawn ~multiple (P.D.top ()) n i v)
 
   let name () = "FlagConfiguredTID: " ^ if history_enabled () then H.name () else P.name ()
 end
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 3bb88a6ead..e1a4560003 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -447,7 +447,7 @@ sig
   val threadenter : (D.t, G.t, C.t, V.t) ctx -> multiple:bool -> lval option -> varinfo -> exp list -> D.t list
 
   (** Updates the local state of the creator thread using initial state of created thread. *)
-  val threadspawn : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
+  val threadspawn : (D.t, G.t, C.t, V.t) ctx -> multiple:bool -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
 
   val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
 end
@@ -697,7 +697,7 @@ struct
     ctx.local
 
   let threadenter ctx ~multiple lval f args = [ctx.local]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 end
 
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index ed492f4237..f474df6834 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -86,8 +86,8 @@ struct
   let threadenter ctx ~multiple lval f args =
     List.map D.lift @@ S.threadenter (conv ctx) ~multiple lval f args
 
-  let threadspawn ctx lval f args fctx =
-    D.lift @@ S.threadspawn (conv ctx) lval f args (conv fctx)
+  let threadspawn ctx ~multiple lval f args fctx =
+    D.lift @@ S.threadspawn (conv ctx) ~multiple lval f args (conv fctx)
 
   let paths_as_set ctx =
     List.map (fun x -> D.lift x) @@ S.paths_as_set (conv ctx)
@@ -170,8 +170,8 @@ struct
   let threadenter ctx ~multiple lval f args =
     S.threadenter (conv ctx) ~multiple lval f args
 
-  let threadspawn ctx lval f args fctx =
-    S.threadspawn (conv ctx) lval f args (conv fctx)
+  let threadspawn ctx ~multiple lval f args fctx =
+    S.threadspawn (conv ctx) ~multiple lval f args (conv fctx)
 
   let paths_as_set ctx = S.paths_as_set (conv ctx)
   let event ctx e octx = S.event (conv ctx) e (conv octx)
@@ -250,7 +250,7 @@ struct
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
 
   let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
-  let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx (lift ctx) (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let leq0 = function
     | `Top -> false
@@ -395,7 +395,7 @@ struct
   let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
 
   let threadenter ctx ~multiple lval f args = S.threadenter (conv ctx) ~multiple lval f args |> List.map (fun d -> (d, snd ctx.local))
-  let threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let enter ctx r f args =
     let m = snd ctx.local in
@@ -486,7 +486,7 @@ struct
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
 
   let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
-  let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx D.lift (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
 
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
 end
@@ -563,7 +563,7 @@ struct
     if !AnalysisState.postsolving then
       sideg (GVar.contexts f) (G.create_contexts (G.CSet.singleton c))
 
-  let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) ctx * D.t list ref * (lval option * varinfo * exp list * D.t) list ref =
+  let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) ctx * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
     let r = ref [] in
     let spawns = ref [] in
     (* now watch this ... *)
@@ -586,7 +586,7 @@ struct
       (* TODO: don't repeat for all paths that spawn same *)
       let ds = S.threadenter ~multiple ctx lval f args in
       List.iter (fun d ->
-          spawns := (lval, f, args, d) :: !spawns;
+          spawns := (lval, f, args, d, multiple) :: !spawns;
           match Cilfacade.find_varinfo_fundec f with
           | fd ->
             let c = S.context fd d in
@@ -618,14 +618,14 @@ struct
         }
       in
       (* TODO: don't forget path dependencies *)
-      let one_spawn (lval, f, args, fd) =
+      let one_spawn (lval, f, args, fd, multiple) =
         let rec fctx =
           { ctx with
             ask = (fun (type a) (q: a Queries.t) -> S.query fctx q)
           ; local = fd
           }
         in
-        S.threadspawn ctx' lval f args fctx
+        S.threadspawn ctx' ~multiple lval f args fctx
       in
       bigsqcup (List.map one_spawn spawns)
 
@@ -1266,9 +1266,9 @@ struct
     let g xs ys = (List.map (fun y -> D.singleton y) ys) @ xs in
     fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let fd1 = D.choose fctx.local in
-    map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))
+    map ctx (Spec.threadspawn ~multiple) (fun h -> h lval f args (conv fctx fd1))
 
   let sync ctx reason = map ctx Spec.sync (fun h -> h reason)
 
@@ -1450,7 +1450,7 @@ struct
   let combine_assign ctx = S.combine_assign (conv ctx)
   let special ctx = S.special (conv ctx)
   let threadenter ctx = S.threadenter (conv ctx)
-  let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
+  let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
   let asm ctx = S.asm (conv ctx)
@@ -1686,7 +1686,7 @@ struct
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
   let threadenter ctx = S.threadenter (conv ctx)
-  let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
+  let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
   let asm ctx = S.asm (conv ctx)
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 73c160e3bb..1816de90c7 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -180,6 +180,6 @@ struct
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
 
   let threadenter ctx  ~multiple lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
-  let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx lift' (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
   let event ctx e octx = lift_fun ctx lift' S.event ((|>) (conv octx) % (|>) e)
 end
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index 45a547c471..e8daf56155 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -77,7 +77,7 @@ struct
 
   let startstate v = `Lifted Automaton.initial
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 1bf6294020..8dedf77a79 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -209,9 +209,9 @@ struct
       ys' @ xs
     in
     fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let fd1 = Dom.choose_key (fst fctx.local) in
-    map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))
+    map ctx (Spec.threadspawn ~multiple) (fun h -> h lval f args (conv fctx fd1))
 
   let sync ctx reason =
     fold'' ctx Spec.sync (fun h -> h reason) (fun (a, async) x r a' ->

From 44ef0843efac4839f45f267f015ace6a27a88414 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Sep 2023 13:54:36 +0200
Subject: [PATCH 5/6] Add example for race despite uniqueness counter

---
 .../40-threadid/11-multiple-unique-counter.c     | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 tests/regression/40-threadid/11-multiple-unique-counter.c

diff --git a/tests/regression/40-threadid/11-multiple-unique-counter.c b/tests/regression/40-threadid/11-multiple-unique-counter.c
new file mode 100644
index 0000000000..37c08ae61a
--- /dev/null
+++ b/tests/regression/40-threadid/11-multiple-unique-counter.c
@@ -0,0 +1,16 @@
+// PARAM: --set ana.thread.unique_thread_id_count 4
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+int main(void) {
+  // This should spawn a non-unique thread
+  unknown(t_fun);
+  return 0;
+}

From b718e46241c0c4f9b926620060a8743c3c49b6d7 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Sep 2023 14:04:49 +0200
Subject: [PATCH 6/6] Add check that only one mainfun is specified to
 privatizations

---
 src/analyses/basePriv.ml   | 2 +-
 src/analyses/commonPriv.ml | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 0154924a1c..3843dda300 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -893,7 +893,7 @@ end
 module MinePrivBase =
 struct
   include NoFinalize
-  include ConfCheck.RequireMutexPathSensInit
+  include ConfCheck.RequireMutexPathSensOneMainInit
   include MutexGlobals (* explicit not needed here because G is Prod anyway? *)
 
   let thread_join ?(force=false) ask get e st = st
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 1b92cb320d..38a8dfe1b7 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -19,12 +19,14 @@ struct
       if not mutex_active then failwith "Privatization (to be useful) requires the 'mutex' analysis to be enabled (it is currently disabled)"
   end
 
-  module RequireMutexPathSensInit =
+  module RequireMutexPathSensOneMainInit =
   struct
     let init () =
       RequireMutexActivatedInit.init ();
       let mutex_path_sens = List.mem "mutex" (GobConfig.get_string_list "ana.path_sens") in
       if not mutex_path_sens then failwith "The activated privatization requires the 'mutex' analysis to be enabled & path sensitive (it is currently enabled, but not path sensitive)";
+      let mainfuns = List.length @@ GobConfig.get_list "mainfun" in
+      if not (mainfuns = 1) then failwith "The activated privatization requires exactly one main function to be specified";
       ()
   end