diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 813d999ac3..ee4db69820 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -65,8 +65,8 @@ struct
     false
 
   let startstate v = false
-  let threadenter ctx lval f args = [false]
-  let threadspawn ctx lval f args fctx = false
+  let threadenter ctx ~multiple lval f args = [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 e99aefa0e5..b181a1c70e 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 ctx ~multiple lval f args = [()]
   let exitstate  v = ()
   let context fd d = ()
 
@@ -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/activeLongjmp.ml b/src/analyses/activeLongjmp.ml
index 9c9868e32f..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 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 069111d3ba..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 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 46c620f390..13f549fc44 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 ctx ~multiple lval f args =
     let st = ctx.local in
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
@@ -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 6536a9c496..a8ad9af95b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1944,7 +1944,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 *)
@@ -1985,7 +1985,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.
@@ -1998,9 +1998,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 *)
@@ -2131,9 +2131,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
@@ -2641,7 +2641,7 @@ struct
     in
     combine_one ctx.local after
 
-  let threadenter 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]
@@ -2651,7 +2651,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/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 793978980b..88181000b9 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
 
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 04b148dd02..3b23dc03fc 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -155,8 +155,8 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
+  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 f121d0380e..fef3d9ff9f 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -84,9 +84,9 @@ struct
     in
     emit_splits ctx d
 
-  let threadenter ctx lval f args = [ctx.local]
+  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 60e389fedf..f084a21edb 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 ctx ~multiple lval f args =
     let d : D.t = ctx.local in
     let tasks = ctx.global tasks_var in
     (* TODO: optimize finding *)
@@ -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 a9088a4bb2..58257b7843 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -287,8 +287,8 @@ struct
     | _ -> m
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
+  let threadspawn ctx ~multiple 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..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 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 9eb21b77ef..50f6d5409b 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 get_bool "exp.single-threaded" then
       M.msg_final Error ~category:Unsound "Thread not spawned"
@@ -324,8 +324,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)
@@ -567,20 +567,20 @@ 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 (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
     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;
     (* 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
@@ -588,7 +588,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 3a501fc72f..d1314d5009 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -52,10 +52,10 @@ struct
       | None -> ctx.local
       | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-  let threadenter ctx lval f args =
+  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 4d5871cb80..f993db0c6e 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -215,8 +215,8 @@ struct
   let name () = "malloc_null"
 
   let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
   let init marshal =
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index 5dae8748cb..a129c9f92c 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -57,7 +57,7 @@ struct
       ctx.local
 
   let startstate v = D.bot ()
-  let threadenter 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 806c35f464..e640a261cd 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -65,8 +65,8 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.top ()]
+  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/poisonVariables.ml b/src/analyses/poisonVariables.ml
index acd687835e..865cb928aa 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -65,7 +65,7 @@ struct
     VS.join au ctx.local
 
   let startstate v = D.bot ()
-  let threadenter 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 0b776282e8..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 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 6d2ae246c3..652526543c 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -175,9 +175,9 @@ struct
   let startstate v =
     `Lifted (RegMap.bot ())
 
-  let threadenter ctx lval f args =
+  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 54ffcd2697..2f754f6160 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -487,8 +487,8 @@ struct
 
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
+  let threadspawn ctx ~multiple 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..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 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 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 d8cebf51d2..f6fdd96c2e 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -29,8 +29,8 @@ struct
   let name () = "symb_locks"
 
   let startstate v = D.top ()
-  let threadenter ctx lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.top ()]
+  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 feb9599977..85dabd1c9d 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -88,9 +88,9 @@ struct
     d
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args =
+  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/termination.ml b/src/analyses/termination.ml
index 6da9225d3f..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 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 1e679a4707..f51e9395db 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -84,8 +84,14 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx =
+
+  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));
+    [D.bot ()]
+
+  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 9ed62e7422..21a8b69c93 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -150,10 +150,10 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.bot ()
 
-  let threadenter ctx lval f args =
+  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 f2ebf82be1..6bd466caef 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -58,12 +58,12 @@ struct
   let access ctx _ =
     is_currently_multi (Analyses.ask_of_ctx ctx)
 
-  let threadenter 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]
 
-  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 8144aea507..da2c688ad1 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -75,10 +75,10 @@ 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 ->
-      let+ tid = Thread.threadenter (current, td) node index v in
+      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
@@ -152,15 +152,15 @@ struct
     | `Lifted node, count -> node, Some count
     | (`Bot | `Top), _ -> ctx.prev_node, None
 
-  let threadenter 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 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 =
+  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/threadReturn.ml b/src/analyses/threadReturn.ml
index 470c4ceaa8..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 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 2d38972d7a..9ed6da7c60 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -88,8 +88,8 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
+  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 3067449e31..a978d0faf4 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -129,8 +129,8 @@ struct
 
   (* You may leave these alone *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.top ()]
+  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 d3b8c69bfd..dc377cdd97 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -39,8 +39,8 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.top ()]
+  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 f8759d9134..8693599a4d 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -25,8 +25,8 @@ struct
   let name () = "uninit"
 
   let startstate v : D.t = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
+  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 ef63ab3e91..a901a8d2e5 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -243,4 +243,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 dcd49c9f02..30b36404af 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -43,8 +43,8 @@ struct
   let name () = "var_eq"
 
   let startstate v = D.top ()
-  let threadenter ctx lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.top ()]
+  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/analyses/vla.ml b/src/analyses/vla.ml
index 865f22b20a..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 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 e98597a66a..2e068329ea 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -96,7 +96,7 @@ struct
 
   let startstate v = D.bot ()
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     (* The new thread receives a fresh counter *)
     [D.bot ()]
 
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 bb2170509d..eec811afc4 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,10 +444,10 @@ 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 : (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,8 +697,8 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
     ctx.local
 
-  let threadenter ctx lval f args = [ctx.local]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [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 812d056de4..cc54c91a5a 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -83,11 +83,11 @@ 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 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)
@@ -167,11 +167,11 @@ 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 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)
@@ -249,8 +249,8 @@ 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 threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) 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 ~multiple lval f args fctx = lift_fun ctx (lift ctx) (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let leq0 = function
     | `Top -> false
@@ -394,8 +394,8 @@ 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 threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  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 ~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
@@ -485,8 +485,8 @@ 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 threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
+  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 ... *)
@@ -581,12 +581,12 @@ 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
+      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)
 
@@ -899,7 +899,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.")
       }
@@ -1263,12 +1263,13 @@ 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 ctx ~multiple 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 []
-  let threadspawn ctx lval f args fctx =
+    fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
+
+  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)
 
@@ -1451,7 +1452,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)
@@ -1689,7 +1690,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/framework/control.ml b/src/framework/control.ml
index 9baa2dd1ca..a45ec5a057 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,13 +417,13 @@ 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))
         }
       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/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..1816de90c7 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 threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) 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 ~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 c8d8563909..e8daf56155 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -76,8 +76,8 @@ struct
     step_ctx ctx
 
   let startstate v = `Lifted Automaton.initial
-  let threadenter ctx lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx ~multiple lval f args = [D.top ()]
+  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 2ce16a5997..8dedf77a79 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 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 *)
@@ -208,10 +208,10 @@ struct
       in
       ys' @ xs
     in
-    fold' ctx Spec.threadenter (fun h -> h lval f args) g []
-  let threadspawn ctx lval f args fctx =
+    fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
+  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' ->
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;
+}
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;
+}