From 9a2eba1e366da7dbc297b2208402e642053fb79b Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:38 +0530
Subject: [PATCH 01/20] verify: Build the counterexample checker without TSan's
 function entry and exit hooks, which overflow its shadow stack.

---
 clang/lib/Verify/CMakeLists.txt | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/clang/lib/Verify/CMakeLists.txt b/clang/lib/Verify/CMakeLists.txt
index 52c508585a..e1b59ee8f4 100644
--- a/clang/lib/Verify/CMakeLists.txt
+++ b/clang/lib/Verify/CMakeLists.txt
@@ -114,6 +114,16 @@ if(CPPVERIFY_SANITIZER)
   endif()
 endif()
 
+# ThreadSanitizer records each instrumented call on a shadow stack of 64 Ki
+# frames that it does not bound. The counterexample checker nests up to
+# CertifyLimits::Frames (50000) evaluations, several frames each, and
+# overflowed it into the runtime's own memory. Its accesses stay checked;
+# only its frames are missing from reported stacks.
+if(_cppverify_sanitizers MATCHES "thread" OR LLVM_USE_SANITIZER MATCHES "Thread")
+  set_source_files_properties(Backend/Certify.cpp PROPERTIES
+    COMPILE_OPTIONS -fno-sanitize-thread-func-entry-exit)
+endif()
+
 target_include_directories(clangVerify PUBLIC
   ${CMAKE_CURRENT_SOURCE_DIR}
   ${CMAKE_CURRENT_SOURCE_DIR}/Driver

From 8f73c3d5f29855a7c8fde53a1e67fbdad7ae3b4d Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:39 +0530
Subject: [PATCH 02/20] verify: Stop a TSan build of cpp-verify before a
 nesting overflows TSan's shadow stack.

---
 clang/tools/cpp-verify/ShadowStackGuard.cpp | 38 +++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 clang/tools/cpp-verify/ShadowStackGuard.cpp

diff --git a/clang/tools/cpp-verify/ShadowStackGuard.cpp b/clang/tools/cpp-verify/ShadowStackGuard.cpp
new file mode 100644
index 0000000000..fe0df2b08a
--- /dev/null
+++ b/clang/tools/cpp-verify/ShadowStackGuard.cpp
@@ -0,0 +1,38 @@
+// ThreadSanitizer builds only, without instrumentation, linked with
+// --wrap=__tsan_func_entry,--wrap=__tsan_func_exit. TSan records each
+// thread's calls on a shadow stack of 64 Ki frames that it does not bound, so
+// a deeper nesting overwrites the runtime's own memory, and the run crashes
+// or hangs at random later. This stops it at the limit with its stack.
+
+#include <cstdio>
+#include <sanitizer/common_interface_defs.h>
+#include <unistd.h>
+
+extern "C" void __real___tsan_func_entry(void *CallerPC);
+extern "C" void __real___tsan_func_exit();
+
+namespace {
+thread_local unsigned long Depth;
+// Interceptors push a frame too.
+constexpr unsigned long MaxDepth = 64 * 1024 - 64;
+} // namespace
+
+extern "C" void __wrap___tsan_func_entry(void *CallerPC) {
+  if (++Depth == MaxDepth) {
+    char Message[160];
+    int Length = std::snprintf(
+        Message, sizeof Message,
+        "cpp-verify: ThreadSanitizer shadow stack full: %lu nested calls\n",
+        Depth);
+    if (write(STDERR_FILENO, Message, Length) < 0)
+      _exit(1);
+    __sanitizer_print_stack_trace();
+    _exit(1);
+  }
+  __real___tsan_func_entry(CallerPC);
+}
+
+extern "C" void __wrap___tsan_func_exit() {
+  --Depth;
+  __real___tsan_func_exit();
+}

From c3a749376a7885e28422f1f3fa0e02f6dd96ae68 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:40 +0530
Subject: [PATCH 03/20] verify: Link the shadow stack guard into
 ThreadSanitizer builds of cpp-verify.

---
 clang/tools/cpp-verify/CMakeLists.txt | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/clang/tools/cpp-verify/CMakeLists.txt b/clang/tools/cpp-verify/CMakeLists.txt
index 71a6084f23..77eaf67648 100644
--- a/clang/tools/cpp-verify/CMakeLists.txt
+++ b/clang/tools/cpp-verify/CMakeLists.txt
@@ -12,8 +12,20 @@ if(_cppverify_sanitize_flags)
   set(_cppverify_pch_reuse DISABLE_PCH_REUSE)
 endif()
 
+# Under ThreadSanitizer, a nesting deeper than its shadow stack holds stops
+# the run with its stack instead of corrupting the runtime.
+set(LLVM_OPTIONAL_SOURCES ShadowStackGuard.cpp)
+set(_cppverify_shadow_stack_guard)
+if((_cppverify_sanitize_flags MATCHES "thread" OR
+    LLVM_USE_SANITIZER MATCHES "Thread") AND NOT APPLE)
+  set(_cppverify_shadow_stack_guard ShadowStackGuard.cpp)
+  set_source_files_properties(ShadowStackGuard.cpp PROPERTIES
+    COMPILE_OPTIONS -fno-sanitize=thread SKIP_PRECOMPILE_HEADERS ON)
+endif()
+
 add_clang_tool(cpp-verify
   Main.cpp
+  ${_cppverify_shadow_stack_guard}
   ${_cppverify_pch_reuse}
   )
 
@@ -32,4 +44,9 @@ endif()
 if(_cppverify_sanitize_flags)
   target_compile_options(cpp-verify PRIVATE ${_cppverify_sanitize_flags})
   target_link_options(cpp-verify PRIVATE ${_cppverify_sanitize_flags})
+endif()
+
+if(_cppverify_shadow_stack_guard)
+  target_link_options(cpp-verify PRIVATE
+    -Wl,--wrap=__tsan_func_entry,--wrap=__tsan_func_exit)
 endif()
\ No newline at end of file

From 123f65501979c53b65237f95644337821d90a68c Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:40 +0530
Subject: [PATCH 04/20] verify: Build the vendored Z3 with ThreadSanitizer when
 LLVM is.

---
 clang/cmake/modules/CppVerifyZ3.cmake | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/clang/cmake/modules/CppVerifyZ3.cmake b/clang/cmake/modules/CppVerifyZ3.cmake
index d0c3b5c787..867db20288 100644
--- a/clang/cmake/modules/CppVerifyZ3.cmake
+++ b/clang/cmake/modules/CppVerifyZ3.cmake
@@ -74,6 +74,18 @@ function(cppverify_z3_build_external)
       list(APPEND _forward "-D${_var}:STRING=${_value}")
     endif()
   endforeach()
+  # Under ThreadSanitizer Z3 is instrumented too, so that its accesses are
+  # checked and its synchronization is seen.
+  if(LLVM_USE_SANITIZER MATCHES "Thread")
+    set(_z3_tsan "-fsanitize=thread -fno-omit-frame-pointer")
+    if(CMAKE_CXX_COMPILER_ID MATCHES "Clang")
+      string(APPEND _z3_tsan " -gline-tables-only")
+    endif()
+    list(APPEND _forward
+      "-DCMAKE_C_FLAGS:STRING=${_z3_tsan}"
+      "-DCMAKE_CXX_FLAGS:STRING=${_z3_tsan}"
+      "-DCMAKE_EXE_LINKER_FLAGS:STRING=-fsanitize=thread")
+  endif()
 
   ExternalProject_Add(cppverify_z3_ep
     ${_src_args}

From 7fd9d4558b6ae9a735261750d0d73d08749dbf76 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:41 +0530
Subject: [PATCH 05/20] ci: Suppress the ThreadSanitizer reports inside Z3 and
 LLVM's crash handler.

---
 .github/workflows/cppverify-tsan.supp | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 .github/workflows/cppverify-tsan.supp

diff --git a/.github/workflows/cppverify-tsan.supp b/.github/workflows/cppverify-tsan.supp
new file mode 100644
index 0000000000..96c5599849
--- /dev/null
+++ b/.github/workflows/cppverify-tsan.supp
@@ -0,0 +1,23 @@
+# ThreadSanitizer suppressions for cppverify-sanitize.sh in thread mode: data
+# races inside Z3 4.13.4 itself, and LLVM's crash handler. Each names a
+# function of Z3 or LLVM that the verifier does not call itself.
+#
+# Every Z3 command context, which pattern inference makes for each quantified
+# query, sets the global verbose stream (util.cpp) without a lock.
+race:set_verbose_stream
+# Z3's statistics read its global allocation counters without the lock its
+# allocator updates them under (memory_manager.cpp).
+race:get_memory_statistics
+# A check's timeout handler sets its flag from Z3's timer thread without
+# synchronization, and Z3_interrupt, which may be called from any thread,
+# reads it (cancel_eh.h).
+race:cancel_eh
+# A nested Z3 timer locks the timer pool's mutex while the outer timer holds
+# its state's mutex, and the pool hands a free state to a new timer by
+# locking the state's mutex under its own. A state is free only once its
+# timer has released it, so the two orders never meet; TSan relates the
+# recycled states (scoped_timer.cpp).
+deadlock:scoped_timer
+# LLVM prints a backtrace after a fatal signal, which is not
+# async-signal-safe; only crash_report_url.cpp crashes on purpose.
+signal:PrintStackTraceSignalHandler

From a1900ba2c7e913802e216c4b3aa90c9b217f39d9 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:42 +0530
Subject: [PATCH 06/20] ci: Sweep in an address or a thread mode over the
 programs lit runs, and report programs without a result.

---
 .github/workflows/cppverify-sanitize.sh | 71 ++++++++++++++++++-------
 1 file changed, 52 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/cppverify-sanitize.sh b/.github/workflows/cppverify-sanitize.sh
index 449e1c2222..e949ee0d78 100755
--- a/.github/workflows/cppverify-sanitize.sh
+++ b/.github/workflows/cppverify-sanitize.sh
@@ -1,34 +1,67 @@
 #!/bin/bash
-# Runs every Verify test program through a cpp-verify built with
-# -DCPPVERIFY_SANITIZER="address;undefined" and fails when a sanitizer reports
-# anything. Verdicts are not compared: the sanitizers slow the verifier, and
-# lit checks verdicts.
+# Runs every Verify test program that lit runs through a sanitized cpp-verify
+# and fails when a sanitizer reports anything. Verdicts are not compared: the
+# sanitizers slow the verifier, and lit checks verdicts.
 #
-# usage: cppverify-sanitize.sh BUILD_DIR [PARALLEL]
+# usage: cppverify-sanitize.sh BUILD_DIR address|thread [PARALLEL]
 #
-# LLVM's allocators poison memory in the instrumented code's copies of their
-# inline functions, which the uninstrumented libraries then use, so poisoning
-# by hand is off; threads get 1 GiB stacks, since instrumented frames are many
-# times larger and the counterexample checker recurses deeply. Each program
-# runs with two jobs, so the pool runs under the sanitizers too.
+# address: a build with -DCPPVERIFY_SANITIZER="address;undefined". LLVM's
+# allocators poison memory in the instrumented code's copies of their inline
+# functions, which the uninstrumented libraries then use, so poisoning by
+# hand is off. Each program runs with two jobs, so the pool runs under the
+# sanitizers too.
+#
+# thread: a build with -DLLVM_USE_SANITIZER=Thread, which instruments LLVM,
+# Clang, the verifier, and the vendored Z3. Each program runs with four jobs
+# and a proof cache of its own, and a program whose tests race Z3 against
+# cvc5 runs on the race backend, so the pool, the cache, and the races run
+# concurrently. cppverify-tsan.supp lists the reports inside Z3 itself and
+# LLVM's crash handler.
+#
+# Threads get 1 GiB stacks, since instrumented frames are larger and the
+# counterexample checker recurses deeply.
 set -u
 BUILD=$1
-PARALLEL=${2:-$(nproc)}
+MODE=$2
+PARALLEL=${3:-$(nproc)}
 HERE=$(cd "$(dirname "$0")" && pwd)
 ROOT=$(cd "$HERE/../.." && pwd)
 TESTS=$ROOT/clang/test/Verify
 OUT=$(mktemp -d)
-export OUT TESTS
+export OUT TESTS MODE
 export CPPVERIFY=$BUILD/bin/cpp-verify
 export ASAN_OPTIONS=detect_leaks=0:allow_user_poisoning=0
 export UBSAN_OPTIONS=print_stacktrace=1
+export TSAN_OPTIONS="suppressions=$HERE/cppverify-tsan.supp second_deadlock_stack=1"
 ulimit -s 1048576
 
+# A runtime that hangs reports nothing, so a program without a result
+# within the time limit is reported too.
+case $MODE in
+  address) REPORT='ERROR: AddressSanitizer|runtime error:' ;;
+  thread) REPORT='WARNING: ThreadSanitizer|ERROR: ThreadSanitizer|ThreadSanitizer shadow stack' ;;
+  *) echo "unknown mode $MODE" >&2; exit 2 ;;
+esac
+REPORT="$REPORT|cppverify-sanitize: no result"
+
 run() {
-  local file=$1 name
+  local file=$1 name extra=()
   name=$(echo "${file#$TESTS/}" | tr / _)
-  timeout -k 60 900 "$CPPVERIFY" --timeout=5000 --jobs=2 "$file" -- \
+  grep -q '^// UNSUPPORTED: true' "$file" && return 0
+  if [ "$MODE" = thread ]; then
+    extra=(--jobs=4 "--proof-cache=$OUT/cache-$name")
+    if grep -q -E -- '--backend[= ]race' "$file" && command -v cvc5 > /dev/null; then
+      extra+=(--backend=race)
+    fi
+  else
+    extra=(--jobs=2)
+  fi
+  timeout -k 60 900 "$CPPVERIFY" --timeout=5000 "${extra[@]}" "$file" -- \
     "-I$TESTS/suite/Inputs" > "$OUT/$name.txt" 2>&1
+  local status=$?
+  if [ $status -eq 124 ] || [ $status -eq 137 ]; then
+    echo "cppverify-sanitize: no result within 900 s (status $status)" >> "$OUT/$name.txt"
+  fi
   return 0
 }
 export -f run
@@ -36,16 +69,16 @@ export -f run
 find "$TESTS" -name '*.cpp' -not -path '*/Inputs/*' -print0 |
   xargs -0 -P "$PARALLEL" -I{} bash -c 'run "$1"' _ {}
 
-reports=$(grep -l -E 'ERROR: AddressSanitizer|runtime error:' "$OUT"/*.txt)
-programs=$(find "$TESTS" -name '*.cpp' -not -path '*/Inputs/*' | wc -l)
+reports=$(grep -l -E "$REPORT" "$OUT"/*.txt)
+programs=$(find "$TESTS" -name '*.cpp' -not -path '*/Inputs/*' -exec grep -L '^// UNSUPPORTED: true' {} + | wc -l)
 if [ -z "$reports" ]; then
-  echo "no reports in $programs programs"
+  echo "$MODE: no reports in $programs programs"
   exit 0
 fi
 for report in $reports; do
   echo "=== $(basename "$report" .txt)"
-  grep -m1 -A40 -E 'ERROR: AddressSanitizer|runtime error:' "$report"
+  grep -m1 -A40 -E "$REPORT" "$report"
 done
-echo "reports in $(echo "$reports" | wc -l) of $programs programs"
+echo "$MODE: reports in $(echo "$reports" | wc -l) of $programs programs"
 mkdir -p sanitizer-reports && cp $reports sanitizer-reports/
 exit 1

From cb8598839e362e708a690d6048adcd94addde921 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:42 +0530
Subject: [PATCH 07/20] ci: Run every test program under ThreadSanitizer every
 night.

---
 .github/workflows/cppverify-sanitizers.yml | 81 ++++++++++++++++++++--
 1 file changed, 77 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/cppverify-sanitizers.yml b/.github/workflows/cppverify-sanitizers.yml
index 99726bc088..3b34cbc437 100644
--- a/.github/workflows/cppverify-sanitizers.yml
+++ b/.github/workflows/cppverify-sanitizers.yml
@@ -3,9 +3,10 @@ name: CppVerify sanitizers
 # Every night, the verifier's own code (clang/lib/Verify and cpp-verify) is
 # built with AddressSanitizer and UndefinedBehaviorSanitizer
 # (-DCPPVERIFY_SANITIZER), beside an uninstrumented LLVM, Clang, and Z3, and
-# every Verify test program runs through it (cppverify-sanitize.sh). A
-# sanitizer report fails the job and uploads the outputs. A pull request that
-# changes this setup runs it too.
+# LLVM, Clang, the verifier, and Z3 together with ThreadSanitizer
+# (-DLLVM_USE_SANITIZER=Thread); every Verify test program runs through each
+# (cppverify-sanitize.sh). A sanitizer report fails the job and uploads the
+# outputs. A pull request that changes this setup runs it too.
 
 on:
   schedule:
@@ -15,6 +16,8 @@ on:
     paths:
       - .github/workflows/cppverify-sanitizers.yml
       - .github/workflows/cppverify-sanitize.sh
+      - .github/workflows/cppverify-tsan.supp
+      - clang/tools/cpp-verify/ShadowStackGuard.cpp
   workflow_dispatch:
 
 permissions:
@@ -81,10 +84,80 @@ jobs:
       - name: Run every test program
         run: |
           build/bin/cpp-verify --version
-          .github/workflows/cppverify-sanitize.sh build
+          .github/workflows/cppverify-sanitize.sh build address
 
       - uses: actions/upload-artifact@v4
         if: failure()
         with:
           name: sanitizer-reports
           path: sanitizer-reports/
+
+  tsan:
+    name: ThreadSanitizer
+    runs-on: ubuntu-24.04
+    timeout-minutes: 355
+    env:
+      CCACHE_DIR: ${{ github.workspace }}/.ccache
+      CCACHE_MAXSIZE: 4G
+      CCACHE_COMPRESS: "1"
+    steps:
+      - name: Free disk space
+        run: sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install build tools and cvc5
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ninja-build ccache clang-18 llvm-18 libclang-rt-18-dev
+          curl -sSfL -o "$RUNNER_TEMP/cvc5.zip" \
+            "https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION/cvc5-Linux-x86_64-static.zip"
+          unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5"
+          dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH"
+
+      - uses: actions/cache/restore@v4
+        with:
+          path: .ccache
+          key: ccache-linux-tsan-${{ github.sha }}
+          restore-keys: ccache-linux-tsan-
+
+      # LLVM, Clang, the verifier, and the vendored Z3 are all instrumented:
+      # TSan sees the synchronization of instrumented code only.
+      - name: Configure
+        run: |
+          cmake -S llvm -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DCMAKE_C_COMPILER=clang-18 \
+            -DCMAKE_CXX_COMPILER=clang++-18 \
+            -DLLVM_ENABLE_PROJECTS=clang \
+            -DLLVM_TARGETS_TO_BUILD=Native \
+            -DCPPVERIFY_VENDOR_Z3=ON \
+            -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF \
+            -DLLVM_ENABLE_ASSERTIONS=ON \
+            -DLLVM_USE_SANITIZER=Thread \
+            -DLLVM_CCACHE_BUILD=ON
+
+      - name: Build
+        run: ninja -C build cpp-verify
+
+      - uses: actions/cache/save@v4
+        if: always()
+        with:
+          path: .ccache
+          key: ccache-linux-tsan-${{ github.sha }}
+
+      # Two programs at once, each with four jobs; llvm-symbolizer names the
+      # frames of a report.
+      - name: Run every test program
+        run: |
+          build/bin/cpp-verify --version
+          PATH=/usr/lib/llvm-18/bin:$PATH \
+            .github/workflows/cppverify-sanitize.sh build thread 2
+
+      - uses: actions/upload-artifact@v4
+        if: failure()
+        with:
+          name: tsan-reports
+          path: sanitizer-reports/

From 247a391041850190db9c1f75ee88153a23bda66e Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:43 +0530
Subject: [PATCH 08/20] docs: Describe the ThreadSanitizer sweep and TSan's
 shadow stack in ARCHITECTURE.md.

---
 docs/ARCHITECTURE.md | 73 +++++++++++++++++++++++++++++++++++---------
 1 file changed, 58 insertions(+), 15 deletions(-)

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 9b7b0abda2..6cbfb4f67a 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -3533,21 +3533,64 @@ fresh context, the API's or `z3`'s, the same assertions are `unknown`
 - Sanitizers: `-DCPPVERIFY_SANITIZER="address;undefined"` builds
   `clangVerify` and `cpp-verify` with AddressSanitizer and
   UndefinedBehaviorSanitizer beside an uninstrumented LLVM, Clang, and Z3,
-  and `.github/workflows/cppverify-sanitize.sh` runs every Verify test
-  program through it with two jobs, failing on any report;
-  `cppverify-sanitizers.yml` does it nightly. Verdicts are not compared,
-  since the sanitizers slow the verifier. Instrumented frames are many times
-  larger, and the counterexample checker's evaluation recurses (a release
-  build passes every test program on 128 KiB threads; an instrumented one
-  needed more than 64 MiB), so the script gives threads 1 GiB stacks. The
-  first run found no report in the verifier's own code. ThreadSanitizer is
-  not run: in such a build, with only the verifier instrumented, its runtime
-  crashed in its own trace lists or hung on its own trace locks in 66 of 69
-  runs of `spec_automation.cpp` with four jobs (run under gdb to see where),
-  so a run cannot tell a race from the runtime's failure. Its reports
-  otherwise named only Z3's timer pool and LLVM's list of files to remove on
-  a signal, whose synchronization is in uninstrumented code; it needs LLVM
-  and Z3 instrumented too.
+  and `.github/workflows/cppverify-sanitize.sh BUILD address` runs every
+  Verify test program that lit runs through it with two jobs, failing on
+  any report; `cppverify-sanitizers.yml` does it nightly. Verdicts are not
+  compared, since the sanitizers slow the verifier. Instrumented frames are
+  many times larger, and the counterexample checker's evaluation recurses (a
+  release build passes every test program on 128 KiB threads; an
+  instrumented one needed more than 64 MiB), so the script gives threads
+  1 GiB stacks. The first run found no report in the verifier's own code.
+- ThreadSanitizer: `-DLLVM_USE_SANITIZER=Thread` instruments LLVM, Clang,
+  the verifier, and the vendored Z3 (`CppVerifyZ3.cmake` passes the flags to
+  Z3's own build), and `cppverify-sanitize.sh BUILD thread` runs every test
+  program that lit runs with four jobs, a proof cache of its own, and the
+  race backend for the programs whose tests race Z3 against cvc5, so the
+  pool, the cache, and the races all run concurrently; the same workflow
+  does it nightly. In either mode a program without a result within 900 s
+  fails the job too, since a runtime that hangs reports nothing.
+  `cppverify-tsan.supp` suppresses three data races and a lock order inside
+  Z3 4.13.4 and the calls LLVM's crash handler makes in a signal handler,
+  each explained there. Two things make a report trustworthy:
+  - TSan records each instrumented call on a per-thread shadow stack of
+    64 Ki frames (`kShadowStackSize`), and only a debug runtime checks the
+    bound. The counterexample checker nests up to `CertifyLimits::Frames`
+    (50000) evaluations of several frames each, so it wrote past the shadow
+    stack into the runtime's own memory, which then crashed in TSan's trace
+    lists, its deadlock detector, or its own `CHECK`s, or hung on its locks.
+    That, not the partial instrumentation or the checker's thread per check,
+    is why an earlier attempt, with only the verifier instrumented, failed
+    in 66 of 69 runs of `spec_automation.cpp` with four jobs: with the
+    checker's thread per check unchanged, 44 of 50 such runs failed, and so
+    did 45 of 50 with everything instrumented; a wrapper of
+    `__tsan_func_entry` stopped 12 of 12 such runs at 65472 nested calls,
+    all in `Backend/Certify.cpp`; and a standalone program that recurses
+    65,600 calls deep beside threads that start and stop failed in 3 of 6
+    runs, while 65,000 never did (0 of 6). Under TSan, `Backend/Certify.cpp`
+    is therefore compiled with `-fno-sanitize-thread-func-entry-exit`: its
+    accesses are still checked, only its frames are missing from the stacks
+    of reports. Then 60 of 60 runs of `spec_automation.cpp` finished with
+    either instrumentation, and 100 more of the nightly's build under gdb.
+  - `cpp-verify` links `tools/cpp-verify/ShadowStackGuard.cpp` in a TSan
+    build, uninstrumented and with
+    `--wrap=__tsan_func_entry,--wrap=__tsan_func_exit`. It counts each
+    thread's nesting and stops a run that reaches the limit
+    with `cpp-verify: ThreadSanitizer shadow stack full: N nested calls` and
+    its stack, which the script reports, so a deep recursion anywhere is
+    named rather than corrupting the runtime.
+
+  The first full run found one race in the verifier, on the source
+  manager's cache of its last lookups: the notes of a failure looked up
+  sources without `Verifier::SourceLock` (see "Verification Backends"), which
+  `suite/parallel_failure_notes.cpp` exercises. Instrumenting only the
+  verifier (`-DCPPVERIFY_SANITIZER=thread`, which the build still takes)
+  hides the synchronization in LLVM and Z3: it reported a race on LLVM's
+  list of files to remove on a signal, which the full build, seeing LLVM's
+  atomics, does not report, and it cannot see a race on a Z3 object that two
+  threads share. One sweep takes about 4800 CPU seconds,
+  most of each program's time in Z3, and a program at most 3.3 GB; only
+  `llvm_uleb128_decoder_exhaustive.cpp`, which lit does not run, needed
+  17.6 GB, more than a runner has.
 
 Every new semantic feature needs layered oracles rather than a solver result
 alone:

From 3151a07c74db08a864585f6d773dfb5da316dbd9 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:44 +0530
Subject: [PATCH 09/20] docs: Describe the ThreadSanitizer build and sweep in
 the tooling reference.

---
 website/source/language/tooling.rst | 63 ++++++++++++++++++++++++++---
 1 file changed, 58 insertions(+), 5 deletions(-)

diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index ca95e284b6..d526fbc0b8 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -1965,11 +1965,64 @@ Set ``CPPVERIFY_ENABLE_COVERAGE=ON`` on ``clangVerify`` only — not the whole L
 ``-DCPPVERIFY_SANITIZER="address;undefined"`` likewise builds only
 ``clangVerify`` and ``cpp-verify`` with the sanitizers, beside an
 uninstrumented LLVM, Clang, and Z3. ``.github/workflows/cppverify-sanitize.sh
-BUILD`` runs every Verify test program through such a build and fails on any
-sanitizer report; CI does it every night. It turns off poisoning by hand
-(``allow_user_poisoning=0``), which LLVM's allocators do in the instrumented
-code's copies of their inline functions and not in the libraries, and gives
-threads 1 GiB stacks.
+BUILD address`` runs every Verify test program that lit runs through such a
+build and fails on any sanitizer report; CI does it every night. It turns off
+poisoning by hand (``allow_user_poisoning=0``), which LLVM's allocators do in
+the instrumented code's copies of their inline functions and not in the
+libraries, and gives threads 1 GiB stacks.
+
+ThreadSanitizer needs everything instrumented, since it sees only the
+synchronization of instrumented code: ``-DLLVM_USE_SANITIZER=Thread`` builds
+LLVM, Clang, the verifier, and the vendored Z3 with it. CI does this every
+night too:
+
+.. code-block:: bash
+
+   cmake -S llvm -B build-tsan -G Ninja -DCMAKE_BUILD_TYPE=Release \
+     -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ \
+     -DLLVM_ENABLE_PROJECTS=clang -DLLVM_TARGETS_TO_BUILD=Native \
+     -DLLVM_USE_SANITIZER=Thread
+   ninja -C build-tsan cpp-verify
+   .github/workflows/cppverify-sanitize.sh build-tsan thread 2
+
+The last argument is how many programs run at once. Each runs with
+``--jobs=4`` and a proof cache of its own, and a program whose tests use the
+race backend runs on it when cvc5 is installed, so the thread pool, the cache,
+and the races between solvers run concurrently. A program uses at most about
+3 GB under ThreadSanitizer. In either mode a program that gives no result
+within 900 s is reported too (``cppverify-sanitize: no result within 900 s``),
+since a sanitizer runtime that hangs prints nothing. ``cppverify-tsan.supp`` suppresses the reports
+inside Z3 4.13.4 itself and the calls LLVM's crash handler makes in a signal
+handler, each with its reason. To look at one program, run it with the same
+options:
+
+.. code-block:: bash
+
+   TSAN_OPTIONS=suppressions=.github/workflows/cppverify-tsan.supp \
+     build-tsan/bin/cpp-verify --jobs=4 program.cpp --
+
+ThreadSanitizer keeps each thread's calls on a shadow stack of 65536 frames
+and does not check its end, so a deeper nesting overwrites the runtime's own
+memory and the run crashes or hangs later, somewhere unrelated. The
+counterexample checker nests that deep, so in a ThreadSanitizer build
+``clang/lib/Verify/Backend/Certify.cpp`` is compiled with
+``-fno-sanitize-thread-func-entry-exit``: its memory accesses are still
+checked, but its frames do not appear in reported stacks. A TSan build of
+``cpp-verify`` also counts each thread's nesting and stops at the limit with
+exit status 1, naming the recursion. Built with the checker's hooks left in,
+``suite/spec_automation.cpp`` stops so (paths shortened):
+
+.. code-block:: text
+
+   cpp-verify: ThreadSanitizer shadow stack full: 65472 nested calls
+       #0 __sanitizer_print_stack_trace <null> (cpp-verify+0x42751f)
+       #1 __wrap___tsan_func_entry clang/tools/cpp-verify/ShadowStackGuard.cpp:29:5 (cpp-verify+0x45efeb)
+       #2 getSignificantBits llvm/include/llvm/ADT/APInt.h:1557:12 (cpp-verify+0xe34cac)
+       #3 minimal clang/lib/Verify/Backend/Certify.cpp:20:41 (cpp-verify+0xe34cac)
+       #4 clang::verify::CertInt::CertInt(llvm::APInt) clang/lib/Verify/Backend/Certify.cpp:23:45 (cpp-verify+0xe34cac)
+       ...
+
+A recursion reported so is compiled the same way, or made iterative.
 
 New language features should have both semantic and structural oracles:
 

From 861935e642083f53696e6fba8a04b3b32569907e Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 15:00:44 +0530
Subject: [PATCH 10/20] docs: Add the nightly ThreadSanitizer sweep to the
 release notes.

---
 website/source/release-notes.rst | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index 1255646738..8d415a54bc 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -997,6 +997,19 @@ and every Verify test program runs through that build every night; a report
 fails the job. The first run found no memory error or undefined behavior in
 the verifier (:doc:`language/tooling`).
 
+**ThreadSanitizer every night.** LLVM, Clang, the verifier, and Z3 are also
+built with ThreadSanitizer (``-DLLVM_USE_SANITIZER=Thread``), and every Verify
+test program runs through that build with four jobs, a proof cache, and the
+race backend where its tests race Z3 against cvc5; a report fails the job. A
+TSan run used to crash or hang inside the runtime: the counterexample
+checker's evaluation nests deeper than the 65536 frames of TSan's shadow
+stack, which TSan does not check. The checker is now built without TSan's
+function entry and exit hooks, its accesses still checked, and a TSan build
+of ``cpp-verify`` stops with the offending stack if any other code nests that
+deep. The first run found one data race in the verifier, on the source
+manager's cache ("Source lookups from parallel failures" above)
+(:doc:`language/tooling`).
+
 Data formats
 ~~~~~~~~~~~~
 

From 40038b062213a5555464a25d91546a0153a9e3ed Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 16:46:43 +0530
Subject: [PATCH 11/20] docs: Say that the certifier's fresh stacks still
 exceed TSan's shadow stack in ARCHITECTURE.md.

---
 docs/ARCHITECTURE.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index bf3b117442..6edded6ce5 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -3600,6 +3600,9 @@ fresh context, the API's or `z3`'s, the same assertions are `unknown`
     accesses are still checked, only its frames are missing from the stacks
     of reports. Then 60 of 60 runs of `spec_automation.cpp` finished with
     either instrumentation, and 100 more of the nightly's build under gdb.
+    The evaluator's fresh stacks (above) do not change this: half of a
+    256 MiB stack holds more than 65536 instrumented frames, and with the
+    hooks put back, 6 of 6 runs still stopped at the limit.
   - `cpp-verify` links `tools/cpp-verify/ShadowStackGuard.cpp` in a TSan
     build, uninstrumented and with
     `--wrap=__tsan_func_entry,--wrap=__tsan_func_exit`. It counts each

From c8e77e9583e2e511bde060e4cd25d7bfb8ca04b5 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 16:46:43 +0530
Subject: [PATCH 12/20] docs: Show the shadow stack guard's output through the
 certifier's fresh stacks.

---
 website/source/language/tooling.rst | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index c0f9ba9da5..ec2bc2f87b 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -2009,7 +2009,8 @@ options:
 ThreadSanitizer keeps each thread's calls on a shadow stack of 65536 frames
 and does not check its end, so a deeper nesting overwrites the runtime's own
 memory and the run crashes or hangs later, somewhere unrelated. The
-counterexample checker nests that deep, so in a ThreadSanitizer build
+counterexample checker nests that deep before it moves to a fresh stack
+(half of 256 MiB holds more frames), so in a ThreadSanitizer build
 ``clang/lib/Verify/Backend/Certify.cpp`` is compiled with
 ``-fno-sanitize-thread-func-entry-exit``: its memory accesses are still
 checked, but its frames do not appear in reported stacks. A TSan build of
@@ -2020,11 +2021,11 @@ exit status 1, naming the recursion. Built with the checker's hooks left in,
 .. code-block:: text
 
    cpp-verify: ThreadSanitizer shadow stack full: 65472 nested calls
-       #0 __sanitizer_print_stack_trace <null> (cpp-verify+0x42751f)
-       #1 __wrap___tsan_func_entry clang/tools/cpp-verify/ShadowStackGuard.cpp:29:5 (cpp-verify+0x45efeb)
-       #2 getSignificantBits llvm/include/llvm/ADT/APInt.h:1557:12 (cpp-verify+0xe34cac)
-       #3 minimal clang/lib/Verify/Backend/Certify.cpp:20:41 (cpp-verify+0xe34cac)
-       #4 clang::verify::CertInt::CertInt(llvm::APInt) clang/lib/Verify/Backend/Certify.cpp:23:45 (cpp-verify+0xe34cac)
+       #0 __sanitizer_print_stack_trace <null> (cpp-verify+0x46276f)
+       #1 __wrap___tsan_func_entry clang/tools/cpp-verify/ShadowStackGuard.cpp:29:5 (cpp-verify+0x49a23b)
+       #2 (anonymous namespace)::Evaluator::evalNodeWithStackSpace(clang::verify::LogicExpr const*) clang/lib/Verify/Backend/Certify.cpp (cpp-verify+0xef00c2)
+       #3 (anonymous namespace)::Evaluator::eval(clang::verify::LogicExpr const*) clang/lib/Verify/Backend/Certify.cpp:3386:39 (cpp-verify+0xee83eb)
+       #4 binary clang/lib/Verify/Backend/Certify.cpp:843:38 (cpp-verify+0xef0233)
        ...
 
 A recursion reported so is compiled the same way, or made iterative.

From 83f8c7e24d9f3aa1d4efad8993eeddde9b81ab5c Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Thu, 29 Oct 2026 16:47:02 +0530
Subject: [PATCH 13/20] docs: Give the measured cost of a ThreadSanitizer sweep
 in ARCHITECTURE.md.

---
 docs/ARCHITECTURE.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 6edded6ce5..bc37699251 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -3619,8 +3619,8 @@ fresh context, the API's or `z3`'s, the same assertions are `unknown`
   hides the synchronization in LLVM and Z3: it reported a race on LLVM's
   list of files to remove on a signal, which the full build, seeing LLVM's
   atomics, does not report, and it cannot see a race on a Z3 object that two
-  threads share. One sweep takes about 4800 CPU seconds,
-  most of each program's time in Z3, and a program at most 3.3 GB; only
+  threads share. One sweep took 4300 to 4800 CPU seconds in two runs, most
+  of each program's time in Z3, and a program at most 3.3 GB; only
   `llvm_uleb128_decoder_exhaustive.cpp`, which lit does not run, needed
   17.6 GB, more than a runner has.
 

From 0fb2d65b8d023787a30db179567d527948991411 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Fri, 30 Oct 2026 01:02:35 +0530
Subject: [PATCH 14/20] cmake: Build the vendored Z3 with the configured flags
 and check its timed wait under ThreadSanitizer.

---
 clang/cmake/modules/CppVerifyZ3.cmake | 47 ++++++++++++++++++++++++---
 1 file changed, 43 insertions(+), 4 deletions(-)

diff --git a/clang/cmake/modules/CppVerifyZ3.cmake b/clang/cmake/modules/CppVerifyZ3.cmake
index 867db20288..c7e47a5838 100644
--- a/clang/cmake/modules/CppVerifyZ3.cmake
+++ b/clang/cmake/modules/CppVerifyZ3.cmake
@@ -26,6 +26,33 @@ set(CPPVERIFY_Z3_SOURCE_DIR "" CACHE PATH "Path to a Z3 source tree (overrides t
 get_filename_component(CPPVERIFY_REPO_ROOT
   "${CMAKE_CURRENT_LIST_DIR}/../../.." ABSOLUTE)
 
+# Z3's timer waits on a std::timed_mutex until a steady_clock time. Under
+# ThreadSanitizer libstdc++ 14.1 to 14.3 and 15.1 to 15.2 declare that wait
+# without the member it calls (GCC PR 121496), so Z3 would fail to compile.
+function(cppverify_z3_check_tsan_library)
+  include(CheckCXXSourceCompiles)
+  set(CMAKE_TRY_COMPILE_TARGET_TYPE STATIC_LIBRARY)
+  set(CMAKE_REQUIRED_FLAGS -fsanitize=thread)
+  check_cxx_source_compiles([[
+#include <chrono>
+#include <mutex>
+bool wait(std::timed_mutex &m) {
+  return m.try_lock_until(std::chrono::steady_clock::now());
+}
+]] CPPVERIFY_TSAN_TIMED_MUTEX_WAIT)
+  if(NOT CPPVERIFY_TSAN_TIMED_MUTEX_WAIT)
+    unset(CPPVERIFY_TSAN_TIMED_MUTEX_WAIT CACHE)
+    message(FATAL_ERROR
+      "Under ThreadSanitizer this C++ library cannot compile "
+      "std::timed_mutex::try_lock_until with a steady_clock time, which the "
+      "vendored Z3 uses: libstdc++ 14.1 to 14.3 and 15.1 to 15.2 have this "
+      "bug (GCC PR 121496), fixed in 14.4 and 15.3. Select another GCC "
+      "installation for C and C++, with Clang for example "
+      "-DCMAKE_C_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13 "
+      "-DCMAKE_CXX_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13.")
+  endif()
+endfunction()
+
 # Build vendored Z3 as an isolated ExternalProject rather than add_subdirectory.
 #
 # Why ExternalProject and not add_subdirectory: Z3's CMake declares a library
@@ -74,18 +101,30 @@ function(cppverify_z3_build_external)
       list(APPEND _forward "-D${_var}:STRING=${_value}")
     endif()
   endforeach()
+  # So are the flags it was configured with, which the cache keeps without
+  # LLVM's own: one that selects the C++ library, as --gcc-install-dir= or
+  # -stdlib= does, must reach every object linked together.
+  set(_z3_C_flags "$CACHE{CMAKE_C_FLAGS}")
+  set(_z3_CXX_flags "$CACHE{CMAKE_CXX_FLAGS}")
+  set(_z3_EXE_LINKER_flags "$CACHE{CMAKE_EXE_LINKER_FLAGS}")
   # Under ThreadSanitizer Z3 is instrumented too, so that its accesses are
   # checked and its synchronization is seen.
   if(LLVM_USE_SANITIZER MATCHES "Thread")
+    cppverify_z3_check_tsan_library()
     set(_z3_tsan "-fsanitize=thread -fno-omit-frame-pointer")
     if(CMAKE_CXX_COMPILER_ID MATCHES "Clang")
       string(APPEND _z3_tsan " -gline-tables-only")
     endif()
-    list(APPEND _forward
-      "-DCMAKE_C_FLAGS:STRING=${_z3_tsan}"
-      "-DCMAKE_CXX_FLAGS:STRING=${_z3_tsan}"
-      "-DCMAKE_EXE_LINKER_FLAGS:STRING=-fsanitize=thread")
+    string(APPEND _z3_C_flags " ${_z3_tsan}")
+    string(APPEND _z3_CXX_flags " ${_z3_tsan}")
+    string(APPEND _z3_EXE_LINKER_flags " -fsanitize=thread")
   endif()
+  foreach(_kind C CXX EXE_LINKER)
+    string(STRIP "${_z3_${_kind}_flags}" _flags)
+    if(_flags)
+      list(APPEND _forward "-DCMAKE_${_kind}_FLAGS:STRING=${_flags}")
+    endif()
+  endforeach()
 
   ExternalProject_Add(cppverify_z3_ep
     ${_src_args}

From 5e41015ad1a8d3d4ec85e3eaa1dd87374fef779d Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Fri, 30 Oct 2026 01:02:36 +0530
Subject: [PATCH 15/20] ci: Build the ThreadSanitizer job against GCC 13's
 libstdc++.

---
 .github/workflows/cppverify-sanitizers.yml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/cppverify-sanitizers.yml b/.github/workflows/cppverify-sanitizers.yml
index 3b34cbc437..097da66e42 100644
--- a/.github/workflows/cppverify-sanitizers.yml
+++ b/.github/workflows/cppverify-sanitizers.yml
@@ -17,6 +17,7 @@ on:
       - .github/workflows/cppverify-sanitizers.yml
       - .github/workflows/cppverify-sanitize.sh
       - .github/workflows/cppverify-tsan.supp
+      - clang/cmake/modules/CppVerifyZ3.cmake
       - clang/tools/cpp-verify/ShadowStackGuard.cpp
   workflow_dispatch:
 
@@ -124,13 +125,19 @@ jobs:
           restore-keys: ccache-linux-tsan-
 
       # LLVM, Clang, the verifier, and the vendored Z3 are all instrumented:
-      # TSan sees the synchronization of instrumented code only.
+      # TSan sees the synchronization of instrumented code only. Clang would
+      # take the libstdc++ of the image's newest GCC, 14.2, whose timed mutex
+      # cannot wait on a steady clock under TSan (GCC PR 121496), as Z3's
+      # timer does; GCC 13's waits with pthread_mutex_clocklock, which TSan
+      # intercepts.
       - name: Configure
         run: |
           cmake -S llvm -B build -G Ninja \
             -DCMAKE_BUILD_TYPE=Release \
             -DCMAKE_C_COMPILER=clang-18 \
             -DCMAKE_CXX_COMPILER=clang++-18 \
+            -DCMAKE_C_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13 \
+            -DCMAKE_CXX_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13 \
             -DLLVM_ENABLE_PROJECTS=clang \
             -DLLVM_TARGETS_TO_BUILD=Native \
             -DCPPVERIFY_VENDOR_Z3=ON \

From ebd5cc131505fb1b4aa1ced671b0b3ee5f4a194a Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Fri, 30 Oct 2026 01:02:37 +0530
Subject: [PATCH 16/20] docs: Explain Z3's configured flags and the libstdc++
 ThreadSanitizer bug in ARCHITECTURE.md.

---
 docs/ARCHITECTURE.md | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 6e4247558a..dd0cbcc06e 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -3612,7 +3612,21 @@ fresh context, the API's or `z3`'s, the same assertions are `unknown`
   fails the job too, since a runtime that hangs reports nothing.
   `cppverify-tsan.supp` suppresses three data races and a lock order inside
   Z3 4.13.4 and the calls LLVM's crash handler makes in a signal handler,
-  each explained there. Two things make a report trustworthy:
+  each explained there. Z3's build gets the flags the build was configured
+  with (the cache's `CMAKE_C_FLAGS`, `CMAKE_CXX_FLAGS`, and
+  `CMAKE_EXE_LINKER_FLAGS`, which hold none of LLVM's own) before TSan's,
+  so a flag that selects the C++ library reaches every object linked
+  together. Z3's timer waits on a `std::timed_mutex` until a `steady_clock`
+  time, which libstdc++ 14.1 to 14.3 and 15.1 to 15.2 cannot compile under
+  TSan (GCC PR 121496): there `_GLIBCXX_USE_PTHREAD_MUTEX_CLOCKLOCK` is 0
+  under TSan, but two of the header's tests of it ask only whether it is
+  defined, so `std::timed_mutex`'s wait calls a member it does not
+  declare. Configure
+  checks this (`CPPVERIFY_TSAN_TIMED_MUTEX_WAIT`) and says how to select
+  another GCC installation. Clang takes the newest GCC on the runner's
+  image, 14.2, so the job selects GCC 13's with `--gcc-install-dir`; its
+  wait calls `pthread_mutex_clocklock`, which LLVM 18's TSan intercepts.
+  Two things make a report trustworthy:
   - TSan records each instrumented call on a per-thread shadow stack of
     64 Ki frames (`kShadowStackSize`), and only a debug runtime checks the
     bound. The counterexample checker nests up to `CertifyLimits::Frames`

From 2c5a4bf9c1f07384f9d071e923a36908d4794104 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Fri, 30 Oct 2026 01:02:39 +0530
Subject: [PATCH 17/20] docs: Show how to select a libstdc++ that compiles Z3
 under ThreadSanitizer.

---
 website/source/language/tooling.rst | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index 5ac351dcd3..4693ade510 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -2019,6 +2019,30 @@ options:
    TSAN_OPTIONS=suppressions=.github/workflows/cppverify-tsan.supp \
      build-tsan/bin/cpp-verify --jobs=4 program.cpp --
 
+Clang compiles against the libstdc++ of the newest GCC it finds. Under
+ThreadSanitizer, that of GCC 14.1 to 14.3 and 15.1 to 15.2 (Ubuntu 24.04's
+``g++-14`` among them) cannot compile a wait on a ``std::timed_mutex`` until
+a ``steady_clock`` time, which Z3's timer makes (`GCC PR 121496
+<https://gcc.gnu.org/bugzilla/show_bug.cgi?id=121496>`_). The configure step
+checks this and stops (paths shortened):
+
+.. code-block:: text
+
+   -- Performing Test CPPVERIFY_TSAN_TIMED_MUTEX_WAIT
+   -- Performing Test CPPVERIFY_TSAN_TIMED_MUTEX_WAIT - Failed
+   CMake Error at clang/cmake/modules/CppVerifyZ3.cmake:45 (message):
+     Under ThreadSanitizer this C++ library cannot compile
+     std::timed_mutex::try_lock_until with a steady_clock time, which the
+     vendored Z3 uses: libstdc++ 14.1 to 14.3 and 15.1 to 15.2 have this bug
+     (GCC PR 121496), fixed in 14.4 and 15.3.  Select another GCC installation
+     for C and C++, with Clang for example
+     -DCMAKE_C_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13
+     -DCMAKE_CXX_FLAGS=--gcc-install-dir=/usr/lib/gcc/x86_64-linux-gnu/13.
+
+Add those two options to the ``cmake`` command above, as CI does. The vendored
+Z3 is built with the flags the build is configured with, so it compiles
+against the same library as everything it is linked with.
+
 ThreadSanitizer keeps each thread's calls on a shadow stack of 65536 frames
 and does not check its end, so a deeper nesting overwrites the runtime's own
 memory and the run crashes or hangs later, somewhere unrelated. The

From 29abfe8fe58c00313275e95f202e75428c64a9e7 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Fri, 30 Oct 2026 01:02:40 +0530
Subject: [PATCH 18/20] docs: Add a release-notes entry for Z3's configured
 flags.

---
 website/source/release-notes.rst | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index ac989478fa..da07e61db4 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -1063,6 +1063,16 @@ deep. The first run found one data race in the verifier, on the source
 manager's cache ("Source lookups from parallel failures" above)
 (:doc:`language/tooling`).
 
+**Z3 built with the configured flags.** The vendored Z3 was built with the
+build's compilers only, so a flag in ``CMAKE_CXX_FLAGS`` that selects the C++
+library, as ``--gcc-install-dir=`` does, reached LLVM and the verifier but not
+Z3, which compiled against the default one. Z3's build now gets
+``CMAKE_C_FLAGS``, ``CMAKE_CXX_FLAGS``, and ``CMAKE_EXE_LINKER_FLAGS`` as
+configured. A ThreadSanitizer build checks at configure time that the C++
+library can compile Z3's timed wait, which libstdc++ 14.1 to 14.3 and 15.1 to
+15.2 cannot under TSan (GCC PR 121496), and says how to select another
+(:doc:`language/tooling`).
+
 Data formats
 ~~~~~~~~~~~~
 

From 627eace9a36b1928edbd6129afd16e933f36b8f3 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Fri, 30 Oct 2026 01:16:12 +0530
Subject: [PATCH 19/20] docs: Give the ThreadSanitizer sweep's cost after
 merging main in ARCHITECTURE.md.

---
 docs/ARCHITECTURE.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index dd0cbcc06e..1ae2227195 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -3665,8 +3665,8 @@ fresh context, the API's or `z3`'s, the same assertions are `unknown`
   hides the synchronization in LLVM and Z3: it reported a race on LLVM's
   list of files to remove on a signal, which the full build, seeing LLVM's
   atomics, does not report, and it cannot see a race on a Z3 object that two
-  threads share. One sweep took 4300 to 4800 CPU seconds in two runs, most
-  of each program's time in Z3, and a program at most 3.3 GB; only
+  threads share. One sweep took 3900 to 4800 CPU seconds in three runs, most
+  of each program's time in Z3, and a program at most 3.5 GB; only
   `llvm_uleb128_decoder_exhaustive.cpp`, which lit does not run, needed
   17.6 GB, more than a runner has.
 

From a9cead2ceea7a0b6196ecf999fb4d7840e52b067 Mon Sep 17 00:00:00 2001
From: SwayamInSync <hawkempire007@gmail.com>
Date: Fri, 30 Oct 2026 01:16:12 +0530
Subject: [PATCH 20/20] docs: Give a ThreadSanitizer program's measured peak
 memory in the tooling reference.

---
 website/source/language/tooling.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index 4693ade510..4b73401712 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -2007,7 +2007,7 @@ The last argument is how many programs run at once. Each runs with
 ``--jobs=4`` and a proof cache of its own, and a program whose tests use the
 race backend runs on it when cvc5 is installed, so the thread pool, the cache,
 and the races between solvers run concurrently. A program uses at most about
-3 GB under ThreadSanitizer. In either mode a program that gives no result
+3.5 GB under ThreadSanitizer. In either mode a program that gives no result
 within 900 s is reported too (``cppverify-sanitize: no result within 900 s``),
 since a sanitizer runtime that hangs prints nothing. ``cppverify-tsan.supp``
 suppresses the reports inside Z3 4.13.4 itself and the calls LLVM's crash