From 94d5e3ed77217da53ee8895391208cd8b0d3877c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 10:34:54 +0300
Subject: [PATCH 01/14] Add test 00-sanity/42-no-threadflag

---
 tests/regression/00-sanity/42-no-threadflag.c | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 tests/regression/00-sanity/42-no-threadflag.c

diff --git a/tests/regression/00-sanity/42-no-threadflag.c b/tests/regression/00-sanity/42-no-threadflag.c
new file mode 100644
index 0000000000..2bd9061f10
--- /dev/null
+++ b/tests/regression/00-sanity/42-no-threadflag.c
@@ -0,0 +1,13 @@
+// PARAM: --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs
+// Also no threadid which can tell being single-threaded
+// With earlyglobs disabled: no threadflag means the same behavior
+#include <goblint.h>
+
+int g;
+
+int main() {
+  __goblint_check(g == 0); // UNKNOWN (no threadflag)
+  g = 1; // RACE (no threadflag)
+  __goblint_check(g == 1); // UNKNOWN (no threadflag)
+  return 0;
+}

From c540556a13aef93d1be6ae5f681b7b87487ac83f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 10:35:11 +0300
Subject: [PATCH 02/14] Add TODOs about exp.single-threaded errors

---
 src/analyses/mCP.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index b972195bad..1e4d91972c 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -152,7 +152,7 @@ struct
       List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d
     in
     if get_bool "exp.single-threaded" then
-      M.msg_final Error ~category:Unsound "Thread not spawned"
+      M.msg_final Error ~category:Unsound "Thread not spawned" (* TODO: non-final error *) (* TODO: only final error if xs is non-empty *)
     else
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 

From c6a696e0e12d5669652fdb66a97c73749bbd59f2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 10:37:09 +0300
Subject: [PATCH 03/14] Add test 00-sanity/43-no-threadflag-single-threaded

---
 .../00-sanity/43-no-threadflag-single-threaded.c     | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 tests/regression/00-sanity/43-no-threadflag-single-threaded.c

diff --git a/tests/regression/00-sanity/43-no-threadflag-single-threaded.c b/tests/regression/00-sanity/43-no-threadflag-single-threaded.c
new file mode 100644
index 0000000000..6b78c3c68e
--- /dev/null
+++ b/tests/regression/00-sanity/43-no-threadflag-single-threaded.c
@@ -0,0 +1,12 @@
+// PARAM: --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs --enable exp.single-threaded
+// Like 00-sanity/42-no-threadflag but forced single-threaded
+#include <goblint.h>
+
+int g;
+
+int main() {
+  __goblint_check(g == 0); // TODO SUCCESS (forced single-threaded)
+  g = 1; // TODO NORACE (forced single-threaded)
+  __goblint_check(g == 1); // TODO SUCCESS (forced single-threaded)
+  return 0;
+}

From f925048495fd8e34ccad8646abbd82c9a1b690ff Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 10:58:39 +0300
Subject: [PATCH 04/14] Use MustBeSingleThreaded query via ThreadFlag functions

---
 src/analyses/apron/relationPriv.apron.ml |  8 ++++----
 src/analyses/basePriv.ml                 |  4 ++--
 src/analyses/memLeak.ml                  | 10 ++++------
 src/analyses/singleThreadedLifter.ml     |  3 +--
 src/analyses/threadEscape.ml             |  1 +
 src/analyses/threadFlag.ml               |  2 ++
 src/analyses/useAfterFree.ml             |  2 +-
 src/analyses/varEq.ml                    |  2 +-
 src/analyses/wrapperFunctionAnalysis.ml  |  2 +-
 src/domains/queries.ml                   |  2 +-
 10 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 9e22fff21c..d7c8acbd49 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -102,7 +102,7 @@ struct
 
   let sync (ask: Q.ask) getg sideg (st: relation_components_t) reason =
     let branched_sync () =
-      if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
+      if not (ThreadFlag.has_ever_been_multi ask) then
         st
       else
         (* must be like enter_multithreaded *)
@@ -351,7 +351,7 @@ struct
 
   let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
     let branched_sync () =
-      if ask.f (Q.MustBeSingleThreaded { since_start= true }) then
+      if not (ThreadFlag.has_ever_been_multi ask) then
         st
       else
         (* must be like enter_multithreaded *)
@@ -647,7 +647,7 @@ struct
 
   let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
     let branched_sync () =
-      if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
+      if not (ThreadFlag.has_ever_been_multi ask) then
         st
       else
         let rel = st.rel in
@@ -1272,7 +1272,7 @@ struct
 
   let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason =
     let branched_sync () =
-      if ask.f (Q.MustBeSingleThreaded {since_start = true}) then
+      if not (ThreadFlag.has_ever_been_multi ask) then
         st
       else
         let rel = st.rel in
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index e40db604cf..b56df13c65 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -579,7 +579,7 @@ struct
     let digest = Digest.current ask in
     let sidev = GMutex.singleton digest (CPA.singleton x v) in
     let l' = L.add lm (CPA.singleton x v) l in
-    let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in
+    let is_recovered_st = ThreadFlag.has_ever_been_multi ask && not @@ ThreadFlag.is_currently_multi ask in
     let l' = if is_recovered_st then
         (* update value of local record for all where it appears *)
         L.map (update_if_mem x v) l'
@@ -705,7 +705,7 @@ struct
     {st with cpa = CPA.bot (); priv = (W.bot (),lmust,l)}
 
   let threadspawn (ask:Queries.ask) get set (st: BaseComponents (D).t) =
-    let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in
+    let is_recovered_st = ThreadFlag.has_ever_been_multi ask && not @@ ThreadFlag.is_currently_multi ask in
     let unprotected_after x = ask.f (Q.MayBePublic {global=x; kind=Write; protection=Weak}) in
     if is_recovered_st then
       (* Remove all things that are now unprotected *)
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 133527b1b5..c86f3c4ff6 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -22,9 +22,6 @@ struct
 
   let context man _ d = d
 
-  let must_be_single_threaded ~since_start man =
-    man.ask (Queries.MustBeSingleThreaded { since_start })
-
   let was_malloc_called man =
     man.global ()
 
@@ -142,7 +139,7 @@ struct
 
   let warn_for_multi_threaded_due_to_abort man =
     let malloc_called = was_malloc_called man in
-    if not (must_be_single_threaded man ~since_start:true) && malloc_called then (
+    if ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) && malloc_called then (
       set_mem_safety_flag InvalidMemTrack;
       set_mem_safety_flag InvalidMemcleanup;
       M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program aborted while running in multi-threaded mode. A memory leak might occur"
@@ -184,13 +181,14 @@ struct
   let return man (exp:exp option) (f:fundec) : D.t =
     (* Check for a valid-memcleanup and memtrack violation in a multi-threaded setting *)
     (* The check for multi-threadedness is to ensure that valid-memtrack and valid-memclenaup are treated separately for single-threaded programs *)
-    if (man.ask (Queries.MayBeThreadReturn) &&  not (must_be_single_threaded man ~since_start:true)) then (
+    let ask = Analyses.ask_of_man man in
+    if man.ask (Queries.MayBeThreadReturn) && ThreadFlag.has_ever_been_multi ask then (
       warn_for_thread_return_or_exit man true
     );
     (* Returning from "main" is one possible program exit => need to check for memory leaks *)
     if f.svar.vname = "main" then (
       check_for_mem_leak man;
-      if not (must_be_single_threaded man ~since_start:false) && was_malloc_called man then begin
+      if ThreadFlag.is_currently_multi ask && was_malloc_called man then begin
         set_mem_safety_flag InvalidMemTrack;
         set_mem_safety_flag InvalidMemcleanup;
         M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Possible memory leak: Memory was allocated in a multithreaded program, but not all threads are joined."
diff --git a/src/analyses/singleThreadedLifter.ml b/src/analyses/singleThreadedLifter.ml
index 3fed5ed222..af2c4aeccf 100644
--- a/src/analyses/singleThreadedLifter.ml
+++ b/src/analyses/singleThreadedLifter.ml
@@ -7,8 +7,7 @@ module SingleThreadedLifter (S: MCPSpec) =
 struct
   include S
 
-  let is_multithreaded (ask:Queries.ask) =
-    not @@ ask.f (MustBeSingleThreaded {since_start = true})
+  let is_multithreaded = ThreadFlag.has_ever_been_multi
 
   let query ctx =
     let return_top (type a) (q: a Queries.t) =
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 2bf67f4bb9..4fb67b6e99 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -7,6 +7,7 @@ module M = Messages
 module AD = Queries.AD
 
 let has_escaped (ask: Queries.ask) (v: varinfo): bool =
+  (* TODO: exp.single-threaded override *)
   assert (not v.vglob);
   if not v.vaddrof then
     false (* Cannot have escaped without taking address. Override provides extra precision for degenerate ask in base eval_exp used for partitioned arrays. *)
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 1e0ff7db9f..7e4f3f7057 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -6,10 +6,12 @@ open GoblintCil
 open Analyses
 
 let is_currently_multi (ask: Queries.ask): bool =
+  (* TODO: exp.single-threaded override *)
   if !AnalysisState.global_initialization then false else
     not (ask.f (Queries.MustBeSingleThreaded {since_start = false}))
 
 let has_ever_been_multi (ask: Queries.ask): bool =
+  (* TODO: exp.single-threaded override *)
   if !AnalysisState.global_initialization then false else
     not (ask.f (Queries.MustBeSingleThreaded {since_start = true}))
 
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index cc94866c7e..fa170a5b28 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -34,7 +34,7 @@ struct
   let warn_for_multi_threaded_access man ?(is_free = false) (heap_var:varinfo) behavior cwe_number =
     let freeing_threads = man.global heap_var in
     (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *)
-    if man.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then ()
+    if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) || G.is_empty freeing_threads then ()
     else begin
       let other_possibly_started current tid joined_threads =
         match tid with
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 0c51cbaf60..fc7434e6bf 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -471,7 +471,7 @@ struct
     let d_local =
       (* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
          TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *)
-      if Queries.AD.is_top tainted || not (man.ask (Queries.MustBeSingleThreaded {since_start = true})) then
+      if Queries.AD.is_top tainted || ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) then
         D.top ()
       else
         let taint_exp =
diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
index ea8572d867..185b6941f7 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -176,7 +176,7 @@ module MallocWrapper : MCPSpec = struct
                              | `Lifted tid -> not (Thread.is_unique tid)
                              | _ ->
                                (* The thread analysis may be completely disabled; in this case we fall back on checking whether the program has been single threaded since start *)
-                               not (man.ask (Q.MustBeSingleThreaded {since_start = true}))
+                               ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)
                             )
         | None -> false
       end
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 6b85a2729c..448f3fd7c5 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -91,7 +91,7 @@ type _ t =
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
   | MustLockset: LockDomain.MustLockset.t t
   | MustBeAtomic: MustBool.t t
-  | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t
+  | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t (** Use via {!ThreadFlag.is_currently_multi} and {!ThreadFlag.has_ever_been_multi}. *)
   | MustBeUniqueThread: MustBool.t t
   | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t
   | ThreadCreateIndexedNode: ThreadNodeLattice.t t

From 86db1cde6e9b31d0539edbec91d31305be212fec Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:00:54 +0300
Subject: [PATCH 05/14] Use exp.single-threaded for ThreadFlag queries

---
 src/analyses/threadFlag.ml                                  | 6 ++----
 .../regression/00-sanity/43-no-threadflag-single-threaded.c | 6 +++---
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 7e4f3f7057..8e341aed4c 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -6,13 +6,11 @@ open GoblintCil
 open Analyses
 
 let is_currently_multi (ask: Queries.ask): bool =
-  (* TODO: exp.single-threaded override *)
-  if !AnalysisState.global_initialization then false else
+  if !AnalysisState.global_initialization || GobConfig.get_bool "exp.single-threaded" then false else
     not (ask.f (Queries.MustBeSingleThreaded {since_start = false}))
 
 let has_ever_been_multi (ask: Queries.ask): bool =
-  (* TODO: exp.single-threaded override *)
-  if !AnalysisState.global_initialization then false else
+  if !AnalysisState.global_initialization || GobConfig.get_bool "exp.single-threaded" then false else
     not (ask.f (Queries.MustBeSingleThreaded {since_start = true}))
 
 module Spec =
diff --git a/tests/regression/00-sanity/43-no-threadflag-single-threaded.c b/tests/regression/00-sanity/43-no-threadflag-single-threaded.c
index 6b78c3c68e..059e78a971 100644
--- a/tests/regression/00-sanity/43-no-threadflag-single-threaded.c
+++ b/tests/regression/00-sanity/43-no-threadflag-single-threaded.c
@@ -5,8 +5,8 @@
 int g;
 
 int main() {
-  __goblint_check(g == 0); // TODO SUCCESS (forced single-threaded)
-  g = 1; // TODO NORACE (forced single-threaded)
-  __goblint_check(g == 1); // TODO SUCCESS (forced single-threaded)
+  __goblint_check(g == 0); // SUCCESS (forced single-threaded)
+  g = 1; // NORACE (forced single-threaded)
+  __goblint_check(g == 1); // SUCCESS (forced single-threaded)
   return 0;
 }

From 3b780e552224663e95e421bed682e4ebb054f356 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:02:31 +0300
Subject: [PATCH 06/14] Add test
 00-sanity/44-no-threadflag-single-threaded-earlyglobs

---
 .../44-no-threadflag-single-threaded-earlyglobs.c    | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c

diff --git a/tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c b/tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c
new file mode 100644
index 0000000000..5f0f87f41b
--- /dev/null
+++ b/tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c
@@ -0,0 +1,12 @@
+// PARAM: --set ana.activated[-] threadflag --set ana.activated[-] threadid --enable exp.earlyglobs --enable exp.single-threaded
+// Like 00-sanity/43-no-threadflag-single-threaded but with earlyglobs enabled
+#include <goblint.h>
+
+int g;
+
+int main() {
+  __goblint_check(g == 0); // UNKNOWN (earlyglobs)
+  g = 1; // NORACE (forced single-threaded)
+  __goblint_check(g == 1); // UNKNOWN (earlyglobs)
+  return 0;
+}

From a68a47b3cf89f807ca7913a554fe3b7087bf567b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:11:21 +0300
Subject: [PATCH 07/14] Combine 00-sanity/*-no-threadflag* tests into one cram
 test

---
 tests/regression/00-sanity/42-no-threadflag.c | 10 ++--
 tests/regression/00-sanity/42-no-threadflag.t | 50 +++++++++++++++++++
 .../43-no-threadflag-single-threaded.c        | 12 -----
 ...no-threadflag-single-threaded-earlyglobs.c | 12 -----
 4 files changed, 54 insertions(+), 30 deletions(-)
 create mode 100644 tests/regression/00-sanity/42-no-threadflag.t
 delete mode 100644 tests/regression/00-sanity/43-no-threadflag-single-threaded.c
 delete mode 100644 tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c

diff --git a/tests/regression/00-sanity/42-no-threadflag.c b/tests/regression/00-sanity/42-no-threadflag.c
index 2bd9061f10..9b1a7689cb 100644
--- a/tests/regression/00-sanity/42-no-threadflag.c
+++ b/tests/regression/00-sanity/42-no-threadflag.c
@@ -1,13 +1,11 @@
-// PARAM: --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs
-// Also no threadid which can tell being single-threaded
-// With earlyglobs disabled: no threadflag means the same behavior
+// CRAM
 #include <goblint.h>
 
 int g;
 
 int main() {
-  __goblint_check(g == 0); // UNKNOWN (no threadflag)
-  g = 1; // RACE (no threadflag)
-  __goblint_check(g == 1); // UNKNOWN (no threadflag)
+  __goblint_check(g == 0);
+  g = 1;
+  __goblint_check(g == 1);
   return 0;
 }
diff --git a/tests/regression/00-sanity/42-no-threadflag.t b/tests/regression/00-sanity/42-no-threadflag.t
new file mode 100644
index 0000000000..846fc4d007
--- /dev/null
+++ b/tests/regression/00-sanity/42-no-threadflag.t
@@ -0,0 +1,50 @@
+Analysis of single-threaded program with threadflag deactivated.
+Also no threadid which can tell being single-threaded.
+
+
+With earlyglobs disabled: no threadflag means the same behavior.
+Assertions should be unknown, race should be present.
+
+  $ goblint --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs 42-no-threadflag.c
+  [Warning][Assert] Assertion "g == 0" is unknown. (42-no-threadflag.c:7:3-7:26)
+  [Warning][Assert] Assertion "g == 1" is unknown. (42-no-threadflag.c:9:3-9:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 5
+    dead: 0
+    total lines: 5
+  [Warning][Race] Memory location g (race with conf. 110): (42-no-threadflag.c:4:5-4:6)
+    write with mhp:{created={Unknown thread id}} (conf. 110)  (exp: & g) (42-no-threadflag.c:8:3-8:8)
+    read with mhp:{created={Unknown thread id}} (conf. 110)  (exp: & g) (42-no-threadflag.c:7:3-7:26)
+    read with mhp:{created={Unknown thread id}} (conf. 110)  (exp: & g) (42-no-threadflag.c:9:3-9:26)
+  [Info][Race] Memory locations race summary:
+    safe: 0
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 1
+
+
+With single-threaded more forced.
+Assertions should succeed, race should not be present.
+
+  $ goblint --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs --enable exp.single-threaded 42-no-threadflag.c
+  [Success][Assert] Assertion "g == 0" will succeed (42-no-threadflag.c:7:3-7:26)
+  [Success][Assert] Assertion "g == 1" will succeed (42-no-threadflag.c:9:3-9:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 5
+    dead: 0
+    total lines: 5
+  [Error][Unsound] Thread not spawned
+
+
+With single-threaded mode forced, but earlyglobs enabled.
+Assertions should be unknown, race should not be present.
+
+  $ goblint --set ana.activated[-] threadflag --set ana.activated[-] threadid --enable exp.earlyglobs --enable exp.single-threaded 42-no-threadflag.c
+  [Warning][Assert] Assertion "g == 0" is unknown. (42-no-threadflag.c:7:3-7:26)
+  [Warning][Assert] Assertion "g == 1" is unknown. (42-no-threadflag.c:9:3-9:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 5
+    dead: 0
+    total lines: 5
+  [Error][Unsound] Thread not spawned
+
diff --git a/tests/regression/00-sanity/43-no-threadflag-single-threaded.c b/tests/regression/00-sanity/43-no-threadflag-single-threaded.c
deleted file mode 100644
index 059e78a971..0000000000
--- a/tests/regression/00-sanity/43-no-threadflag-single-threaded.c
+++ /dev/null
@@ -1,12 +0,0 @@
-// PARAM: --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs --enable exp.single-threaded
-// Like 00-sanity/42-no-threadflag but forced single-threaded
-#include <goblint.h>
-
-int g;
-
-int main() {
-  __goblint_check(g == 0); // SUCCESS (forced single-threaded)
-  g = 1; // NORACE (forced single-threaded)
-  __goblint_check(g == 1); // SUCCESS (forced single-threaded)
-  return 0;
-}
diff --git a/tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c b/tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c
deleted file mode 100644
index 5f0f87f41b..0000000000
--- a/tests/regression/00-sanity/44-no-threadflag-single-threaded-earlyglobs.c
+++ /dev/null
@@ -1,12 +0,0 @@
-// PARAM: --set ana.activated[-] threadflag --set ana.activated[-] threadid --enable exp.earlyglobs --enable exp.single-threaded
-// Like 00-sanity/43-no-threadflag-single-threaded but with earlyglobs enabled
-#include <goblint.h>
-
-int g;
-
-int main() {
-  __goblint_check(g == 0); // UNKNOWN (earlyglobs)
-  g = 1; // NORACE (forced single-threaded)
-  __goblint_check(g == 1); // UNKNOWN (earlyglobs)
-  return 0;
-}

From 08fbbc2efdf51f1aaff9ddb69cd20ccee5d5cce0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:29:11 +0300
Subject: [PATCH 08/14] Add test 00-sanity/43-no-escape

---
 src/analyses/threadEscape.ml                  |  2 +-
 tests/regression/00-sanity/42-no-threadflag.t |  2 +-
 tests/regression/00-sanity/43-no-escape.c     | 13 ++++++++
 tests/regression/00-sanity/43-no-escape.t     | 30 +++++++++++++++++++
 4 files changed, 45 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/00-sanity/43-no-escape.c
 create mode 100644 tests/regression/00-sanity/43-no-escape.t

diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 4fb67b6e99..0f3c6f781f 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -6,7 +6,7 @@ open Analyses
 module M = Messages
 module AD = Queries.AD
 
-let has_escaped (ask: Queries.ask) (v: varinfo): bool =
+let has_escaped (ask: Queries.ask) (v: varinfo): bool = (* TODO: use everywhere instead of query *)
   (* TODO: exp.single-threaded override *)
   assert (not v.vglob);
   if not v.vaddrof then
diff --git a/tests/regression/00-sanity/42-no-threadflag.t b/tests/regression/00-sanity/42-no-threadflag.t
index 846fc4d007..a3a3538de1 100644
--- a/tests/regression/00-sanity/42-no-threadflag.t
+++ b/tests/regression/00-sanity/42-no-threadflag.t
@@ -23,7 +23,7 @@ Assertions should be unknown, race should be present.
     total memory locations: 1
 
 
-With single-threaded more forced.
+With single-threaded mode forced.
 Assertions should succeed, race should not be present.
 
   $ goblint --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs --enable exp.single-threaded 42-no-threadflag.c
diff --git a/tests/regression/00-sanity/43-no-escape.c b/tests/regression/00-sanity/43-no-escape.c
new file mode 100644
index 0000000000..fb57998fdc
--- /dev/null
+++ b/tests/regression/00-sanity/43-no-escape.c
@@ -0,0 +1,13 @@
+// CRAM
+#include <goblint.h>
+
+
+int main() {
+  int x = 0;
+  __goblint_check(x == 0);
+  x = 1;
+  __goblint_check(x == 1);
+
+  int *p = &x; // confuse naive escape check
+  return 0;
+}
diff --git a/tests/regression/00-sanity/43-no-escape.t b/tests/regression/00-sanity/43-no-escape.t
new file mode 100644
index 0000000000..625f8c2dcb
--- /dev/null
+++ b/tests/regression/00-sanity/43-no-escape.t
@@ -0,0 +1,30 @@
+Analysis of single-threaded program with escape deactivated.
+Also earlyglobs enabled, otherwise MayEscape queries are not used.
+Earlyglobs should not matter for local variable.
+
+
+Assertions should be unknown.
+
+  $ goblint --set ana.activated[-] escape --enable exp.earlyglobs 43-no-escape.c
+  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
+  [Warning][Assert] Assertion "x == 0" is unknown. (43-no-escape.c:7:3-7:26)
+  [Warning][Assert] Assertion "x == 1" is unknown. (43-no-escape.c:9:3-9:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+
+
+With single-threaded mode forced.
+Assertions should succeed.
+
+  $ goblint --set ana.activated[-] escape --enable exp.earlyglobs --enable exp.single-threaded 43-no-escape.c
+  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
+  [Warning][Assert] Assertion "x == 0" is unknown. (43-no-escape.c:7:3-7:26)
+  [Warning][Assert] Assertion "x == 1" is unknown. (43-no-escape.c:9:3-9:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Error][Unsound] Thread not spawned
+

From 6ea1af6e4d94b85345de15dc1ac2275ba0f8d667 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:31:12 +0300
Subject: [PATCH 09/14] Use exp.single-threaded for ThreadEscape queries

---
 src/analyses/threadEscape.ml              | 3 ++-
 tests/regression/00-sanity/43-no-escape.t | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 0f3c6f781f..9712ed8abf 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -7,10 +7,11 @@ module M = Messages
 module AD = Queries.AD
 
 let has_escaped (ask: Queries.ask) (v: varinfo): bool = (* TODO: use everywhere instead of query *)
-  (* TODO: exp.single-threaded override *)
   assert (not v.vglob);
   if not v.vaddrof then
     false (* Cannot have escaped without taking address. Override provides extra precision for degenerate ask in base eval_exp used for partitioned arrays. *)
+  else if GobConfig.get_bool "exp.single-threaded" then
+    false (* Cannot have escaped if no other threads are assumed to exist. Override provides extra precision for analyzing single-threaded programs without escape analysis. *)
   else
     ask.f (Queries.MayEscape v)
 
diff --git a/tests/regression/00-sanity/43-no-escape.t b/tests/regression/00-sanity/43-no-escape.t
index 625f8c2dcb..f0f7ea31d2 100644
--- a/tests/regression/00-sanity/43-no-escape.t
+++ b/tests/regression/00-sanity/43-no-escape.t
@@ -20,8 +20,8 @@ Assertions should succeed.
 
   $ goblint --set ana.activated[-] escape --enable exp.earlyglobs --enable exp.single-threaded 43-no-escape.c
   [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
-  [Warning][Assert] Assertion "x == 0" is unknown. (43-no-escape.c:7:3-7:26)
-  [Warning][Assert] Assertion "x == 1" is unknown. (43-no-escape.c:9:3-9:26)
+  [Success][Assert] Assertion "x == 0" will succeed (43-no-escape.c:7:3-7:26)
+  [Success][Assert] Assertion "x == 1" will succeed (43-no-escape.c:9:3-9:26)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0

From 7b2a22337b0f1ccd794dd450529518dcb1a136d8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:35:19 +0300
Subject: [PATCH 10/14] Use MayEscape query via ThreadEscape.has_escaped

---
 src/analyses/mutexAnalysis.ml | 4 ++--
 src/analyses/raceAnalysis.ml  | 4 ++--
 src/analyses/threadEscape.ml  | 2 +-
 src/domains/queries.ml        | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 5875825320..ec85db7caf 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -331,10 +331,10 @@ struct
         | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound."
       in
       let module AD = Queries.AD in
-      let has_escaped g = oman.ask (Queries.MayEscape g) in
+      let oask = Analyses.ask_of_man oman in
       let on_ad ad =
         let f = function
-          | AD.Addr.Addr (g,_) when g.vglob || has_escaped g -> old_access (Some g)
+          | AD.Addr.Addr (g,_) when g.vglob || ThreadEscape.has_escaped oask g -> old_access (Some g)
           | UnknownPtr -> old_access None
           | _ -> ()
         in
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index f9aed59f2c..26a6d4ed28 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -321,7 +321,7 @@ struct
         let acc = part_access None in
         Access.add_one ~side:(side_access oman {conf; kind; node; exp; acc}) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
       in
-      let has_escaped g = oman.ask (Queries.MayEscape g) in
+      let oask = Analyses.ask_of_man oman in
       (* The following function adds accesses to the lval-set ls
          -- this is the common case if we have a sound points-to set. *)
       let on_ad ad includes_uk =
@@ -329,7 +329,7 @@ struct
         let conf = if includes_uk then conf - 10 else conf in
         let f addr =
           match addr with
-          | AD.Addr.Addr (g,o) when g.vglob || has_escaped g ->
+          | AD.Addr.Addr (g,o) when g.vglob || ThreadEscape.has_escaped oask g ->
             let coffs = ValueDomain.Offs.to_cil o in
             add_access conf (Some (g, coffs))
           | UnknownPtr -> add_access conf None
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 9712ed8abf..f81019f4e6 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -6,7 +6,7 @@ open Analyses
 module M = Messages
 module AD = Queries.AD
 
-let has_escaped (ask: Queries.ask) (v: varinfo): bool = (* TODO: use everywhere instead of query *)
+let has_escaped (ask: Queries.ask) (v: varinfo): bool =
   assert (not v.vglob);
   if not v.vaddrof then
     false (* Cannot have escaped without taking address. Override provides extra precision for degenerate ask in base eval_exp used for partitioned arrays. *)
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 448f3fd7c5..83b7964fef 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -85,7 +85,7 @@ type _ t =
   | ReachableFrom: exp -> AD.t t
   | ReachableUkTypes: exp -> TS.t t
   | Regions: exp -> LS.t t
-  | MayEscape: varinfo -> MayBool.t t
+  | MayEscape: varinfo -> MayBool.t t (** Use via {!ThreadEscape.has_escaped}. *)
   | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *)
   | MayBePublicWithout: maybepublicwithout -> MayBool.t t
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t

From 309026d8917c3eab468d0bbc2388312a8cf4d6b8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:53:13 +0300
Subject: [PATCH 11/14] Promote vars count decrease in weak-deps test

Due to 7b2a22337b0f1ccd794dd450529518dcb1a136d8, locals which have vaddrof false are not longer queried at all by mutex/race analysis.
---
 tests/regression/td3/weak-deps.t/run.t | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/regression/td3/weak-deps.t/run.t b/tests/regression/td3/weak-deps.t/run.t
index df51633e13..320de1c1a0 100644
--- a/tests/regression/td3/weak-deps.t/run.t
+++ b/tests/regression/td3/weak-deps.t/run.t
@@ -1,9 +1,9 @@
   $ goblint --set solver td3 --set solvers.td3.weak-deps none -v weak-deps.c 2>&1 | grep 'evals'
-  [Info] vars = 40    evals = 33    narrow_reuses = 0
+  [Info] vars = 34    evals = 33    narrow_reuses = 0
 
   $ goblint --set solver td3 --set solvers.td3.weak-deps eager -v weak-deps.c 2>&1 | grep 'evals'
-  [Info] vars = 40    evals = 36    narrow_reuses = 0
+  [Info] vars = 34    evals = 36    narrow_reuses = 0
 
   $ goblint --set solver td3 --set solvers.td3.weak-deps lazy -v weak-deps.c 2>&1 | grep 'evals'
-  [Info] vars = 40    evals = 32    narrow_reuses = 0
+  [Info] vars = 34    evals = 32    narrow_reuses = 0
 

From 354f523bb8957b12b1b87494085370f0ca92ee4d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 11:57:55 +0300
Subject: [PATCH 12/14] Add cram test for 02-base/32-single-thr

---
 tests/regression/02-base/32-single-thr.t | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 tests/regression/02-base/32-single-thr.t

diff --git a/tests/regression/02-base/32-single-thr.t b/tests/regression/02-base/32-single-thr.t
new file mode 100644
index 0000000000..f1205f99e4
--- /dev/null
+++ b/tests/regression/02-base/32-single-thr.t
@@ -0,0 +1,11 @@
+  $ goblint --set exp.single-threaded true 32-single-thr.c
+  [Error][Imprecise][Unsound] Function definition missing for no_spawn (32-single-thr.c:12:3-12:15)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (32-single-thr.c:12:3-12:15)
+  [Info][Imprecise] Invalidating expressions: & g, (void *)(& f) (32-single-thr.c:12:3-12:15)
+  [Warning][Deadcode] Function 'f' is uncalled: 2 LLoC (32-single-thr.c:6:1-8:1)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 2 (2 in uncalled functions)
+    total lines: 6
+  [Error][Unsound] Thread not spawned
+  [Error][Imprecise][Unsound] Function definition missing

From bb1e7aa6b294c7c6430bfe318b8f6f3336205ae8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 8 Apr 2026 12:01:53 +0300
Subject: [PATCH 13/14] Fix exp.single-threaded spawning errors

1. Don't output final message if no thread creations are even attempted by the program.
2. Output non-final message for each suppressed thread.
---
 src/analyses/mCP.ml                           | 12 +++++++-----
 tests/regression/00-sanity/42-no-threadflag.t |  2 --
 tests/regression/00-sanity/43-no-escape.t     |  1 -
 tests/regression/02-base/32-single-thr.t      |  1 +
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 1e4d91972c..1794c1d2eb 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -149,12 +149,14 @@ struct
 
   let do_spawns man (xs:(varinfo * (lval option * exp list * bool)) list) =
     let spawn_one v d =
-      List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d
+      if get_bool "exp.single-threaded" then (
+        M.msg_final Error ~category:Unsound "Thread not spawned";
+        M.error ~category:Unsound "Thread not spawned from %a" CilType.Varinfo.pretty v
+      )
+      else
+        List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d
     in
-    if get_bool "exp.single-threaded" then
-      M.msg_final Error ~category:Unsound "Thread not spawned" (* TODO: non-final error *) (* TODO: only final error if xs is non-empty *)
-    else
-      iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
+    iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 
   let do_sideg man (xs:(V.t * (WideningTokenLifter.TS.t * G.t)) list) =
     let side_one v dts =
diff --git a/tests/regression/00-sanity/42-no-threadflag.t b/tests/regression/00-sanity/42-no-threadflag.t
index a3a3538de1..c67b422c00 100644
--- a/tests/regression/00-sanity/42-no-threadflag.t
+++ b/tests/regression/00-sanity/42-no-threadflag.t
@@ -33,7 +33,6 @@ Assertions should succeed, race should not be present.
     live: 5
     dead: 0
     total lines: 5
-  [Error][Unsound] Thread not spawned
 
 
 With single-threaded mode forced, but earlyglobs enabled.
@@ -46,5 +45,4 @@ Assertions should be unknown, race should not be present.
     live: 5
     dead: 0
     total lines: 5
-  [Error][Unsound] Thread not spawned
 
diff --git a/tests/regression/00-sanity/43-no-escape.t b/tests/regression/00-sanity/43-no-escape.t
index f0f7ea31d2..7261ea19fd 100644
--- a/tests/regression/00-sanity/43-no-escape.t
+++ b/tests/regression/00-sanity/43-no-escape.t
@@ -26,5 +26,4 @@ Assertions should succeed.
     live: 7
     dead: 0
     total lines: 7
-  [Error][Unsound] Thread not spawned
 
diff --git a/tests/regression/02-base/32-single-thr.t b/tests/regression/02-base/32-single-thr.t
index f1205f99e4..ea000c0150 100644
--- a/tests/regression/02-base/32-single-thr.t
+++ b/tests/regression/02-base/32-single-thr.t
@@ -2,6 +2,7 @@
   [Error][Imprecise][Unsound] Function definition missing for no_spawn (32-single-thr.c:12:3-12:15)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (32-single-thr.c:12:3-12:15)
   [Info][Imprecise] Invalidating expressions: & g, (void *)(& f) (32-single-thr.c:12:3-12:15)
+  [Error][Unsound] Thread not spawned from f (32-single-thr.c:12:3-12:15)
   [Warning][Deadcode] Function 'f' is uncalled: 2 LLoC (32-single-thr.c:6:1-8:1)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 4

From ed80c4c53cca63cc4f7f3145d748295b02faec6f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 14 Apr 2026 00:05:52 +0300
Subject: [PATCH 14/14] Adapt disabled escape analysis warning for
 exp.single-threaded override

---
 src/maingoblint.ml                               | 2 +-
 tests/regression/00-sanity/43-no-escape.t        | 3 +--
 tests/regression/02-base/87-casts-dep-on-param.t | 2 +-
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 823b65279f..6584ac7c82 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -128,7 +128,7 @@ let check_arguments () =
   in
   let warn m = Logs.warn "%s" m in
   if get_bool "allfuns" && not (get_bool "exp.earlyglobs") then (set_bool "exp.earlyglobs" true; warn "allfuns enables exp.earlyglobs.");
-  if not @@ List.mem "escape" @@ get_string_list "ana.activated" then warn "Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!";
+  if not (get_bool "exp.single-threaded") && not @@ List.mem "escape" @@ get_string_list "ana.activated" then warn "Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global! (Except when exp.single-threaded is enabled.)";
   if List.mem "malloc_null" @@ get_string_list "ana.activated" && not @@ get_bool "sem.malloc.fail" then (set_bool "sem.malloc.fail" true; warn "The malloc_null analysis enables sem.malloc.fail.");
   if List.mem "memOutOfBounds" @@ get_string_list "ana.activated" && not @@ get_bool "cil.addNestedScopeAttr" then (set_bool "cil.addNestedScopeAttr" true; warn "The memOutOfBounds analysis enables cil.addNestedScopeAttr.");
   if get_bool "ana.base.context.int" && not (get_bool "ana.base.context.non-ptr") then (set_bool "ana.base.context.int" false; warn "ana.base.context.int implicitly disabled by ana.base.context.non-ptr");
diff --git a/tests/regression/00-sanity/43-no-escape.t b/tests/regression/00-sanity/43-no-escape.t
index 7261ea19fd..6e586ea9a9 100644
--- a/tests/regression/00-sanity/43-no-escape.t
+++ b/tests/regression/00-sanity/43-no-escape.t
@@ -6,7 +6,7 @@ Earlyglobs should not matter for local variable.
 Assertions should be unknown.
 
   $ goblint --set ana.activated[-] escape --enable exp.earlyglobs 43-no-escape.c
-  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
+  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global! (Except when exp.single-threaded is enabled.)
   [Warning][Assert] Assertion "x == 0" is unknown. (43-no-escape.c:7:3-7:26)
   [Warning][Assert] Assertion "x == 1" is unknown. (43-no-escape.c:9:3-9:26)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
@@ -19,7 +19,6 @@ With single-threaded mode forced.
 Assertions should succeed.
 
   $ goblint --set ana.activated[-] escape --enable exp.earlyglobs --enable exp.single-threaded 43-no-escape.c
-  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
   [Success][Assert] Assertion "x == 0" will succeed (43-no-escape.c:7:3-7:26)
   [Success][Assert] Assertion "x == 1" will succeed (43-no-escape.c:9:3-9:26)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
diff --git a/tests/regression/02-base/87-casts-dep-on-param.t b/tests/regression/02-base/87-casts-dep-on-param.t
index 822a10a116..afb4b37361 100644
--- a/tests/regression/02-base/87-casts-dep-on-param.t
+++ b/tests/regression/02-base/87-casts-dep-on-param.t
@@ -1,5 +1,5 @@
   $ goblint --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] 'base' --set ana.ctx_insens[+] 'mallocWrapper' --set ana.base.privatization none --enable warn.debug 87-casts-dep-on-param.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' | tee default-output.txt
-  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
+  [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global! (Except when exp.single-threaded is enabled.)
   [Info][Unsound] Unknown address in i has escaped. (87-casts-dep-on-param.c:11:3-11:11)
   [Info][Unsound] Unknown value in ? could be an escaped pointer address! (87-casts-dep-on-param.c:11:3-11:11)
   [Debug][Analyzer] Base EvalInt i query answering bot instead of {?, NULL, &(alloc@sid:$SID)} (87-casts-dep-on-param.c:13:7-13:15)