From a5f0a113120b54bdef3109ea818e776e6f2fdccc Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 18 Jun 2026 15:24:37 +0200
Subject: [PATCH 01/10] Initial commit for yaml witnesses

---
 README.md                                    |  39 ++-
 example/README.md                            |  28 +-
 example/concurrent-data-race.i               |  30 ++
 example/concurrent-data-race.witness-2.2.yml |  65 ++++
 example/concurrent-unreach.i                 |  28 ++
 example/concurrent-unreach.witness-2.2.yml   |  73 ++++
 main.py                                      |  60 +++-
 requirements.txt                             |   1 +
 smoketest.sh                                 |  17 +
 svcomp.c                                     |  18 +-
 witness2ast.py                               | 334 +++++++++----------
 witnessparser.py                             | 239 +++++++++++++
 12 files changed, 735 insertions(+), 197 deletions(-)
 create mode 100644 example/concurrent-data-race.i
 create mode 100644 example/concurrent-data-race.witness-2.2.yml
 create mode 100644 example/concurrent-unreach.i
 create mode 100644 example/concurrent-unreach.witness-2.2.yml
 create mode 100644 witnessparser.py

diff --git a/README.md b/README.md
index c031f93e65..8f723539df 100644
--- a/README.md
+++ b/README.md
@@ -6,28 +6,55 @@
 
 # ConcurrentWitness2Test 
 
-ConcurrentWitness2Test validates violation witnesses for the ConcurrencySafety category at [SV-COMP](https://sv-comp.sosy-lab.org/).
+ConcurrentWitness2Test validates violation witnesses for the ConcurrencySafety category at [SV-COMP](https://sv-comp.sosy-lab.org/) by *executing* them: the witness is compiled into the program as source-level instrumentation that steers the schedule (and fixes nondeterministic values), and the resulting test is run repeatedly to see whether the claimed violation is reached.
+
+Both witness formats of SV-COMP are supported and detected automatically:
+
+* **GraphML** (witness format 1.0): the single non-branching path of the witness automaton is replayed; `threadId` changes along the path become schedule points.
+* **YAML** (witness format 2.0–2.2, `violation_sequence` entries): the `follow` waypoints are replayed in segment order. The format 2.2 concurrency extension is supported: the optional `thread_id` field on waypoints identifies the executing thread, and the segment order is enforced as the cross-thread (happens-before) order.
+
+Two kinds of properties are supported:
+
+* **Reachability** (`unreach-call` and similar): the violation is observed when the instrumented program calls `reach_error()`.
+* **Data races** (`no-data-race`, YAML witnesses): the program is compiled with [ThreadSanitizer](https://github.com/google/sanitizers/wiki/ThreadSanitizerCppManual) (`gcc -fsanitize=thread`) and the violation is observed when the sanitizer reports a data race. The racing pair — the two `target` waypoints of the witness' final multi-follow segment — is deliberately *not* synchronized by the instrumentation (the accesses only wait for the preceding segments), since any synchronization between them would establish a happens-before edge and hide the very race the witness claims.
 
 ## Installation
 
 Minimal necessary packages for Ubuntu 24.04 LTS:
 * python3
+* gcc (with `libtsan` for data race validation)
+
+The python dependencies in `requirements.txt` are expected in a virtualenv at `./venv` (used by `start.sh`):
+```sh
+python3 -m venv venv && ./venv/bin/pip install -r requirements.txt
+```
 
 ## Contents of the Repository
 ```
 CONTRIBUTORS.md  -- code contributors to the project
 LICENSE          -- apache 2.0 license
 README.md        -- this README
-main.py          -- main python entrypoint
+example/         -- example programs and witnesses (see example/README.md)
+main.py          -- main python entrypoint: compiles and runs the test, derives the verdict
 requirements.txt -- python dependencies (included in venv)
+smoketest.sh     -- runs the bundled examples
 start.sh         -- script to start the validation process
-svcomp.c         -- test harness
-tweaks.py        -- additional source file
-witness2ast.py   -- additional source file
+svcomp.c         -- test harness (yield/release scheduler, SV-COMP stubs)
+tweaks.py        -- AST fixes for pycparser/SV-COMP quirks
+witnessparser.py -- parses GraphML and YAML witnesses into a common step sequence
+witness2ast.py   -- applies the parsed witness to the program AST
 ```
 
 ## Usage
-Run `./start.sh <preprocessed-c-file> --witness <witnessfile> --mode <strict/normal/permissive>` to validate a violation witness. 
+Run `./start.sh <preprocessed-c-file> --witness <witnessfile> [--mode <strict/normal/permissive>] [--timeout <seconds>]` to validate a violation witness (GraphML or YAML).
+
+The instrumented test is executed up to 100 times (each run limited to `--timeout` seconds, 10 by default), and the mode decides when to stop:
+
+* `strict`: stop at the first execution that does **not** reach the violation,
+* `permissive`: stop at the first execution that **does** reach the violation,
+* `normal`: run all repetitions.
+
+The verdict summarizes the observed executions: `ALWAYS` (every execution reached the violation), `SOMETIMES`, `NEVER`, or `TIMEOUT` (no execution finished in time).
 
 ## Publications
 For more information on how the validation works, check out our SV-COMP 2023 [tool paper](https://leventebajczi.com/publications/tacas24cwt.pdf) and [slides](https://leventebajczi.com/publications/slides/tacas24cwt.pdf).
diff --git a/example/README.md b/example/README.md
index a7afc08101..ca710402d5 100644
--- a/example/README.md
+++ b/example/README.md
@@ -1,3 +1,25 @@
-example witness is incorrect (does not give value to tmp_guard, which would be relevant)
-so we can not validate it
-but we can generate the test and use the present witness infos
+# Examples
+
+Run all of them via `./smoketest.sh` from the repository root.
+
+## mix000.opt.i + mix000.opt.i.graphml (GraphML, format 1.0)
+
+The example witness is incomplete (it does not give a value to `tmp_guard`,
+which would be relevant), so the verdict is not guaranteed; in practice the
+enforced schedule reaches the violation in nearly every execution
+(`ALWAYS`/`SOMETIMES`). The smoketest only checks that the test is generated
+and runs.
+
+## concurrent-unreach.i + concurrent-unreach.witness-2.2.yml (YAML, format 2.2)
+
+Reachability (`unreach-call`) witness for a concurrent program: the writer
+thread must write `x = 1` before main reads `x`. The witness pins this order
+through its segment order (write in an earlier segment than the read), which
+the instrumentation enforces; the expected verdict is `ALWAYS`.
+
+## concurrent-data-race.i + concurrent-data-race.witness-2.2.yml (YAML, format 2.2)
+
+Data race (`no-data-race`) witness: two threads write `x` without
+synchronization. The racing pair is given as the two `target` waypoints of the
+final multi-follow segment; the test is compiled with ThreadSanitizer, which
+reports the race. The expected verdict is `ALWAYS`.
diff --git a/example/concurrent-data-race.i b/example/concurrent-data-race.i
new file mode 100644
index 0000000000..276afeb7b2
--- /dev/null
+++ b/example/concurrent-data-race.i
@@ -0,0 +1,30 @@
+// Concurrent data race: two threads write to x with no synchronization.
+// Property: G ! data-race
+// Preprocessed equivalent of the sv-witnesses concurrent-data-race.c example.
+
+typedef unsigned long int pthread_t;
+union pthread_attr_t { char __size[56]; long int __align; };
+typedef union pthread_attr_t pthread_attr_t;
+extern int pthread_create(pthread_t *__newthread, const pthread_attr_t *__attr, void *(*__start_routine)(void *), void *__arg);
+extern int pthread_join(pthread_t __th, void **__thread_return);
+
+int x = 0;
+
+void *t1_func(void *arg) {
+    x = 1;
+    return ((void *)0);
+}
+
+void *t2_func(void *arg) {
+    x = 2;
+    return ((void *)0);
+}
+
+int main(void) {
+    pthread_t ta, tb;
+    pthread_create(&ta, ((void *)0), t1_func, ((void *)0));
+    pthread_create(&tb, ((void *)0), t2_func, ((void *)0));
+    pthread_join(ta, ((void *)0));
+    pthread_join(tb, ((void *)0));
+    return 0;
+}
diff --git a/example/concurrent-data-race.witness-2.2.yml b/example/concurrent-data-race.witness-2.2.yml
new file mode 100644
index 0000000000..36b8e1863d
--- /dev/null
+++ b/example/concurrent-data-race.witness-2.2.yml
@@ -0,0 +1,65 @@
+# Violation witness (format 2.2) for example/concurrent-data-race.i using the
+# concurrency extension for the no-data-race property: the two racing
+# accesses are the two target waypoints of the final multi-follow segment.
+# Sharing one segment keeps them unordered by happens-before -- which is
+# exactly what makes them a data race.
+
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.2"
+    uuid: "c2d3e4f5-a6b7-4890-bcde-f01234567890"
+    creation_time: "2026-06-12T12:00:00Z"
+    producer:
+      name: "Handcrafted"
+      version: "1.0"
+    task:
+      input_files:
+        - "example/concurrent-data-race.i"
+      input_file_hashes:
+        "example/concurrent-data-race.i": "e3ed107653ea2609d77af560750d091c354bbca7c79c80d532b95cb2496ce26e"
+      specification: "G ! data-race"
+      data_model: "ILP32"
+      language: "C"
+  content:
+  - segment:
+    - waypoint:
+        # registers t1_func as thread 1 (1st thread-creating function_enter)
+        type: function_enter
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-data-race.i"
+          line: 25
+          column: 19
+          function: "main"
+  - segment:
+    - waypoint:
+        # registers t2_func as thread 2 (2nd thread-creating function_enter)
+        type: function_enter
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-data-race.i"
+          line: 26
+          column: 19
+          function: "main"
+  - segment:
+    # multi-follow final segment: the two conflicting accesses (both targets)
+    - waypoint:
+        type: target
+        action: follow
+        thread_id: 1
+        location:
+          file_name: "example/concurrent-data-race.i"
+          line: 14
+          column: 5
+          function: "t1_func"
+    - waypoint:
+        type: target
+        action: follow
+        thread_id: 2
+        location:
+          file_name: "example/concurrent-data-race.i"
+          line: 19
+          column: 5
+          function: "t2_func"
diff --git a/example/concurrent-unreach.i b/example/concurrent-unreach.i
new file mode 100644
index 0000000000..9e0ba6017e
--- /dev/null
+++ b/example/concurrent-unreach.i
@@ -0,0 +1,28 @@
+// Concurrent violation: the writer thread writes x=1 before main reads x,
+// so the branch on x in main is taken and reach_error is called.
+// Preprocessed equivalent of the sv-witnesses concurrent-unreach.c example.
+
+typedef unsigned long int pthread_t;
+union pthread_attr_t { char __size[56]; long int __align; };
+typedef union pthread_attr_t pthread_attr_t;
+extern int pthread_create(pthread_t *__newthread, const pthread_attr_t *__attr, void *(*__start_routine)(void *), void *__arg);
+extern int pthread_join(pthread_t __th, void **__thread_return);
+
+void reach_error() {}
+
+int x = 0;
+
+void *writer(void *arg) {
+    x = 1;
+    return ((void *)0);
+}
+
+int main(void) {
+    pthread_t t;
+    pthread_create(&t, ((void *)0), writer, ((void *)0));
+    if (x == 1) {
+        reach_error();
+    }
+    pthread_join(t, ((void *)0));
+    return 0;
+}
diff --git a/example/concurrent-unreach.witness-2.2.yml b/example/concurrent-unreach.witness-2.2.yml
new file mode 100644
index 0000000000..beef2fb42b
--- /dev/null
+++ b/example/concurrent-unreach.witness-2.2.yml
@@ -0,0 +1,73 @@
+# Violation witness (format 2.2) for example/concurrent-unreach.i using the
+# concurrency extension: waypoints carry a thread_id (0 = main thread, k =
+# thread registered by the k-th thread-creating function_enter waypoint), and
+# the segment order is the cross-thread (happens-before) order.
+
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.2"
+    uuid: "b1c2d3e4-f5a6-4789-abcd-ef0123456789"
+    creation_time: "2026-06-12T12:00:00Z"
+    producer:
+      name: "Handcrafted"
+      version: "1.0"
+    task:
+      input_files:
+        - "example/concurrent-unreach.i"
+      input_file_hashes:
+        "example/concurrent-unreach.i": "9605b865c7025954d80f25945b8d5db2d9c1212d0f43329c706c7b954f1914c9"
+      specification: "G ! call(reach_error())"
+      data_model: "ILP32"
+      language: "C"
+  content:
+  - segment:
+    - waypoint:
+        # registers writer as thread 1 (1st thread-creating function_enter)
+        type: function_enter
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-unreach.i"
+          line: 22
+          column: 19
+          function: "main"
+  - segment:
+    - waypoint:
+        # thread 1 has performed its write: at the sequence point before its
+        # `return`, x is 1. Placing this in an earlier segment than main's
+        # read orders the write happens-before the read.
+        type: assumption
+        action: follow
+        thread_id: 1
+        constraint:
+          value: "x == 1"
+          format: c_expression
+        location:
+          file_name: "example/concurrent-unreach.i"
+          line: 17
+          column: 5
+          function: "writer"
+  - segment:
+    - waypoint:
+        # main observes x == 1, so the branch `if (x == 1)` is taken
+        type: assumption
+        action: follow
+        thread_id: 0
+        constraint:
+          value: "x == 1"
+          format: c_expression
+        location:
+          file_name: "example/concurrent-unreach.i"
+          line: 23
+          column: 5
+          function: "main"
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        thread_id: 0
+        location:
+          file_name: "example/concurrent-unreach.i"
+          line: 24
+          column: 9
+          function: "main"
diff --git a/main.py b/main.py
index 75c055f0ea..d66713fa14 100644
--- a/main.py
+++ b/main.py
@@ -29,8 +29,8 @@
 from witness2ast import apply_witness
 
 
-def translate_to_c(filename, witness, mode):
-    """Simply use the c_generator module to emit a parsed AST."""
+def translate_to_c(filename, witness, mode, timeout):
+    """Apply the witness to the parsed AST, then compile and run the result."""
     try:
         ast = parse_file(filename, use_cpp=False)
     except KnownErrorVerdict as e:
@@ -42,7 +42,7 @@ def translate_to_c(filename, witness, mode):
         sys.exit(-1)
 
     try:
-        apply_witness(ast, filename, witness)
+        parsed_witness = apply_witness(ast, filename, witness)
     except KnownErrorVerdict as e:
         print("Verdict: " + e.verdict)
         sys.exit(-1)
@@ -51,6 +51,12 @@ def translate_to_c(filename, witness, mode):
         print("Verdict: Incompatible witness")
         sys.exit(-1)
 
+    # For a no-data-race witness the violation is observed by the thread
+    # sanitizer at runtime instead of a reach_error() call.
+    data_race = parsed_witness.data_race
+    if data_race:
+        print("Data race witness: compiling with ThreadSanitizer")
+
     try:
         fix_inline(ast)
         fix_struct_def(ast)
@@ -67,6 +73,10 @@ def translate_to_c(filename, witness, mode):
                     "gcc",
                     "-w",
                     "-Wno-implicit-function-declaration",
+                    "-pthread",
+                ]
+                + (["-fsanitize=thread", "-g"] if data_race else [])
+                + [
                     tmp.name,
                     os.path.dirname(__file__) + os.sep + "svcomp.c",
                     "-o",
@@ -83,17 +93,35 @@ def translate_to_c(filename, witness, mode):
             if result.returncode != 0:
                 print("Verdict: Compilation error")
                 sys.exit(-1)
+            env = os.environ.copy()
+            if data_race:
+                # Stop at the first race and reuse the reach_error() exit
+                # code, so race detection follows the same path below.
+                env["TSAN_OPTIONS"] = "halt_on_error=1 exitcode=74"
             codes = {}
             for i in range(100):
                 try:
-                    result = subprocess.run([bin_name], capture_output=True, text=True)
                     print("Execution started")
+                    result = subprocess.run(
+                        [bin_name],
+                        capture_output=True,
+                        text=True,
+                        timeout=timeout,
+                        env=env,
+                    )
                     reached_error = result.returncode == 74
                     if not reached_error and result.stdout:
                         for line in result.stdout.split("\n"):
                             if "Reached error!" in line:
                                 reached_error = True
                                 break
+                    if (
+                        not reached_error
+                        and data_race
+                        and result.stderr
+                        and "ThreadSanitizer: data race" in result.stderr
+                    ):
+                        reached_error = True
                     if result.stdout:
                         print(result.stdout)
                     if result.stderr:
@@ -190,23 +218,34 @@ def parse_arguments():
         description="Parse command line arguments for ConcurrentWitness2Test.py"
     )
 
-    parser.add_argument("--version", action="version", version="1.0")
+    parser.add_argument("--version", action="version", version="2.0")
     parser.add_argument(
         "input_file", metavar="<input.c>", type=str, help="Input file (.c)"
     )
     parser.add_argument(
         "--witness",
         "--graphml-witness",
-        metavar="<witness.graphml>",
+        "--yaml-witness",
+        metavar="<witness.graphml|witness.yml>",
         type=str,
         required=True,
-        help="Witness file (graphml)",
+        help="Witness file; GraphML (format 1.0) and YAML (format 2.x) "
+        "violation witnesses are detected automatically",
     )
     parser.add_argument(
         "--mode",
         choices=["strict", "normal", "permissive"],
         default="normal",
-        help="Mode (default: normal)",
+        help="Mode (default: normal): strict stops at the first execution "
+        "missing the error, permissive at the first one reaching it, "
+        "normal runs all repetitions",
+    )
+    parser.add_argument(
+        "--timeout",
+        metavar="<seconds>",
+        type=float,
+        default=10.0,
+        help="Timeout for a single execution of the test in seconds " "(default: 10)",
     )
 
     return parser.parse_args()
@@ -225,4 +264,7 @@ def parse_arguments():
         argparse.ArgumentParser().print_help()
         sys.exit(-1)
 
-    perform_hacks(args.input_file, lambda x: translate_to_c(x, args.witness, args.mode))
+    perform_hacks(
+        args.input_file,
+        lambda x: translate_to_c(x, args.witness, args.mode, args.timeout),
+    )
diff --git a/requirements.txt b/requirements.txt
index c386590a79..b5178a97f7 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1,2 +1,3 @@
 pycparser==2.20
 networkx==3.4.2
+PyYAML==6.0.2
diff --git a/smoketest.sh b/smoketest.sh
index 66cc746753..268c9f448d 100755
--- a/smoketest.sh
+++ b/smoketest.sh
@@ -1,2 +1,19 @@
 #!/bin/bash
+set -e
+
+check_verdict() {
+    out=$("$@")
+    echo "$out"
+    grep -q "Verdict: ALWAYS" <<< "$out"
+}
+
+# GraphML (format 1.0) witness. The bundled witness is known to be
+# incomplete (see example/README.md), so only successful test generation
+# is checked here, not the verdict.
 ./start.sh example/mix000.opt.i --witness example/mix000.opt.i.graphml --mode permissive
+
+# YAML (format 2.2) concurrent reachability witness
+check_verdict ./start.sh example/concurrent-unreach.i --witness example/concurrent-unreach.witness-2.2.yml --mode permissive
+
+# YAML (format 2.2) data race witness (requires gcc with ThreadSanitizer)
+check_verdict ./start.sh example/concurrent-data-race.i --witness example/concurrent-data-race.witness-2.2.yml --mode permissive
diff --git a/svcomp.c b/svcomp.c
index 1ac4a50750..2785042b9c 100644
--- a/svcomp.c
+++ b/svcomp.c
@@ -37,15 +37,18 @@ void reach_error() {
 atomic_int c2tt_global_counter = 0;
 mtx_t c2tt_mtx;
 cnd_t c2tt_cv;
-_Bool c2tt_init;
+once_flag c2tt_once = ONCE_FLAG_INIT;
+
+/* call_once keeps the initialization race-free: a plain initialized-flag
+ * would itself be reported as a data race by the thread sanitizer. */
+static void c2tt_initialize(void) {
+    mtx_init(&c2tt_mtx, mtx_plain);
+    cnd_init(&c2tt_cv);
+    printf("Initialized variables\n");
+}
 
 void yield(int target_value, int threadid) {
-    if(!c2tt_init) {
-        c2tt_init = 1;
-        mtx_init(&c2tt_mtx, mtx_plain);
-        cnd_init(&c2tt_cv);
-        printf("Initialized variables\n");
-    }
+    call_once(&c2tt_once, c2tt_initialize);
     mtx_lock(&c2tt_mtx);
 
     if (atomic_load(&c2tt_global_counter) >= target_value) {
@@ -64,6 +67,7 @@ void yield(int target_value, int threadid) {
 }
 
 void release(int target_value, int threadid) {
+    call_once(&c2tt_once, c2tt_initialize);
     mtx_lock(&c2tt_mtx);
     if (atomic_load(&c2tt_global_counter) > target_value) {
         mtx_unlock(&c2tt_mtx);
diff --git a/witness2ast.py b/witness2ast.py
index 62689f38fe..73ed436a6b 100644
--- a/witness2ast.py
+++ b/witness2ast.py
@@ -12,16 +12,36 @@
 WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 See the License for the specific language governing permissions and
 limitations under the License.
+
+Application of a parsed witness to the program AST.
+
+The witness (of either format, see ``witnessparser``) is reduced to a
+sequence of steps; this module turns those steps into source-level
+instrumentation:
+
+* steps carrying an ``assumption`` over a ``__VERIFIER_nondet_*()``
+  assignment replace the nondeterministic call with the assumed constant;
+* steps where the executing thread changes become *schedule points*: a
+  ``yield(slot, tid)``/``release(slot, tid)`` pair (implemented in
+  ``svcomp.c``) that blocks the thread until all earlier schedule points
+  have been passed, realizing the witness' cross-thread ordering.
+
+For a ``no-data-race`` witness the racing accesses (the ``target``
+waypoints of the final multi-follow segment) are special: they must stay
+unsynchronized, so they share a single slot and only ``yield`` on it --
+a ``release`` between them would create a happens-before edge that hides
+the race from the thread sanitizer.
 """
 
-import networkx as nx
+import re
+
 from pycparser.c_ast import (
     Compound,
     If,
     While,
     DoWhile,
     For,
-    FuncDef,
+    Return,
     FuncCall,
     NodeVisitor,
     ID,
@@ -29,51 +49,9 @@
     Constant,
     Assignment,
 )
-import re
 
 from Exceptions import KnownErrorVerdict
-
-
-def get_offset_of_line(c_file, line):
-    with open(c_file, "r") as f:
-        for i in range(1, line):
-            f.readline()
-        return f.tell()
-
-
-def get_line_of_offset(c_file, offset):
-    with open(c_file, "r") as f:
-        i = 0
-        line = ""
-        while f.tell() <= offset:
-            line = f.readline()
-            i = i + 1
-        return i, len(line) - (f.tell() - offset)
-
-
-def get_coords(c_file, startline=None, endline=None, startoffset=None, endoffset=None):
-    if not endline and startline:
-        endline = startline
-
-    if not startoffset and startline:
-        startoffset = get_offset_of_line(c_file, int(startline))
-
-    if not endoffset and endline:
-        endoffset = get_offset_of_line(c_file, int(endline) + 1)
-
-    if endoffset:
-        with open(c_file, "r") as f:
-            f.seek(int(startoffset))
-            content = f.read(int(endoffset) - int(startoffset) - 1)
-            startline, column = get_line_of_offset(c_file, int(startoffset))
-            return {
-                "startline": int(startline),
-                "column": int(column),
-                "endline": int(endline),
-                "length": int(endoffset) - int(startoffset) + 1,
-                "content": content,
-            }
-    return None
+from witnessparser import parse_witness, FORMAT_YAML
 
 
 def find_nondet_assignment_on_line(ast, target_line):
@@ -115,6 +93,33 @@ def visit_Compound(self, node):
         return None, None
 
 
+def find_last_nondet_assignment_before_line(ast, target_line, varnames):
+    """Find the last `var = __VERIFIER_nondet_*()` with var in `varnames`
+    at or before `target_line`."""
+
+    class LineVisitor(NodeVisitor):
+        def __init__(self):
+            self.statement = None
+            self.line = -1
+
+        def visit_Assignment(self, node):
+            if (
+                node.coord
+                and self.line < node.coord.line <= target_line
+                and type(node.rvalue) == FuncCall
+                and type(node.rvalue.name) == ID
+                and "__VERIFIER_nondet" in node.rvalue.name.name
+                and getattr(node.lvalue, "name", None) in varnames
+            ):
+                self.statement = node
+                self.line = node.coord.line
+            self.generic_visit(node)
+
+    line_visitor = LineVisitor()
+    line_visitor.visit(ast)
+    return line_visitor.statement
+
+
 def find_first_statement_on_line(ast, target_line):
     class LineVisitor(NodeVisitor):
         def __init__(self, target_line):
@@ -149,58 +154,6 @@ def visit_Compound(self, node):
         return None, None
 
 
-def extract_metadata(witnessfile, c_file):
-    witness = nx.read_graphml(witnessfile)
-    if witness.graph["witness-type"] != "violation_witness":
-        raise KnownErrorVerdict("Correctness witness")
-    ret = []
-
-    keys = {k for node in witness.nodes for k in witness.nodes[node].keys()}
-    entry_key = "entry" if "entry" in keys else "isEntryNode"
-    sink_key = "sink" if "sink" in keys else "isSinkNode"
-
-    entry_nodes = list(nx.get_node_attributes(witness, entry_key).keys())
-    if len(entry_nodes) == 0:
-        entry_nodes = list(
-            set([u for u, deg in witness.in_degree() if not deg])
-            - set([u for u, deg in witness.out_degree() if not deg])
-        )
-        if len(entry_nodes) == 0:
-            raise KnownErrorVerdict("No entry node")
-
-    if len(entry_nodes) > 1:
-        raise KnownErrorVerdict("Multiple entry nodes")
-
-    node = entry_nodes[0]
-
-    sink_nodes = set(nx.get_node_attributes(witness, sink_key).keys())
-
-    while len(witness.out_edges(node)) > 0:
-        out_edges = list(
-            filter(lambda x: x[1] not in sink_nodes, witness.out_edges(node))
-        )
-        if len(out_edges) > 1:
-            raise KnownErrorVerdict("Has branching")
-        edge = list(out_edges)[0]
-        attrs = witness.get_edge_data(edge[0], edge[1])
-
-        startline = attrs["startline"] if "startline" in attrs else None
-        endline = attrs["endline"] if "endline" in attrs else None
-        startoffset = attrs["startoffset"] if "startoffset" in attrs else None
-        endoffset = attrs["endoffset"] if "endoffset" in attrs else None
-
-        coords = get_coords(c_file, startline, endline, startoffset, endoffset)
-        metadata = {
-            key: attrs[key]
-            for key in ["assumption", "control", "threadId", "createThread"]
-            if key in attrs
-        }
-        ret.append((coords, metadata))
-        node = edge[1]
-
-    return ret
-
-
 nondet_return_types = {
     "__VERIFIER_nondet_bool": "_Bool",
     "__VERIFIER_nondet_char": "char",
@@ -228,84 +181,121 @@ def extract_metadata(witnessfile, c_file):
     "__VERIFIER_nondet_ushort": "unsigned short",
 }
 
+# TODO not perfect regex, but hard to solve well for everything ( e.g., assumption: !(var == 1) and variants )
+assumption_pattern = r"([^\s]*)\s*==\s*([^\s]*)"
 
-def apply_witness(ast, c_file, witnessfile):
-    funcdefs = {}
-    for node in ast.ext:
-        if isinstance(node, FuncDef):
-            funcdefs[node.decl.name] = node.body
-    metadata = extract_metadata(witnessfile, c_file)
-    threadid = metadata[0][1]["threadId"] if "threadId" in metadata[0][1] else 0
-    i = 0
-    # TODO not perfect regex, but hard to solve well for everything ( e.g., assumption: !(var == 1) and variants )
-    assumption_pattern = r"([^\s]*)\s*==\s*([^\s]*)"
-
-    for coords, data in metadata:
-        # TODO current implementation is limited: will not work if single assignment executes 1+ time (e.g., in a loop)
-        if "assumption" in data and "content" in coords and "startline" in coords:
-            nondet_assign_node, first_parent = find_nondet_assignment_on_line(
-                ast, coords["startline"]
-            )
-            if nondet_assign_node is not None:
-                assumptions = {}
-                matches = re.findall(assumption_pattern, data["assumption"])
-                for i, (varname, value) in enumerate(matches, 1):
-                    assumptions[varname] = value
-
-                varname = nondet_assign_node.lvalue.name
-                if any(varname in d for d in assumptions):
-                    # TODO change nondet call to value
-                    if nondet_assign_node.rvalue.name.name in nondet_return_types:
-                        ret_type = nondet_return_types[
-                            nondet_assign_node.rvalue.name.name
-                        ]
-                        nondet_assign_node.rvalue = Constant(
-                            type=ret_type, value=assumptions[varname]
-                        )
-        elif (
-            (data["threadId"] if "threadId" in data else threadid) != threadid
-            and coords
-            and "startline" in coords
-        ):
-            threadid = data["threadId"] if "threadId" in data else threadid
-            nondet_assign_node, first_parent = find_first_statement_on_line(
-                ast, coords["startline"]
+
+def apply_assumption(ast, line, assumption, anchored_after=False):
+    """Fix the value of a __VERIFIER_nondet_*() assignment near `line`.
+
+    If the assumption constrains the assigned variable to a constant
+    (`var == value`), the nondeterministic call is replaced by that
+    constant. Assumptions of any other shape are ignored.
+
+    The two witness formats anchor assumptions differently: a GraphML edge
+    carries the assumption on the assigning statement itself, while a YAML
+    assumption waypoint holds at the sequence point *before* its location,
+    i.e., it follows the assignment (anchored_after=True).
+    """
+    # TODO current implementation is limited: will not work if single assignment executes 1+ time (e.g., in a loop)
+    assumptions = dict(re.findall(assumption_pattern, assumption))
+    if anchored_after:
+        nondet_assign_node = find_last_nondet_assignment_before_line(
+            ast, line, set(assumptions)
+        )
+    else:
+        nondet_assign_node, _ = find_nondet_assignment_on_line(ast, line)
+    if nondet_assign_node is None:
+        return
+
+    varname = nondet_assign_node.lvalue.name
+    if varname in assumptions:
+        if nondet_assign_node.rvalue.name.name in nondet_return_types:
+            ret_type = nondet_return_types[nondet_assign_node.rvalue.name.name]
+            nondet_assign_node.rvalue = Constant(
+                type=ret_type, value=assumptions[varname]
             )
 
-            yield_func = FuncCall(
-                ID("yield"),
-                ExprList(
-                    [
-                        Constant(type="int", value=f"{i}"),
-                        Constant(type="int", value=f"{threadid}"),
-                    ]
-                ),
+
+def make_schedule_call(name, slot, threadid):
+    return FuncCall(
+        ID(name),
+        ExprList(
+            [
+                Constant(type="int", value=f"{slot}"),
+                Constant(type="int", value=f"{threadid}"),
+            ]
+        ),
+    )
+
+
+def insert_schedule_point(ast, line, slot, threadid, release=True):
+    """Instrument the statement at (or first after) `line` as a schedule point.
+
+    A yield(slot, threadid) call before the statement blocks the thread
+    until all earlier schedule points have released their slot; a
+    release(slot, threadid) call afterwards lets the next schedule point
+    proceed. For control statements the release goes to the start of the
+    body/branches (so it happens only once the statement is really being
+    executed), and for a return statement it goes before the statement
+    (code after a return would never run).
+
+    With release=False only the yield is inserted and the slot is not
+    consumed; this keeps racing accesses of a data-race witness free of
+    synchronization between one another.
+
+    Returns the slot the next schedule point should use.
+    """
+    statement, parent = find_first_statement_on_line(ast, line)
+
+    yield_func = make_schedule_call("yield", slot, threadid)
+    first_index = parent.block_items.index(statement)
+    parent.block_items.insert(first_index, yield_func)
+
+    if not release:
+        return slot
+
+    release_func = make_schedule_call("release", slot, threadid)
+    if isinstance(statement, Return):
+        parent.block_items.insert(first_index + 1, release_func)
+    elif isinstance(statement, Compound):
+        statement.block_items = [release_func] + (statement.block_items or [])
+    elif isinstance(statement, (While, DoWhile, For)):
+        statement.stmt = Compound(block_items=[release_func, statement.stmt])
+    elif isinstance(statement, If):
+        if statement.iftrue:
+            statement.iftrue = Compound(block_items=[release_func, statement.iftrue])
+        if statement.iffalse:
+            statement.iffalse = Compound(block_items=[release_func, statement.iffalse])
+    else:
+        parent.block_items.insert(first_index + 2, release_func)
+    return slot + 1
+
+
+def apply_witness(ast, c_file, witnessfile):
+    """Instrument `ast` according to the witness; returns the ParsedWitness."""
+    witness = parse_witness(witnessfile, c_file)
+    if not witness.steps:
+        raise KnownErrorVerdict("Empty witness")
+
+    first_metadata = witness.steps[0][1]
+    threadid = first_metadata["threadId"] if "threadId" in first_metadata else 0
+
+    slot = 0
+    anchored_after = witness.format == FORMAT_YAML
+    for coords, data in witness.steps:
+        usable_coords = coords and "startline" in coords
+        if "assumption" in data and usable_coords:
+            apply_assumption(
+                ast, coords["startline"], data["assumption"], anchored_after
             )
-            release_func = FuncCall(
-                ID("release"),
-                ExprList(
-                    [
-                        Constant(type="int", value=f"{i}"),
-                        Constant(type="int", value=f"{threadid}"),
-                    ]
-                ),
+
+        step_threadid = data["threadId"] if "threadId" in data else threadid
+        if step_threadid != threadid and usable_coords:
+            threadid = step_threadid
+            release = not (witness.data_race and data.get("type") == "target")
+            slot = insert_schedule_point(
+                ast, coords["startline"], slot, threadid, release
             )
 
-            i = i + 1
-            first_index = first_parent.block_items.index(nondet_assign_node)
-            first_parent.block_items.insert(first_index, yield_func)
-            if isinstance(nondet_assign_node, (Compound, While, DoWhile, For)):
-                nondet_assign_node.stmt = Compound(
-                    block_items=[release_func, nondet_assign_node.stmt]
-                )
-            elif isinstance(nondet_assign_node, If):
-                if nondet_assign_node.iftrue:
-                    nondet_assign_node.iftrue = Compound(
-                        block_items=[release_func, nondet_assign_node.iftrue]
-                    )
-                if nondet_assign_node.iffalse:
-                    nondet_assign_node.iffalse = Compound(
-                        block_items=[release_func, nondet_assign_node.iffalse]
-                    )
-            else:
-                first_parent.block_items.insert(first_index + 2, release_func)
+    return witness
diff --git a/witnessparser.py b/witnessparser.py
new file mode 100644
index 0000000000..7d31b0ec75
--- /dev/null
+++ b/witnessparser.py
@@ -0,0 +1,239 @@
+"""
+Copyright 2026 Budapest University of Technology and Economics
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+
+Format-independent parsing of violation witnesses.
+
+Two witness formats are supported:
+
+* GraphML (witness format 1.0): the witness is an automaton; the single
+  non-branching path from the entry node is read off edge by edge.
+* YAML (witness format 2.0--2.2): the witness is a ``violation_sequence``
+  of segments; the ``follow`` waypoints are read off in segment order.
+  This includes the concurrency extension of format 2.2, where waypoints
+  may carry a ``thread_id`` and a ``no-data-race`` witness ends in a
+  multi-follow segment holding the two racing ``target`` waypoints.
+
+Both parsers produce the same intermediate representation -- a
+``ParsedWitness`` whose ``steps`` are ``(coords, metadata)`` pairs in
+execution (happens-before) order -- so that the AST instrumentation in
+``witness2ast`` does not need to know which format the witness came in.
+
+``coords`` describes the source location in the C file (``startline``,
+``endline``, ``column``, ``length``, ``content``) or is ``None`` when the
+witness gives no usable location. ``metadata`` may contain:
+
+* ``assumption``: a C expression that holds at this step,
+* ``threadId``: the thread executing this step (``0`` = main thread),
+* ``type``: the waypoint type (YAML witnesses only, e.g. ``target``).
+"""
+
+import yaml
+import networkx as nx
+
+from Exceptions import KnownErrorVerdict
+
+FORMAT_GRAPHML = "graphml"
+FORMAT_YAML = "yaml"
+
+
+class ParsedWitness:
+    """A violation witness reduced to a linear sequence of steps."""
+
+    def __init__(self, steps, specification, witness_format):
+        self.steps = steps
+        self.specification = specification or ""
+        self.format = witness_format
+
+    @property
+    def data_race(self):
+        """Whether the witness claims a data race (no-data-race property)."""
+        return "data-race" in self.specification
+
+
+def get_offset_of_line(c_file, line):
+    with open(c_file, "r") as f:
+        for i in range(1, line):
+            f.readline()
+        return f.tell()
+
+
+def get_line_of_offset(c_file, offset):
+    with open(c_file, "r") as f:
+        i = 0
+        line = ""
+        while f.tell() <= offset:
+            line = f.readline()
+            i = i + 1
+        return i, len(line) - (f.tell() - offset)
+
+
+def get_coords(c_file, startline=None, endline=None, startoffset=None, endoffset=None):
+    if not endline and startline:
+        endline = startline
+
+    if not startoffset and startline:
+        startoffset = get_offset_of_line(c_file, int(startline))
+
+    if not endoffset and endline:
+        endoffset = get_offset_of_line(c_file, int(endline) + 1)
+
+    if endoffset:
+        with open(c_file, "r") as f:
+            f.seek(int(startoffset))
+            content = f.read(int(endoffset) - int(startoffset) - 1)
+            startline, column = get_line_of_offset(c_file, int(startoffset))
+            return {
+                "startline": int(startline),
+                "column": int(column),
+                "endline": int(endline),
+                "length": int(endoffset) - int(startoffset) + 1,
+                "content": content,
+            }
+    return None
+
+
+def detect_format(witnessfile):
+    """Decide whether a witness file is GraphML or YAML.
+
+    The file extension is authoritative; for unknown extensions the content
+    is sniffed (GraphML witnesses are XML documents starting with '<').
+    """
+    lower = witnessfile.lower()
+    if lower.endswith(".graphml") or lower.endswith(".xml"):
+        return FORMAT_GRAPHML
+    if lower.endswith(".yml") or lower.endswith(".yaml"):
+        return FORMAT_YAML
+    with open(witnessfile, "r") as f:
+        for line in f:
+            stripped = line.strip()
+            if stripped:
+                return FORMAT_GRAPHML if stripped.startswith("<") else FORMAT_YAML
+    raise KnownErrorVerdict("Empty witness")
+
+
+def parse_witness(witnessfile, c_file):
+    """Parse a witness of either format into a ParsedWitness."""
+    if detect_format(witnessfile) == FORMAT_GRAPHML:
+        return parse_graphml_witness(witnessfile, c_file)
+    return parse_yaml_witness(witnessfile, c_file)
+
+
+def parse_graphml_witness(witnessfile, c_file):
+    witness = nx.read_graphml(witnessfile)
+    if witness.graph["witness-type"] != "violation_witness":
+        raise KnownErrorVerdict("Correctness witness")
+    steps = []
+
+    keys = {k for node in witness.nodes for k in witness.nodes[node].keys()}
+    entry_key = "entry" if "entry" in keys else "isEntryNode"
+    sink_key = "sink" if "sink" in keys else "isSinkNode"
+
+    entry_nodes = list(nx.get_node_attributes(witness, entry_key).keys())
+    if len(entry_nodes) == 0:
+        entry_nodes = list(
+            set([u for u, deg in witness.in_degree() if not deg])
+            - set([u for u, deg in witness.out_degree() if not deg])
+        )
+        if len(entry_nodes) == 0:
+            raise KnownErrorVerdict("No entry node")
+
+    if len(entry_nodes) > 1:
+        raise KnownErrorVerdict("Multiple entry nodes")
+
+    node = entry_nodes[0]
+
+    sink_nodes = set(nx.get_node_attributes(witness, sink_key).keys())
+
+    while len(witness.out_edges(node)) > 0:
+        out_edges = list(
+            filter(lambda x: x[1] not in sink_nodes, witness.out_edges(node))
+        )
+        if len(out_edges) > 1:
+            raise KnownErrorVerdict("Has branching")
+        edge = list(out_edges)[0]
+        attrs = witness.get_edge_data(edge[0], edge[1])
+
+        startline = attrs["startline"] if "startline" in attrs else None
+        endline = attrs["endline"] if "endline" in attrs else None
+        startoffset = attrs["startoffset"] if "startoffset" in attrs else None
+        endoffset = attrs["endoffset"] if "endoffset" in attrs else None
+
+        coords = get_coords(c_file, startline, endline, startoffset, endoffset)
+        metadata = {
+            key: attrs[key]
+            for key in ["assumption", "control", "threadId", "createThread"]
+            if key in attrs
+        }
+        steps.append((coords, metadata))
+        node = edge[1]
+
+    specification = witness.graph.get("specification", "")
+    return ParsedWitness(steps, specification, FORMAT_GRAPHML)
+
+
+def parse_yaml_witness(witnessfile, c_file):
+    with open(witnessfile, "r") as f:
+        entries = yaml.safe_load(f)
+
+    if not isinstance(entries, list):
+        raise KnownErrorVerdict("Malformed witness")
+
+    sequence = None
+    for entry in entries:
+        entry_type = entry.get("entry_type") if isinstance(entry, dict) else None
+        if entry_type == "violation_sequence":
+            sequence = entry
+            break
+        if entry_type == "invariant_set":
+            raise KnownErrorVerdict("Correctness witness")
+    if sequence is None:
+        raise KnownErrorVerdict("No violation sequence")
+
+    specification = (
+        sequence.get("metadata", {}).get("task", {}).get("specification", "")
+    )
+
+    steps = []
+    for segment_entry in sequence.get("content", []):
+        for waypoint_entry in segment_entry.get("segment", []):
+            waypoint = waypoint_entry.get("waypoint", {})
+            if waypoint.get("action") != "follow":
+                # 'avoid' waypoints restrict the matching of the witness
+                # automaton; a concrete test execution cannot make use of
+                # them, so they are skipped.
+                continue
+
+            location = waypoint.get("location", {})
+            line = location.get("line")
+            coords = get_coords(c_file, startline=line) if line else None
+
+            metadata = {
+                "type": waypoint.get("type"),
+                # thread_id is the format-2.2 concurrency extension; its
+                # absence means the main thread (thread 0).
+                "threadId": int(waypoint.get("thread_id", 0)),
+            }
+
+            constraint = waypoint.get("constraint", {})
+            if (
+                waypoint.get("type") == "assumption"
+                and constraint.get("format", "c_expression") == "c_expression"
+                and constraint.get("value") is not None
+            ):
+                metadata["assumption"] = constraint["value"]
+
+            steps.append((coords, metadata))
+
+    return ParsedWitness(steps, specification, FORMAT_YAML)

From 2ecb19cab94a3dedc4f738ef3583e0b5ca4280e1 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 18 Jun 2026 15:33:56 +0200
Subject: [PATCH 02/10] packaging is now better

---
 .github/actions/create-archive/action.yml | 13 ++----------
 .gitignore                                |  4 ++++
 main.py                                   |  2 +-
 package.sh                                | 25 +++++++++++++++++++++++
 4 files changed, 32 insertions(+), 12 deletions(-)
 create mode 100755 package.sh

diff --git a/.github/actions/create-archive/action.yml b/.github/actions/create-archive/action.yml
index 25a1b2278b..2a85ac1072 100644
--- a/.github/actions/create-archive/action.yml
+++ b/.github/actions/create-archive/action.yml
@@ -9,18 +9,9 @@ runs:
       shell: bash
       run: |
         sudo apt install python3
-    - name: Create venv
+    - name: Create archive
       shell: bash
-      run: |
-        python3 -m venv --copies venv
-        source venv/bin/activate
-        pip install -r requirements.txt
-    - name: Create zip
-      shell: bash
-      run: |
-        mkdir ConcurrentWitness2Test
-        cp venv *.py *.md LICENSE requirements.txt svcomp.c *.sh example ConcurrentWitness2Test/ -r
-        zip ConcurrentWitness2Test.zip ConcurrentWitness2Test -r
+      run: ./package.sh
     - name: Upload results
       uses: actions/upload-artifact@v4
       with:
diff --git a/.gitignore b/.gitignore
index 18e308f463..bda67e8d41 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,7 @@ venv
 a.out
 .idea
 __pycache__
+build
+ConcurrentWitness2Test
+ConcurrentWitness2Test.pyz
+ConcurrentWitness2Test.zip
diff --git a/main.py b/main.py
index d66713fa14..5f8698ae5e 100644
--- a/main.py
+++ b/main.py
@@ -78,7 +78,7 @@ def translate_to_c(filename, witness, mode, timeout):
                 + (["-fsanitize=thread", "-g"] if data_race else [])
                 + [
                     tmp.name,
-                    os.path.dirname(__file__) + os.sep + "svcomp.c",
+                    os.path.dirname(os.path.abspath(sys.argv[0])) + os.sep + "svcomp.c",
                     "-o",
                     bin_name,
                 ],
diff --git a/package.sh b/package.sh
new file mode 100755
index 0000000000..fe89f55c5b
--- /dev/null
+++ b/package.sh
@@ -0,0 +1,25 @@
+#!/bin/bash
+# Build ConcurrentWitness2Test.zip: a self-contained pyz bundling the
+# python sources and pure-python dependencies, plus svcomp.c, docs,
+# examples and a start.sh wrapper. Used both locally and by
+# .github/actions/create-archive.
+set -e
+scriptdir=$(cd "$(dirname "$0")" && pwd)
+cd "$scriptdir"
+
+rm -rf build ConcurrentWitness2Test ConcurrentWitness2Test.pyz ConcurrentWitness2Test.zip
+
+mkdir build
+pip install --target build -r requirements.txt
+cp *.py build/
+mv build/main.py build/__main__.py
+python3 -m zipapp build -o ConcurrentWitness2Test.pyz -p "/usr/bin/env python3"
+rm -rf build
+
+mkdir ConcurrentWitness2Test
+cp ConcurrentWitness2Test.pyz *.md LICENSE svcomp.c example ConcurrentWitness2Test/ -r
+printf '#!/bin/bash\nscriptdir=$(dirname "$0")\npython3 "$scriptdir"/ConcurrentWitness2Test.pyz "$@"\n' > ConcurrentWitness2Test/start.sh
+chmod +x ConcurrentWitness2Test/start.sh
+zip ConcurrentWitness2Test.zip ConcurrentWitness2Test -r
+
+echo "Created $scriptdir/ConcurrentWitness2Test.zip"

From 731b85fbe02737505c85fbcfa2544855bf31b6fe Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 18 Jun 2026 15:35:47 +0200
Subject: [PATCH 03/10] Packaging smoketest as well

---
 package.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/package.sh b/package.sh
index fe89f55c5b..69f8a88f8d 100755
--- a/package.sh
+++ b/package.sh
@@ -17,9 +17,9 @@ python3 -m zipapp build -o ConcurrentWitness2Test.pyz -p "/usr/bin/env python3"
 rm -rf build
 
 mkdir ConcurrentWitness2Test
-cp ConcurrentWitness2Test.pyz *.md LICENSE svcomp.c example ConcurrentWitness2Test/ -r
+cp ConcurrentWitness2Test.pyz *.md LICENSE svcomp.c example smoketest.sh ConcurrentWitness2Test/ -r
 printf '#!/bin/bash\nscriptdir=$(dirname "$0")\npython3 "$scriptdir"/ConcurrentWitness2Test.pyz "$@"\n' > ConcurrentWitness2Test/start.sh
-chmod +x ConcurrentWitness2Test/start.sh
+chmod +x ConcurrentWitness2Test/start.sh ConcurrentWitness2Test/smoketest.sh
 zip ConcurrentWitness2Test.zip ConcurrentWitness2Test -r
 
 echo "Created $scriptdir/ConcurrentWitness2Test.zip"

From c90c80364f3fe8e23f6c03aa1182ca67b62f5b35 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Fri, 19 Jun 2026 16:46:20 +0200
Subject: [PATCH 04/10] Added header include support

---
 README.md          |   3 +-
 headers/NOTICE.md  |  13 +
 headers/assert.h   |   4 +
 headers/ctype.h    |  15 +
 headers/errno.h    |   0
 headers/float.h    |   0
 headers/inttypes.h |  95 +++++++
 headers/limits.h   |   0
 headers/math.h     | 172 ++++++++++++
 headers/pthread.h  | 672 +++++++++++++++++++++++++++++++++++++++++++++
 headers/setjmp.h   |   4 +
 headers/signal.h   |   3 +
 headers/stdarg.h   |   2 +
 headers/stddef.h   |   2 +
 headers/stdint.h   |  11 +
 headers/stdio.h    |  60 ++++
 headers/stdlib.h   |  44 +++
 headers/string.h   |  31 +++
 headers/time.h     |  31 +++
 main.py            |  26 +-
 package.sh         |   2 +-
 21 files changed, 1187 insertions(+), 3 deletions(-)
 create mode 100644 headers/NOTICE.md
 create mode 100644 headers/assert.h
 create mode 100644 headers/ctype.h
 create mode 100644 headers/errno.h
 create mode 100644 headers/float.h
 create mode 100644 headers/inttypes.h
 create mode 100644 headers/limits.h
 create mode 100644 headers/math.h
 create mode 100644 headers/pthread.h
 create mode 100644 headers/setjmp.h
 create mode 100644 headers/signal.h
 create mode 100644 headers/stdarg.h
 create mode 100644 headers/stddef.h
 create mode 100644 headers/stdint.h
 create mode 100644 headers/stdio.h
 create mode 100644 headers/stdlib.h
 create mode 100644 headers/string.h
 create mode 100644 headers/time.h

diff --git a/README.md b/README.md
index 8f723539df..90679efd57 100644
--- a/README.md
+++ b/README.md
@@ -35,6 +35,7 @@ CONTRIBUTORS.md  -- code contributors to the project
 LICENSE          -- apache 2.0 license
 README.md        -- this README
 example/         -- example programs and witnesses (see example/README.md)
+headers/         -- minimal stub system headers used to preprocess input files (see headers/NOTICE.md)
 main.py          -- main python entrypoint: compiles and runs the test, derives the verdict
 requirements.txt -- python dependencies (included in venv)
 smoketest.sh     -- runs the bundled examples
@@ -46,7 +47,7 @@ witness2ast.py   -- applies the parsed witness to the program AST
 ```
 
 ## Usage
-Run `./start.sh <preprocessed-c-file> --witness <witnessfile> [--mode <strict/normal/permissive>] [--timeout <seconds>]` to validate a violation witness (GraphML or YAML).
+Run `./start.sh <c-file> --witness <witnessfile> [--mode <strict/normal/permissive>] [--timeout <seconds>]` to validate a violation witness (GraphML or YAML). The C file is preprocessed automatically (against a minimal set of stub system headers in `headers/`, since pycparser cannot handle the GNU extensions present in real glibc headers); files using system headers outside that stub set (e.g. `<stdatomic.h>`) or GCC inline assembly are not supported.
 
 The instrumented test is executed up to 100 times (each run limited to `--timeout` seconds, 10 by default), and the mode decides when to stop:
 
diff --git a/headers/NOTICE.md b/headers/NOTICE.md
new file mode 100644
index 0000000000..a61e7a4550
--- /dev/null
+++ b/headers/NOTICE.md
@@ -0,0 +1,13 @@
+These minimal stub system headers let `pycparser` parse SV-COMP benchmarks
+that still contain `#include` directives, without dragging in real glibc
+headers (which use GNU extensions pycparser's grammar doesn't support).
+
+Adapted from theta's C frontend
+(`subprojects/frontends/c-frontend/.../frontend/stdlib/*.h.kt`,
+https://github.com/ftsrg/theta), itself taken from the
+[c-std-headers](https://github.com/eliphatfs/c-std-headers) project.
+Both are licensed under the Apache License, Version 2.0 (see `../LICENSE`).
+
+Local additions on top of the theta originals (`NULL`, `intptr_t`/`uintptr_t`)
+fill gaps that theta's own frontend papers over with special-cased Java
+logic instead of a textual macro/typedef.
diff --git a/headers/assert.h b/headers/assert.h
new file mode 100644
index 0000000000..1cba3a007f
--- /dev/null
+++ b/headers/assert.h
@@ -0,0 +1,4 @@
+#define NULL ((void *)0)
+extern void abort(void);
+extern int printf(const char * format, ...);
+extern void assert(int expression);
diff --git a/headers/ctype.h b/headers/ctype.h
new file mode 100644
index 0000000000..82df1e3f8c
--- /dev/null
+++ b/headers/ctype.h
@@ -0,0 +1,15 @@
+#define NULL ((void *)0)
+extern int isalnum(int c);
+extern int isalpha(int c);
+extern int isblank(int c);
+extern int iscntrl(int c);
+extern int isdigit(int c);
+extern int isgraph(int c);
+extern int islower(int c);
+extern int isprint(int c);
+extern int ispunct(int c);
+extern int isspace(int c);
+extern int isupper(int c);
+extern int isxdigit(int c);
+extern int tolower(int c);
+extern int toupper(int c);
diff --git a/headers/errno.h b/headers/errno.h
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/headers/float.h b/headers/float.h
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/headers/inttypes.h b/headers/inttypes.h
new file mode 100644
index 0000000000..23eab2b242
--- /dev/null
+++ b/headers/inttypes.h
@@ -0,0 +1,95 @@
+#define NULL ((void *)0)
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Wpedantic"
+typedef unsigned char __u_char;
+typedef unsigned short int __u_short;
+typedef unsigned int __u_int;
+typedef unsigned long int __u_long;
+typedef signed char __int8_t;
+typedef unsigned char __uint8_t;
+typedef signed short int __int16_t;
+typedef unsigned short int __uint16_t;
+typedef signed int __int32_t;
+typedef unsigned int __uint32_t;
+typedef signed long int __int64_t;
+typedef unsigned long int __uint64_t;
+typedef __int8_t __int_least8_t;
+typedef __uint8_t __uint_least8_t;
+typedef __int16_t __int_least16_t;
+typedef __uint16_t __uint_least16_t;
+typedef __int32_t __int_least32_t;
+typedef __uint32_t __uint_least32_t;
+typedef __int64_t __int_least64_t;
+typedef __uint64_t __uint_least64_t;
+typedef long int __quad_t;
+typedef unsigned long int __u_quad_t;
+typedef long int __intmax_t;
+typedef unsigned long int __uintmax_t;
+typedef unsigned long int __dev_t;
+typedef unsigned int __uid_t;
+typedef unsigned int __gid_t;
+typedef unsigned long int __ino_t;
+typedef unsigned long int __ino64_t;
+typedef unsigned int __mode_t;
+typedef unsigned long int __nlink_t;
+typedef long int __off_t;
+typedef long int __off64_t;
+typedef int __pid_t;
+typedef struct { int __val[2]; } __fsid_t;
+typedef long int __clock_t;
+typedef unsigned long int __rlim_t;
+typedef unsigned long int __rlim64_t;
+typedef unsigned int __id_t;
+typedef long int __time_t;
+typedef unsigned int __useconds_t;
+typedef long int __suseconds_t;
+typedef long int __suseconds64_t;
+typedef int __daddr_t;
+typedef int __key_t;
+typedef int __clockid_t;
+typedef void * __timer_t;
+typedef long int __blksize_t;
+typedef long int __blkcnt_t;
+typedef long int __blkcnt64_t;
+typedef unsigned long int __fsblkcnt_t;
+typedef unsigned long int __fsblkcnt64_t;
+typedef unsigned long int __fsfilcnt_t;
+typedef unsigned long int __fsfilcnt64_t;
+typedef long int __fsword_t;
+typedef long int __ssize_t;
+typedef long int __syscall_slong_t;
+typedef unsigned long int __syscall_ulong_t;
+typedef __off64_t __loff_t;
+typedef char *__caddr_t;
+typedef long int __intptr_t;
+typedef unsigned int __socklen_t;
+typedef int __sig_atomic_t;
+typedef __int8_t int8_t;
+typedef __int16_t int16_t;
+typedef __int32_t int32_t;
+typedef __int64_t int64_t;
+typedef __uint8_t uint8_t;
+typedef __uint16_t uint16_t;
+typedef __uint32_t uint32_t;
+typedef __uint64_t uint64_t;
+typedef __int_least8_t int_least8_t;
+typedef __int_least16_t int_least16_t;
+typedef __int_least32_t int_least32_t;
+typedef __int_least64_t int_least64_t;
+typedef __uint_least8_t uint_least8_t;
+typedef __uint_least16_t uint_least16_t;
+typedef __uint_least32_t uint_least32_t;
+typedef __uint_least64_t uint_least64_t;
+typedef signed char int_fast8_t;
+typedef long int int_fast16_t;
+typedef long int int_fast32_t;
+typedef long int int_fast64_t;
+typedef unsigned char uint_fast8_t;
+typedef unsigned long int uint_fast16_t;
+typedef unsigned long int uint_fast32_t;
+typedef unsigned long int uint_fast64_t;
+typedef long int intptr_t;
+typedef unsigned long int uintptr_t;
+typedef __intmax_t intmax_t;
+typedef __uintmax_t uintmax_t;
+#pragma GCC diagnostic pop
diff --git a/headers/limits.h b/headers/limits.h
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/headers/math.h b/headers/math.h
new file mode 100644
index 0000000000..ec745e275b
--- /dev/null
+++ b/headers/math.h
@@ -0,0 +1,172 @@
+#define NULL ((void *)0)
+extern double acos(double x);
+extern float acosf(float x);
+extern long double acosl(long double x);
+extern double asin(double x);
+extern float asinf(float x);
+extern long double asinl(long double x);
+extern double atan(double x);
+extern float atanf(float x);
+extern long double atanl(long double x);
+extern double atan2(double y, double x);
+extern float atan2f(float y, float x);
+extern long double atan2l(long double y, long double x);
+extern double cos(double x);
+extern float cosf(float x);
+extern long double cosl(long double x);
+extern double sin(double x);
+extern float sinf(float x);
+extern long double sinl(long double x);
+extern double tan(double x);
+extern float tanf(float x);
+extern long double tanl(long double x);
+extern double acosh(double x);
+extern float acoshf(float x);
+extern long double acoshl(long double x);
+extern double asinh(double x);
+extern float asinhf(float x);
+extern long double asinhl(long double x);
+extern double atanh(double x);
+extern float atanhf(float x);
+extern long double atanhl(long double x);
+extern double cosh(double x);
+extern float coshf(float x);
+extern long double coshl(long double x);
+extern double sinh(double x);
+extern float sinhf(float x);
+extern long double sinhl(long double x);
+extern double tanh(double x);
+extern float tanhf(float x);
+extern long double tanhl(long double x);
+extern double exp(double x);
+extern float expf(float x);
+extern long double expl(long double x);
+extern double exp2(double x);
+extern float exp2f(float x);
+extern long double exp2l(long double x);
+extern double expm1(double x);
+extern float expm1f(float x);
+extern long double expm1l(long double x);
+extern double frexp(double value, int *exp);
+extern float frexpf(float value, int *exp);
+extern long double frexpl(long double value, int *exp);
+extern int ilogb(double x);
+extern int ilogbf(float x);
+extern int ilogbl(long double x);
+extern double ldexp(double x, int exp);
+extern float ldexpf(float x, int exp);
+extern long double ldexpl(long double x, int exp);
+extern double log(double x);
+extern float logf(float x);
+extern long double logl(long double x);
+extern double log10(double x);
+extern float log10f(float x);
+extern long double log10l(long double x);
+extern double log1p(double x);
+extern float log1pf(float x);
+extern long double log1pl(long double x);
+extern double log2(double x);
+extern float log2f(float x);
+extern long double log2l(long double x);
+extern double logb(double x);
+extern float logbf(float x);
+extern long double logbl(long double x);
+extern double modf(double value, double *iptr);
+extern float modff(float value, float *iptr);
+extern long double modfl(long double value, long double *iptr);
+extern double scalbn(double x, int n);
+extern float scalbnf(float x, int n);
+extern long double scalbnl(long double x, int n);
+extern double scalbln(double x, long int n);
+extern float scalblnf(float x, long int n);
+extern long double scalblnl(long double x, long int n);
+extern double cbrt(double x);
+extern float cbrtf(float x);
+extern long double cbrtl(long double x);
+extern double fabs(double x);
+extern float fabsf(float x);
+extern long double fabsl(long double x);
+extern double hypot(double x, double y);
+extern float hypotf(float x, float y);
+extern long double hypotl(long double x, long double y);
+extern double pow(double x, double y);
+extern float powf(float x, float y);
+extern long double powl(long double x, long double y);
+extern double sqrt(double x);
+extern float sqrtf(float x);
+extern long double sqrtl(long double x);
+extern double erf(double x);
+extern float erff(float x);
+extern long double erfl(long double x);
+extern double erfc(double x);
+extern float erfcf(float x);
+extern long double erfcl(long double x);
+extern double lgamma(double x);
+extern float lgammaf(float x);
+extern long double lgammal(long double x);
+extern double tgamma(double x);
+extern float tgammaf(float x);
+extern long double tgammal(long double x);
+extern double ceil(double x);
+extern float ceilf(float x);
+extern long double ceill(long double x);
+extern double floor(double x);
+extern float floorf(float x);
+extern long double floorl(long double x);
+extern double nearbyint(double x);
+extern float nearbyintf(float x);
+extern long double nearbyintl(long double x);
+extern double rint(double x);
+extern float rintf(float x);
+extern long double rintl(long double x);
+extern long int lrint(double x);
+extern long int lrintf(float x);
+extern long int lrintl(long double x);
+extern long long int llrint(double x);
+extern long long int llrintf(float x);
+extern long long int llrintl(long double x);
+extern double round(double x);
+extern float roundf(float x);
+extern long double roundl(long double x);
+extern long int lround(double x);
+extern long int lroundf(float x);
+extern long int lroundl(long double x);
+extern long long int llround(double x);
+extern long long int llroundf(float x);
+extern long long int llroundl(long double x);
+extern double trunc(double x);
+extern float truncf(float x);
+extern long double truncl(long double x);
+extern double fmod(double x, double y);
+extern float fmodf(float x, float y);
+extern long double fmodl(long double x, long double y);
+extern double remainder(double x, double y);
+extern float remainderf(float x, float y);
+extern long double remainderl(long double x, long double y);
+extern double remquo(double x, double y, int *quo);
+extern float remquof(float x, float y, int *quo);
+extern long double remquol(long double x, long double y, int *quo);
+extern double copysign(double x, double y);
+extern float copysignf(float x, float y);
+extern long double copysignl(long double x, long double y);
+extern double nan(const char *tagp);
+extern float nanf(const char *tagp);
+extern long double nanl(const char *tagp);
+extern double nextafter(double x, double y);
+extern float nextafterf(float x, float y);
+extern long double nextafterl(long double x, long double y);
+extern double nexttoward(double x, long double y);
+extern float nexttowardf(float x, long double y);
+extern long double nexttowardl(long double x, long double y);
+extern double fdim(double x, double y);
+extern float fdimf(float x, float y);
+extern long double fdiml(long double x, long double y);
+extern double fmax(double x, double y);
+extern float fmaxf(float x, float y);
+extern long double fmaxl(long double x, long double y);
+extern double fmin(double x, double y);
+extern float fminf(float x, float y);
+extern long double fminl(long double x, long double y);
+extern double fma(double x, double y, double z);
+extern float fmaf(float x, float y, float z);
+extern long double fmal(long double x, long double y, long double z);
diff --git a/headers/pthread.h b/headers/pthread.h
new file mode 100644
index 0000000000..85a0173aee
--- /dev/null
+++ b/headers/pthread.h
@@ -0,0 +1,672 @@
+#define NULL ((void *)0)
+typedef unsigned char __u_char;
+typedef unsigned short int __u_short;
+typedef unsigned int __u_int;
+typedef unsigned long int __u_long;
+typedef signed char __int8_t;
+typedef unsigned char __uint8_t;
+typedef signed short int __int16_t;
+typedef unsigned short int __uint16_t;
+typedef signed int __int32_t;
+typedef unsigned int __uint32_t;
+__extension__ typedef signed long long int __int64_t;
+__extension__ typedef unsigned long long int __uint64_t;
+__extension__ typedef long long int __quad_t;
+__extension__ typedef unsigned long long int __u_quad_t;
+__extension__ typedef long long int __intmax_t;
+__extension__ typedef unsigned long long int __uintmax_t;
+__extension__ typedef __u_quad_t __dev_t;
+__extension__ typedef unsigned int __uid_t;
+__extension__ typedef unsigned int __gid_t;
+__extension__ typedef unsigned long int __ino_t;
+__extension__ typedef __u_quad_t __ino64_t;
+__extension__ typedef unsigned int __mode_t;
+__extension__ typedef unsigned int __nlink_t;
+__extension__ typedef long int __off_t;
+__extension__ typedef __quad_t __off64_t;
+__extension__ typedef int __pid_t;
+__extension__ typedef struct { int __val[2]; } __fsid_t;
+__extension__ typedef long int __clock_t;
+__extension__ typedef unsigned long int __rlim_t;
+__extension__ typedef __u_quad_t __rlim64_t;
+__extension__ typedef unsigned int __id_t;
+__extension__ typedef long int __time_t;
+__extension__ typedef unsigned int __useconds_t;
+__extension__ typedef long int __suseconds_t;
+__extension__ typedef int __daddr_t;
+__extension__ typedef int __key_t;
+__extension__ typedef int __clockid_t;
+__extension__ typedef void * __timer_t;
+__extension__ typedef long int __blksize_t;
+__extension__ typedef long int __blkcnt_t;
+__extension__ typedef __quad_t __blkcnt64_t;
+__extension__ typedef unsigned long int __fsblkcnt_t;
+__extension__ typedef __u_quad_t __fsblkcnt64_t;
+__extension__ typedef unsigned long int __fsfilcnt_t;
+__extension__ typedef __u_quad_t __fsfilcnt64_t;
+__extension__ typedef int __fsword_t;
+__extension__ typedef int __ssize_t;
+__extension__ typedef long int __syscall_slong_t;
+__extension__ typedef unsigned long int __syscall_ulong_t;
+typedef __off64_t __loff_t;
+typedef char *__caddr_t;
+__extension__ typedef int __intptr_t;
+__extension__ typedef unsigned int __socklen_t;
+typedef int __sig_atomic_t;
+static __inline unsigned int
+__bswap_32 (unsigned int __bsx)
+{
+  return __builtin_bswap32 (__bsx);
+}
+static __inline __uint64_t
+__bswap_64 (__uint64_t __bsx)
+{
+  return __builtin_bswap64 (__bsx);
+}
+static __inline __uint16_t
+__uint16_identity (__uint16_t __x)
+{
+  return __x;
+}
+static __inline __uint32_t
+__uint32_identity (__uint32_t __x)
+{
+  return __x;
+}
+static __inline __uint64_t
+__uint64_identity (__uint64_t __x)
+{
+  return __x;
+}
+typedef unsigned int size_t;
+typedef __time_t time_t;
+struct timespec
+{
+  __time_t tv_sec;
+  __syscall_slong_t tv_nsec;
+};
+typedef __pid_t pid_t;
+struct sched_param
+{
+  int sched_priority;
+};
+
+
+typedef unsigned long int __cpu_mask;
+typedef struct
+{
+  __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))];
+} cpu_set_t;
+
+extern int __sched_cpucount (size_t __setsize, const cpu_set_t *__setp)
+     __attribute__ ((__nothrow__ , __leaf__));
+extern cpu_set_t *__sched_cpualloc (size_t __count) __attribute__ ((__nothrow__ , __leaf__)) ;
+extern void __sched_cpufree (cpu_set_t *__set) __attribute__ ((__nothrow__ , __leaf__));
+
+
+extern int sched_setparam (__pid_t __pid, const struct sched_param *__param)
+     __attribute__ ((__nothrow__ , __leaf__));
+extern int sched_getparam (__pid_t __pid, struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__));
+extern int sched_setscheduler (__pid_t __pid, int __policy,
+          const struct sched_param *__param) __attribute__ ((__nothrow__ , __leaf__));
+extern int sched_getscheduler (__pid_t __pid) __attribute__ ((__nothrow__ , __leaf__));
+extern int sched_yield (void) __attribute__ ((__nothrow__ , __leaf__));
+extern int sched_get_priority_max (int __algorithm) __attribute__ ((__nothrow__ , __leaf__));
+extern int sched_get_priority_min (int __algorithm) __attribute__ ((__nothrow__ , __leaf__));
+extern int sched_rr_get_interval (__pid_t __pid, struct timespec *__t) __attribute__ ((__nothrow__ , __leaf__));
+
+typedef __clock_t clock_t;
+struct tm
+{
+  int tm_sec;
+  int tm_min;
+  int tm_hour;
+  int tm_mday;
+  int tm_mon;
+  int tm_year;
+  int tm_wday;
+  int tm_yday;
+  int tm_isdst;
+  long int tm_gmtoff;
+  const char *tm_zone;
+};
+typedef __clockid_t clockid_t;
+typedef __timer_t timer_t;
+struct itimerspec
+  {
+    struct timespec it_interval;
+    struct timespec it_value;
+  };
+struct sigevent;
+struct __locale_struct
+{
+  struct __locale_data *__locales[13];
+  const unsigned short int *__ctype_b;
+  const int *__ctype_tolower;
+  const int *__ctype_toupper;
+  const char *__names[13];
+};
+typedef struct __locale_struct *__locale_t;
+typedef __locale_t locale_t;
+
+extern clock_t clock (void) __attribute__ ((__nothrow__ , __leaf__));
+extern time_t time (time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
+extern double difftime (time_t __time1, time_t __time0)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
+extern time_t mktime (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
+extern size_t strftime (char *__restrict __s, size_t __maxsize,
+   const char *__restrict __format,
+   const struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
+extern size_t strftime_l (char *__restrict __s, size_t __maxsize,
+     const char *__restrict __format,
+     const struct tm *__restrict __tp,
+     locale_t __loc) __attribute__ ((__nothrow__ , __leaf__));
+extern struct tm *gmtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
+extern struct tm *localtime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
+extern struct tm *gmtime_r (const time_t *__restrict __timer,
+       struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
+extern struct tm *localtime_r (const time_t *__restrict __timer,
+          struct tm *__restrict __tp) __attribute__ ((__nothrow__ , __leaf__));
+extern char *asctime (const struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
+extern char *ctime (const time_t *__timer) __attribute__ ((__nothrow__ , __leaf__));
+extern char *asctime_r (const struct tm *__restrict __tp,
+   char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
+extern char *ctime_r (const time_t *__restrict __timer,
+        char *__restrict __buf) __attribute__ ((__nothrow__ , __leaf__));
+extern char *__tzname[2];
+extern int __daylight;
+extern long int __timezone;
+extern char *tzname[2];
+extern void tzset (void) __attribute__ ((__nothrow__ , __leaf__));
+extern int daylight;
+extern long int timezone;
+extern int stime (const time_t *__when) __attribute__ ((__nothrow__ , __leaf__));
+extern time_t timegm (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
+extern time_t timelocal (struct tm *__tp) __attribute__ ((__nothrow__ , __leaf__));
+extern int dysize (int __year) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
+extern int nanosleep (const struct timespec *__requested_time,
+        struct timespec *__remaining);
+extern int clock_getres (clockid_t __clock_id, struct timespec *__res) __attribute__ ((__nothrow__ , __leaf__));
+extern int clock_gettime (clockid_t __clock_id, struct timespec *__tp) __attribute__ ((__nothrow__ , __leaf__));
+extern int clock_settime (clockid_t __clock_id, const struct timespec *__tp)
+     __attribute__ ((__nothrow__ , __leaf__));
+extern int clock_nanosleep (clockid_t __clock_id, int __flags,
+       const struct timespec *__req,
+       struct timespec *__rem);
+extern int clock_getcpuclockid (pid_t __pid, clockid_t *__clock_id) __attribute__ ((__nothrow__ , __leaf__));
+extern int timer_create (clockid_t __clock_id,
+    struct sigevent *__restrict __evp,
+    timer_t *__restrict __timerid) __attribute__ ((__nothrow__ , __leaf__));
+extern int timer_delete (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__));
+extern int timer_settime (timer_t __timerid, int __flags,
+     const struct itimerspec *__restrict __value,
+     struct itimerspec *__restrict __ovalue) __attribute__ ((__nothrow__ , __leaf__));
+extern int timer_gettime (timer_t __timerid, struct itimerspec *__value)
+     __attribute__ ((__nothrow__ , __leaf__));
+extern int timer_getoverrun (timer_t __timerid) __attribute__ ((__nothrow__ , __leaf__));
+extern int timespec_get (struct timespec *__ts, int __base)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+
+struct __pthread_rwlock_arch_t
+{
+  unsigned int __readers;
+  unsigned int __writers;
+  unsigned int __wrphase_futex;
+  unsigned int __writers_futex;
+  unsigned int __pad3;
+  unsigned int __pad4;
+  unsigned char __flags;
+  unsigned char __shared;
+  signed char __rwelision;
+  unsigned char __pad2;
+  int __cur_writer;
+};
+typedef struct __pthread_internal_slist
+{
+  struct __pthread_internal_slist *__next;
+} __pthread_slist_t;
+struct __pthread_mutex_s
+{
+  int __lock ;
+  unsigned int __count;
+  int __owner;
+  int __kind;
+ 
+  unsigned int __nusers;
+  __extension__ union
+  {
+    struct { short __espins; short __eelision; } __elision_data;
+    __pthread_slist_t __list;
+  };
+ 
+};
+struct __pthread_cond_s
+{
+  __extension__ union
+  {
+    __extension__ unsigned long long int __wseq;
+    struct
+    {
+      unsigned int __low;
+      unsigned int __high;
+    } __wseq32;
+  };
+  __extension__ union
+  {
+    __extension__ unsigned long long int __g1_start;
+    struct
+    {
+      unsigned int __low;
+      unsigned int __high;
+    } __g1_start32;
+  };
+  unsigned int __g_refs[2] ;
+  unsigned int __g_size[2];
+  unsigned int __g1_orig_size;
+  unsigned int __wrefs;
+  unsigned int __g_signals[2];
+};
+typedef unsigned long int pthread_t;
+typedef union
+{
+  char __size[4];
+  int __align;
+} pthread_mutexattr_t;
+typedef union
+{
+  char __size[4];
+  int __align;
+} pthread_condattr_t;
+typedef unsigned int pthread_key_t;
+typedef int pthread_once_t;
+union pthread_attr_t
+{
+  char __size[36];
+  long int __align;
+};
+typedef union pthread_attr_t pthread_attr_t;
+typedef union
+{
+  struct __pthread_mutex_s __data;
+  char __size[24];
+  long int __align;
+} pthread_mutex_t;
+typedef union
+{
+  struct __pthread_cond_s __data;
+  char __size[48];
+  __extension__ long long int __align;
+} pthread_cond_t;
+typedef union
+{
+  struct __pthread_rwlock_arch_t __data;
+  char __size[32];
+  long int __align;
+} pthread_rwlock_t;
+typedef union
+{
+  char __size[8];
+  long int __align;
+} pthread_rwlockattr_t;
+typedef volatile int pthread_spinlock_t;
+typedef union
+{
+  char __size[20];
+  long int __align;
+} pthread_barrier_t;
+typedef union
+{
+  char __size[4];
+  int __align;
+} pthread_barrierattr_t;
+typedef int __jmp_buf[6];
+enum
+{
+  PTHREAD_CREATE_JOINABLE,
+  PTHREAD_CREATE_DETACHED
+};
+enum
+{
+  PTHREAD_MUTEX_TIMED_NP,
+  PTHREAD_MUTEX_RECURSIVE_NP,
+  PTHREAD_MUTEX_ERRORCHECK_NP,
+  PTHREAD_MUTEX_ADAPTIVE_NP
+  ,
+  PTHREAD_MUTEX_NORMAL = PTHREAD_MUTEX_TIMED_NP,
+  PTHREAD_MUTEX_RECURSIVE = PTHREAD_MUTEX_RECURSIVE_NP,
+  PTHREAD_MUTEX_ERRORCHECK = PTHREAD_MUTEX_ERRORCHECK_NP,
+  PTHREAD_MUTEX_DEFAULT = PTHREAD_MUTEX_NORMAL
+};
+enum
+{
+  PTHREAD_MUTEX_STALLED,
+  PTHREAD_MUTEX_STALLED_NP = PTHREAD_MUTEX_STALLED,
+  PTHREAD_MUTEX_ROBUST,
+  PTHREAD_MUTEX_ROBUST_NP = PTHREAD_MUTEX_ROBUST
+};
+enum
+{
+  PTHREAD_PRIO_NONE,
+  PTHREAD_PRIO_INHERIT,
+  PTHREAD_PRIO_PROTECT
+};
+enum
+{
+  PTHREAD_RWLOCK_PREFER_READER_NP,
+  PTHREAD_RWLOCK_PREFER_WRITER_NP,
+  PTHREAD_RWLOCK_PREFER_WRITER_NONRECURSIVE_NP,
+  PTHREAD_RWLOCK_DEFAULT_NP = PTHREAD_RWLOCK_PREFER_READER_NP
+};
+enum
+{
+  PTHREAD_INHERIT_SCHED,
+  PTHREAD_EXPLICIT_SCHED
+};
+enum
+{
+  PTHREAD_SCOPE_SYSTEM,
+  PTHREAD_SCOPE_PROCESS
+};
+enum
+{
+  PTHREAD_PROCESS_PRIVATE,
+  PTHREAD_PROCESS_SHARED
+};
+struct _pthread_cleanup_buffer
+{
+  void (*__routine) (void *);
+  void *__arg;
+  int __canceltype;
+  struct _pthread_cleanup_buffer *__prev;
+};
+enum
+{
+  PTHREAD_CANCEL_ENABLE,
+  PTHREAD_CANCEL_DISABLE
+};
+enum
+{
+  PTHREAD_CANCEL_DEFERRED,
+  PTHREAD_CANCEL_ASYNCHRONOUS
+};
+
+extern int pthread_create (pthread_t *__restrict __newthread,
+      const pthread_attr_t *__restrict __attr,
+      void *(*__start_routine) (void *),
+      void *__restrict __arg) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 3)));
+extern void pthread_exit (void *__retval) __attribute__ ((__noreturn__));
+extern int pthread_join (pthread_t __th, void **__thread_return);
+extern int pthread_detach (pthread_t __th) __attribute__ ((__nothrow__ , __leaf__));
+extern pthread_t pthread_self (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
+extern int pthread_equal (pthread_t __thread1, pthread_t __thread2)
+  __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));
+extern int pthread_attr_init (pthread_attr_t *__attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_destroy (pthread_attr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_getdetachstate (const pthread_attr_t *__attr,
+     int *__detachstate)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_setdetachstate (pthread_attr_t *__attr,
+     int __detachstate)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_getguardsize (const pthread_attr_t *__attr,
+          size_t *__guardsize)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_setguardsize (pthread_attr_t *__attr,
+          size_t __guardsize)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_getschedparam (const pthread_attr_t *__restrict __attr,
+           struct sched_param *__restrict __param)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_setschedparam (pthread_attr_t *__restrict __attr,
+           const struct sched_param *__restrict
+           __param) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_getschedpolicy (const pthread_attr_t *__restrict
+     __attr, int *__restrict __policy)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_setschedpolicy (pthread_attr_t *__attr, int __policy)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_getinheritsched (const pthread_attr_t *__restrict
+      __attr, int *__restrict __inherit)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_setinheritsched (pthread_attr_t *__attr,
+      int __inherit)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_getscope (const pthread_attr_t *__restrict __attr,
+      int *__restrict __scope)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_setscope (pthread_attr_t *__attr, int __scope)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_getstackaddr (const pthread_attr_t *__restrict
+          __attr, void **__restrict __stackaddr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))) __attribute__ ((__deprecated__));
+extern int pthread_attr_setstackaddr (pthread_attr_t *__attr,
+          void *__stackaddr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) __attribute__ ((__deprecated__));
+extern int pthread_attr_getstacksize (const pthread_attr_t *__restrict
+          __attr, size_t *__restrict __stacksize)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_attr_setstacksize (pthread_attr_t *__attr,
+          size_t __stacksize)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_attr_getstack (const pthread_attr_t *__restrict __attr,
+      void **__restrict __stackaddr,
+      size_t *__restrict __stacksize)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3)));
+extern int pthread_attr_setstack (pthread_attr_t *__attr, void *__stackaddr,
+      size_t __stacksize) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_setschedparam (pthread_t __target_thread, int __policy,
+      const struct sched_param *__param)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3)));
+extern int pthread_getschedparam (pthread_t __target_thread,
+      int *__restrict __policy,
+      struct sched_param *__restrict __param)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 3)));
+extern int pthread_setschedprio (pthread_t __target_thread, int __prio)
+     __attribute__ ((__nothrow__ , __leaf__));
+extern int pthread_once (pthread_once_t *__once_control,
+    void (*__init_routine) (void)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_setcancelstate (int __state, int *__oldstate);
+extern int pthread_setcanceltype (int __type, int *__oldtype);
+extern int pthread_cancel (pthread_t __th);
+extern void pthread_testcancel (void);
+typedef struct
+{
+  struct
+  {
+    __jmp_buf __cancel_jmp_buf;
+    int __mask_was_saved;
+  } __cancel_jmp_buf[1];
+  void *__pad[4];
+} __pthread_unwind_buf_t __attribute__ ((__aligned__));
+struct __pthread_cleanup_frame
+{
+  void (*__cancel_routine) (void *);
+  void *__cancel_arg;
+  int __do_it;
+  int __cancel_type;
+};
+extern void __pthread_register_cancel (__pthread_unwind_buf_t *__buf)
+     __attribute__ ((__regparm__ (1)));
+extern void __pthread_unregister_cancel (__pthread_unwind_buf_t *__buf)
+  __attribute__ ((__regparm__ (1)));
+extern void __pthread_unwind_next (__pthread_unwind_buf_t *__buf)
+     __attribute__ ((__regparm__ (1))) __attribute__ ((__noreturn__))
+     __attribute__ ((__weak__))
+     ;
+struct __jmp_buf_tag;
+extern int __sigsetjmp (struct __jmp_buf_tag *__env, int __savemask) __attribute__ ((__nothrow__));
+extern int pthread_mutex_init (pthread_mutex_t *__mutex,
+          const pthread_mutexattr_t *__mutexattr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutex_destroy (pthread_mutex_t *__mutex)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutex_trylock (pthread_mutex_t *__mutex)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutex_lock (pthread_mutex_t *__mutex)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutex_timedlock (pthread_mutex_t *__restrict __mutex,
+        const struct timespec *__restrict
+        __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_mutex_unlock (pthread_mutex_t *__mutex)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutex_getprioceiling (const pthread_mutex_t *
+      __restrict __mutex,
+      int *__restrict __prioceiling)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_mutex_setprioceiling (pthread_mutex_t *__restrict __mutex,
+      int __prioceiling,
+      int *__restrict __old_ceiling)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 3)));
+extern int pthread_mutex_consistent (pthread_mutex_t *__mutex)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutexattr_init (pthread_mutexattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutexattr_destroy (pthread_mutexattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutexattr_getpshared (const pthread_mutexattr_t *
+      __restrict __attr,
+      int *__restrict __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_mutexattr_setpshared (pthread_mutexattr_t *__attr,
+      int __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutexattr_gettype (const pthread_mutexattr_t *__restrict
+          __attr, int *__restrict __kind)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_mutexattr_settype (pthread_mutexattr_t *__attr, int __kind)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutexattr_getprotocol (const pthread_mutexattr_t *
+       __restrict __attr,
+       int *__restrict __protocol)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_mutexattr_setprotocol (pthread_mutexattr_t *__attr,
+       int __protocol)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutexattr_getprioceiling (const pthread_mutexattr_t *
+          __restrict __attr,
+          int *__restrict __prioceiling)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_mutexattr_setprioceiling (pthread_mutexattr_t *__attr,
+          int __prioceiling)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_mutexattr_getrobust (const pthread_mutexattr_t *__attr,
+     int *__robustness)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_mutexattr_setrobust (pthread_mutexattr_t *__attr,
+     int __robustness)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlock_init (pthread_rwlock_t *__restrict __rwlock,
+    const pthread_rwlockattr_t *__restrict
+    __attr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlock_destroy (pthread_rwlock_t *__rwlock)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlock_rdlock (pthread_rwlock_t *__rwlock)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlock_tryrdlock (pthread_rwlock_t *__rwlock)
+  __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlock_timedrdlock (pthread_rwlock_t *__restrict __rwlock,
+           const struct timespec *__restrict
+           __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_rwlock_wrlock (pthread_rwlock_t *__rwlock)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlock_trywrlock (pthread_rwlock_t *__rwlock)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlock_timedwrlock (pthread_rwlock_t *__restrict __rwlock,
+           const struct timespec *__restrict
+           __abstime) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_rwlock_unlock (pthread_rwlock_t *__rwlock)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlockattr_init (pthread_rwlockattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlockattr_destroy (pthread_rwlockattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlockattr_getpshared (const pthread_rwlockattr_t *
+       __restrict __attr,
+       int *__restrict __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_rwlockattr_setpshared (pthread_rwlockattr_t *__attr,
+       int __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_rwlockattr_getkind_np (const pthread_rwlockattr_t *
+       __restrict __attr,
+       int *__restrict __pref)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_rwlockattr_setkind_np (pthread_rwlockattr_t *__attr,
+       int __pref) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_cond_init (pthread_cond_t *__restrict __cond,
+         const pthread_condattr_t *__restrict __cond_attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_cond_destroy (pthread_cond_t *__cond)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_cond_signal (pthread_cond_t *__cond)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_cond_broadcast (pthread_cond_t *__cond)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_cond_wait (pthread_cond_t *__restrict __cond,
+         pthread_mutex_t *__restrict __mutex)
+     __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_cond_timedwait (pthread_cond_t *__restrict __cond,
+       pthread_mutex_t *__restrict __mutex,
+       const struct timespec *__restrict __abstime)
+     __attribute__ ((__nonnull__ (1, 2, 3)));
+extern int pthread_condattr_init (pthread_condattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_condattr_destroy (pthread_condattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_condattr_getpshared (const pthread_condattr_t *
+     __restrict __attr,
+     int *__restrict __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_condattr_setpshared (pthread_condattr_t *__attr,
+     int __pshared) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_condattr_getclock (const pthread_condattr_t *
+          __restrict __attr,
+          __clockid_t *__restrict __clock_id)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_condattr_setclock (pthread_condattr_t *__attr,
+          __clockid_t __clock_id)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_spin_init (pthread_spinlock_t *__lock, int __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_spin_destroy (pthread_spinlock_t *__lock)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_spin_lock (pthread_spinlock_t *__lock)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_spin_trylock (pthread_spinlock_t *__lock)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_spin_unlock (pthread_spinlock_t *__lock)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_barrier_init (pthread_barrier_t *__restrict __barrier,
+     const pthread_barrierattr_t *__restrict
+     __attr, unsigned int __count)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_barrier_destroy (pthread_barrier_t *__barrier)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_barrier_wait (pthread_barrier_t *__barrier)
+     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_barrierattr_init (pthread_barrierattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_barrierattr_destroy (pthread_barrierattr_t *__attr)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_barrierattr_getpshared (const pthread_barrierattr_t *
+        __restrict __attr,
+        int *__restrict __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));
+extern int pthread_barrierattr_setpshared (pthread_barrierattr_t *__attr,
+        int __pshared)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_key_create (pthread_key_t *__key,
+          void (*__destr_function) (void *))
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
+extern int pthread_key_delete (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
+extern void *pthread_getspecific (pthread_key_t __key) __attribute__ ((__nothrow__ , __leaf__));
+extern int pthread_setspecific (pthread_key_t __key,
+    const void *__pointer) __attribute__ ((__nothrow__ , __leaf__)) ;
+extern int pthread_getcpuclockid (pthread_t __thread_id,
+      __clockid_t *__clock_id)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));
+extern int pthread_atfork (void (*__prepare) (void),
+      void (*__parent) (void),
+      void (*__child) (void)) __attribute__ ((__nothrow__ , __leaf__));
+
diff --git a/headers/setjmp.h b/headers/setjmp.h
new file mode 100644
index 0000000000..6dcb0255b8
--- /dev/null
+++ b/headers/setjmp.h
@@ -0,0 +1,4 @@
+#define NULL ((void *)0)
+typedef void* jmp_buf;
+extern int setjmp(jmp_buf __jmpb);
+extern void longjmp(jmp_buf __jmpb, int __ret);
diff --git a/headers/signal.h b/headers/signal.h
new file mode 100644
index 0000000000..fed8ef0b7c
--- /dev/null
+++ b/headers/signal.h
@@ -0,0 +1,3 @@
+#define NULL ((void *)0)
+extern void (*signal(int sig, void (*func)(int)))(int);
+extern int raise(int sig);
diff --git a/headers/stdarg.h b/headers/stdarg.h
new file mode 100644
index 0000000000..e383a4c770
--- /dev/null
+++ b/headers/stdarg.h
@@ -0,0 +1,2 @@
+#define NULL ((void *)0)
+typedef char* va_list;
diff --git a/headers/stddef.h b/headers/stddef.h
new file mode 100644
index 0000000000..e122b7efad
--- /dev/null
+++ b/headers/stddef.h
@@ -0,0 +1,2 @@
+typedef unsigned size_t;
+#define NULL ((void *)0)
diff --git a/headers/stdint.h b/headers/stdint.h
new file mode 100644
index 0000000000..8c5435078d
--- /dev/null
+++ b/headers/stdint.h
@@ -0,0 +1,11 @@
+#define NULL ((void *)0)
+typedef char int8_t;
+typedef short int16_t;
+typedef long int32_t;
+typedef long long int64_t;
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned long uint32_t;
+typedef unsigned long long uint64_t;
+typedef long intptr_t;
+typedef unsigned long uintptr_t;
diff --git a/headers/stdio.h b/headers/stdio.h
new file mode 100644
index 0000000000..506e6b9510
--- /dev/null
+++ b/headers/stdio.h
@@ -0,0 +1,60 @@
+#define NULL ((void *)0)
+typedef long int ptrdiff_t;
+typedef long unsigned int size_t;
+typedef int wchar_t;
+typedef struct {
+  long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
+  long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
+} max_align_t;
+  typedef __typeof__(nullptr) nullptr_t;
+typedef __builtin_va_list __gnuc_va_list;
+typedef __gnuc_va_list va_list;
+typedef void FILE;
+extern FILE *stdin, *stdout, *stderr;
+typedef long fpos_t;
+extern int remove(const char *filename);
+extern int rename(const char *old, const char *new_);
+extern FILE *tmpfile(void);
+extern char *tmpnam(char *s);
+extern int fclose(FILE *stream);
+extern int fflush(FILE *stream);
+extern FILE *fopen(const char * filename, const char * mode);
+extern FILE *freopen(const char * filename, const char * mode, FILE * stream);
+extern void setbuf(FILE * stream, char * buf);
+extern int setvbuf(FILE * stream, char * buf, int mode, size_t size);
+extern int fprintf(FILE * stream, const char * format, ...);
+extern int fscanf(FILE * stream, const char * format, ...);
+extern int printf(const char * format, ...);
+extern int scanf(const char * format, ...);
+extern int snprintf(char * s, size_t n, const char * format, ...);
+extern int sprintf(char * s, const char * format, ...);
+extern int sscanf(const char * s, const char * format, ...);
+extern int vfprintf(FILE * stream, const char * format, va_list arg);
+extern int vfscanf(FILE * stream, const char * format, va_list arg);
+extern int vprintf(const char * format, va_list arg);
+extern int vscanf(const char * format, va_list arg);
+extern int vsnprintf(char * s, size_t n, const char * format, va_list arg);
+extern int vsprintf(char * s, const char * format, va_list arg);
+extern int vsscanf(const char * s, const char * format, va_list arg);
+extern int fgetc(FILE *stream);
+extern char *fgets(char * s, int n, FILE * stream);
+extern int fputc(int c, FILE *stream);
+extern int fputs(const char * s, FILE * stream);
+extern int getc(FILE *stream);
+extern int getchar(void);
+extern char *gets(char *s);
+extern int putc(int c, FILE *stream);
+extern int putchar(int c);
+extern int puts(const char *s);
+extern int ungetc(int c, FILE *stream);
+extern size_t fread(void * ptr, size_t size, size_t nmemb, FILE * stream);
+extern size_t fwrite(const void * ptr, size_t size, size_t nmemb, FILE * stream);
+extern int fgetpos(FILE * stream, fpos_t * pos);
+extern int fseek(FILE *stream, long int offset, int whence);
+extern int fsetpos(FILE *stream, const fpos_t *pos);
+extern long int ftell(FILE *stream);
+extern void rewind(FILE *stream);
+extern void clearerr(FILE *stream);
+extern int feof(FILE *stream);
+extern int ferror(FILE *stream);
+extern void perror(const char *s);
diff --git a/headers/stdlib.h b/headers/stdlib.h
new file mode 100644
index 0000000000..3ef9823d0a
--- /dev/null
+++ b/headers/stdlib.h
@@ -0,0 +1,44 @@
+#define NULL ((void *)0)
+typedef long int ptrdiff_t;
+typedef long unsigned int size_t;
+typedef int wchar_t;
+typedef struct {
+  long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
+  long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
+} max_align_t;
+  typedef __typeof__(nullptr) nullptr_t;
+typedef struct { int quot, rem; } div_t;
+typedef struct { long quot, rem; } ldiv_t;
+typedef struct { long long quot, rem; } lldiv_t;
+extern double atof(const char *nptr);
+extern int atoi(const char *nptr);
+extern long int atol(const char *nptr);
+extern long long int atoll(const char *nptr);
+extern double strtod(const char * nptr, char ** endptr);
+extern float strtof(const char * nptr, char ** endptr);
+extern long double strtold(const char * nptr, char ** endptr);
+extern long int strtol(const char * nptr, char ** endptr, int base);
+extern long long int strtoll(const char * nptr, char ** endptr, int base);
+extern unsigned long int strtoul(const char * nptr, char ** endptr, int base);
+extern unsigned long long int strtoull(const char * nptr, char ** endptr, int base);
+extern int rand(void);
+extern void srand(unsigned int seed);
+extern void *calloc(size_t nmemb, size_t size);
+extern void free(void *ptr);
+extern void *malloc(size_t size);
+extern void *realloc(void *ptr, size_t size);
+extern void abort(void);
+extern int atexit(void (*func)(void));
+extern void exit(int status);
+extern void _Exit(int status);
+extern char *getenv(const char *name);
+extern int system(const char *string);
+extern void *bsearch(const void *key, const void *base, size_t nmemb, size_t size, int (*compar)(const void *, const void *));
+extern void qsort(void *base, size_t nmemb, size_t size, int (*compar)(const void *, const void *));
+extern int abs(int j);
+extern long int labs(long int j);
+extern long long int llabs(long long int j);
+extern div_t div(int numer, int denom);
+extern ldiv_t ldiv(long int numer, long int denom);
+extern lldiv_t lldiv(long long int numer, long long int denom);
+extern int mblen(const char *s, size_t n);
diff --git a/headers/string.h b/headers/string.h
new file mode 100644
index 0000000000..5725393358
--- /dev/null
+++ b/headers/string.h
@@ -0,0 +1,31 @@
+#define NULL ((void *)0)
+typedef long int ptrdiff_t;
+typedef long unsigned int size_t;
+typedef int wchar_t;
+typedef struct {
+  long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
+  long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
+} max_align_t;
+  typedef __typeof__(nullptr) nullptr_t;
+extern void *memcpy(void * s1, const void * s2, size_t n);
+extern void *memmove(void *s1, const void *s2, size_t n);
+extern char *strcpy(char * s1, const char * s2);
+extern char *strncpy(char * s1, const char * s2, size_t n);
+extern char *strcat(char * s1, const char * s2);
+extern char *strncat(char * s1, const char * s2, size_t n);
+extern int memcmp(const void *s1, const void *s2, size_t n);
+extern int strcmp(const char *s1, const char *s2);
+extern int strcoll(const char *s1, const char *s2);
+extern int strncmp(const char *s1, const char *s2, size_t n);
+extern size_t strxfrm(char * s1, const char * s2, size_t n);
+extern void *memchr(const void *s, int c, size_t n);
+extern char *strchr(const char *s, int c);
+extern size_t strcspn(const char *s1, const char *s2);
+extern char *strpbrk(const char *s1, const char *s2);
+extern char *strrchr(const char *s, int c);
+extern size_t strspn(const char *s1, const char *s2);
+extern char *strstr(const char *s1, const char *s2);
+extern char *strtok(char * s1, const char * s2);
+extern void *memset(void *s, int c, size_t n);
+extern char *strerror(int errnum);
+extern size_t strlen(const char *s);
diff --git a/headers/time.h b/headers/time.h
new file mode 100644
index 0000000000..0ccb1c0dfc
--- /dev/null
+++ b/headers/time.h
@@ -0,0 +1,31 @@
+#define NULL ((void *)0)
+typedef long int ptrdiff_t;
+typedef long unsigned int size_t;
+typedef int wchar_t;
+typedef struct {
+  long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
+  long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
+} max_align_t;
+  typedef __typeof__(nullptr) nullptr_t;
+struct tm {
+    int tm_sec;
+    int tm_min;
+    int tm_hour;
+    int tm_mday;
+    int tm_mon;
+    int tm_year;
+    int tm_wday;
+    int tm_yday;
+    int tm_isdst;
+};
+typedef long time_t;
+typedef long clock_t;
+extern clock_t clock(void);
+extern double difftime(time_t time1, time_t time0);
+extern time_t mktime(struct tm *timeptr);
+extern time_t time(time_t *timer);
+extern char *asctime(const struct tm *timeptr);
+extern char *ctime(const time_t *timer);
+extern struct tm *gmtime(const time_t *timer);
+extern struct tm *localtime(const time_t *timer);
+extern size_t strftime(char * s, size_t maxsize, const char * format, const struct tm * timeptr);
diff --git a/main.py b/main.py
index 5f8698ae5e..3dffe17d49 100644
--- a/main.py
+++ b/main.py
@@ -28,11 +28,35 @@
 from tweaks import reach_error, fix_inline, fix_struct_def
 from witness2ast import apply_witness
 
+HEADERS_DIR = os.path.dirname(os.path.abspath(sys.argv[0])) + os.sep + "headers"
+
+# pycparser only understands standard C, so GNU extensions used by the stub
+# headers (and by real system headers, for anything the stubs don't cover)
+# are preprocessed away rather than parsed.
+CPP_GNU_COMPAT_ARGS = [
+    "-D__attribute__(x)=",
+    "-D__extension__=",
+    "-D__restrict=",
+    "-D__restrict__=",
+    "-D__inline=inline",
+    "-D__inline__=inline",
+    "-D__const=const",
+    "-D__signed__=signed",
+    "-D__volatile__=volatile",
+    "-D__typeof__(x)=void*",
+    "-D__builtin_va_list=void*",
+]
+
 
 def translate_to_c(filename, witness, mode, timeout):
     """Apply the witness to the parsed AST, then compile and run the result."""
     try:
-        ast = parse_file(filename, use_cpp=False)
+        ast = parse_file(
+            filename,
+            use_cpp=True,
+            cpp_path="cpp",
+            cpp_args=["-I" + HEADERS_DIR] + CPP_GNU_COMPAT_ARGS,
+        )
     except KnownErrorVerdict as e:
         print("Verdict: " + e.verdict)
         sys.exit(-1)
diff --git a/package.sh b/package.sh
index 69f8a88f8d..b1136fb6be 100755
--- a/package.sh
+++ b/package.sh
@@ -17,7 +17,7 @@ python3 -m zipapp build -o ConcurrentWitness2Test.pyz -p "/usr/bin/env python3"
 rm -rf build
 
 mkdir ConcurrentWitness2Test
-cp ConcurrentWitness2Test.pyz *.md LICENSE svcomp.c example smoketest.sh ConcurrentWitness2Test/ -r
+cp ConcurrentWitness2Test.pyz *.md LICENSE svcomp.c example headers smoketest.sh ConcurrentWitness2Test/ -r
 printf '#!/bin/bash\nscriptdir=$(dirname "$0")\npython3 "$scriptdir"/ConcurrentWitness2Test.pyz "$@"\n' > ConcurrentWitness2Test/start.sh
 chmod +x ConcurrentWitness2Test/start.sh ConcurrentWitness2Test/smoketest.sh
 zip ConcurrentWitness2Test.zip ConcurrentWitness2Test -r

From 07a91201fd45d61ff09702c9835574af5307c671 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Fri, 19 Jun 2026 18:53:56 +0200
Subject: [PATCH 05/10] fixed parsing

---
 headers/assert.h    |  6 +++-
 headers/limits.h    | 23 +++++++++++++
 headers/pthread.h   |  8 ++++-
 headers/stdatomic.h | 83 +++++++++++++++++++++++++++++++++++++++++++++
 headers/stddef.h    |  2 +-
 headers/stdio.h     |  3 ++
 headers/stdlib.h    |  3 ++
 headers/string.h    |  3 ++
 headers/time.h      |  3 ++
 main.py             | 10 +++---
 tweaks.py           |  4 ++-
 11 files changed, 138 insertions(+), 10 deletions(-)
 create mode 100644 headers/stdatomic.h

diff --git a/headers/assert.h b/headers/assert.h
index 1cba3a007f..af05c8214d 100644
--- a/headers/assert.h
+++ b/headers/assert.h
@@ -1,4 +1,8 @@
 #define NULL ((void *)0)
 extern void abort(void);
 extern int printf(const char * format, ...);
-extern void assert(int expression);
+/* Real glibc only ships assert() as a macro (around __assert_fail, which
+   isn't a stable/linkable symbol either) -- not as a real extern function,
+   so declaring it as one leaves "undefined reference to `assert'" at link
+   time for any program that doesn't override the macro itself. */
+#define assert(expression) ((void)((expression) ? 0 : (abort(), 0)))
diff --git a/headers/limits.h b/headers/limits.h
index e69de29bb2..db3ed2ec90 100644
--- a/headers/limits.h
+++ b/headers/limits.h
@@ -0,0 +1,23 @@
+#define CHAR_BIT 8
+
+#define SCHAR_MIN (-128)
+#define SCHAR_MAX 127
+#define UCHAR_MAX 255
+#define CHAR_MIN SCHAR_MIN
+#define CHAR_MAX SCHAR_MAX
+
+#define SHRT_MIN (-32768)
+#define SHRT_MAX 32767
+#define USHRT_MAX 65535
+
+#define INT_MIN (-2147483647 - 1)
+#define INT_MAX 2147483647
+#define UINT_MAX 4294967295U
+
+#define LONG_MIN (-9223372036854775807L - 1)
+#define LONG_MAX 9223372036854775807L
+#define ULONG_MAX 18446744073709551615UL
+
+#define LLONG_MIN (-9223372036854775807LL - 1)
+#define LLONG_MAX 9223372036854775807LL
+#define ULLONG_MAX 18446744073709551615ULL
diff --git a/headers/pthread.h b/headers/pthread.h
index 85a0173aee..a33eff2559 100644
--- a/headers/pthread.h
+++ b/headers/pthread.h
@@ -78,7 +78,7 @@ __uint64_identity (__uint64_t __x)
 {
   return __x;
 }
-typedef unsigned int size_t;
+typedef long unsigned int size_t;
 typedef __time_t time_t;
 struct timespec
 {
@@ -279,6 +279,7 @@ typedef union
 } pthread_condattr_t;
 typedef unsigned int pthread_key_t;
 typedef int pthread_once_t;
+#define PTHREAD_ONCE_INIT 0
 union pthread_attr_t
 {
   char __size[36];
@@ -303,6 +304,11 @@ typedef union
   char __size[32];
   long int __align;
 } pthread_rwlock_t;
+#define PTHREAD_MUTEX_INITIALIZER { 0 }
+#define PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP { 0 }
+#define PTHREAD_ERRORCHECK_MUTEX_INITIALIZER_NP { 0 }
+#define PTHREAD_COND_INITIALIZER { 0 }
+#define PTHREAD_RWLOCK_INITIALIZER { 0 }
 typedef union
 {
   char __size[8];
diff --git a/headers/stdatomic.h b/headers/stdatomic.h
new file mode 100644
index 0000000000..6889531296
--- /dev/null
+++ b/headers/stdatomic.h
@@ -0,0 +1,83 @@
+#define NULL ((void *)0)
+
+typedef enum {
+  memory_order_relaxed,
+  memory_order_consume,
+  memory_order_acquire,
+  memory_order_release,
+  memory_order_acq_rel,
+  memory_order_seq_cst
+} memory_order;
+
+typedef _Bool atomic_bool;
+typedef char atomic_char;
+typedef signed char atomic_schar;
+typedef unsigned char atomic_uchar;
+typedef short atomic_short;
+typedef unsigned short atomic_ushort;
+typedef int atomic_int;
+typedef unsigned int atomic_uint;
+typedef long atomic_long;
+typedef unsigned long atomic_ulong;
+typedef long long atomic_llong;
+typedef unsigned long long atomic_ullong;
+typedef long atomic_intptr_t;
+typedef unsigned long atomic_uintptr_t;
+typedef unsigned long atomic_size_t;
+typedef long atomic_ptrdiff_t;
+typedef long atomic_intmax_t;
+typedef unsigned long atomic_uintmax_t;
+
+typedef struct {
+  int __flag;
+} atomic_flag;
+
+#define ATOMIC_FLAG_INIT \
+  { 0 }
+#define ATOMIC_VAR_INIT(value) (value)
+
+#define atomic_init(obj, value) (*(obj) = (value))
+#define atomic_is_lock_free(obj) 1
+
+#define atomic_load_explicit(obj, order) __atomic_load_n(obj, order)
+#define atomic_load(obj) atomic_load_explicit(obj, memory_order_seq_cst)
+
+#define atomic_store_explicit(obj, value, order) __atomic_store_n(obj, value, order)
+#define atomic_store(obj, value) atomic_store_explicit(obj, value, memory_order_seq_cst)
+
+#define atomic_exchange_explicit(obj, value, order) __atomic_exchange_n(obj, value, order)
+#define atomic_exchange(obj, value) atomic_exchange_explicit(obj, value, memory_order_seq_cst)
+
+#define atomic_fetch_add_explicit(obj, value, order) __atomic_fetch_add(obj, value, order)
+#define atomic_fetch_add(obj, value) atomic_fetch_add_explicit(obj, value, memory_order_seq_cst)
+
+#define atomic_fetch_sub_explicit(obj, value, order) __atomic_fetch_sub(obj, value, order)
+#define atomic_fetch_sub(obj, value) atomic_fetch_sub_explicit(obj, value, memory_order_seq_cst)
+
+#define atomic_fetch_or_explicit(obj, value, order) __atomic_fetch_or(obj, value, order)
+#define atomic_fetch_or(obj, value) atomic_fetch_or_explicit(obj, value, memory_order_seq_cst)
+
+#define atomic_fetch_xor_explicit(obj, value, order) __atomic_fetch_xor(obj, value, order)
+#define atomic_fetch_xor(obj, value) atomic_fetch_xor_explicit(obj, value, memory_order_seq_cst)
+
+#define atomic_fetch_and_explicit(obj, value, order) __atomic_fetch_and(obj, value, order)
+#define atomic_fetch_and(obj, value) atomic_fetch_and_explicit(obj, value, memory_order_seq_cst)
+
+#define atomic_compare_exchange_strong_explicit(obj, expected, desired, success, failure) \
+  __atomic_compare_exchange_n(obj, expected, desired, 0, success, failure)
+#define atomic_compare_exchange_strong(obj, expected, desired) \
+  atomic_compare_exchange_strong_explicit(obj, expected, desired, memory_order_seq_cst, memory_order_seq_cst)
+
+#define atomic_compare_exchange_weak_explicit(obj, expected, desired, success, failure) \
+  __atomic_compare_exchange_n(obj, expected, desired, 1, success, failure)
+#define atomic_compare_exchange_weak(obj, expected, desired) \
+  atomic_compare_exchange_weak_explicit(obj, expected, desired, memory_order_seq_cst, memory_order_seq_cst)
+
+#define atomic_flag_test_and_set_explicit(obj, order) __atomic_test_and_set(&(obj)->__flag, order)
+#define atomic_flag_test_and_set(obj) atomic_flag_test_and_set_explicit(obj, memory_order_seq_cst)
+
+#define atomic_flag_clear_explicit(obj, order) __atomic_clear(&(obj)->__flag, order)
+#define atomic_flag_clear(obj) atomic_flag_clear_explicit(obj, memory_order_seq_cst)
+
+#define atomic_thread_fence(order) __atomic_thread_fence(order)
+#define atomic_signal_fence(order) __atomic_signal_fence(order)
diff --git a/headers/stddef.h b/headers/stddef.h
index e122b7efad..2517c7e0af 100644
--- a/headers/stddef.h
+++ b/headers/stddef.h
@@ -1,2 +1,2 @@
-typedef unsigned size_t;
+typedef long unsigned int size_t;
 #define NULL ((void *)0)
diff --git a/headers/stdio.h b/headers/stdio.h
index 506e6b9510..c9eeb7ae80 100644
--- a/headers/stdio.h
+++ b/headers/stdio.h
@@ -2,10 +2,13 @@
 typedef long int ptrdiff_t;
 typedef long unsigned int size_t;
 typedef int wchar_t;
+#ifndef __CW2T_MAX_ALIGN_T_DEFINED
+#define __CW2T_MAX_ALIGN_T_DEFINED
 typedef struct {
   long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
   long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
 } max_align_t;
+#endif
   typedef __typeof__(nullptr) nullptr_t;
 typedef __builtin_va_list __gnuc_va_list;
 typedef __gnuc_va_list va_list;
diff --git a/headers/stdlib.h b/headers/stdlib.h
index 3ef9823d0a..259429e71d 100644
--- a/headers/stdlib.h
+++ b/headers/stdlib.h
@@ -2,10 +2,13 @@
 typedef long int ptrdiff_t;
 typedef long unsigned int size_t;
 typedef int wchar_t;
+#ifndef __CW2T_MAX_ALIGN_T_DEFINED
+#define __CW2T_MAX_ALIGN_T_DEFINED
 typedef struct {
   long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
   long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
 } max_align_t;
+#endif
   typedef __typeof__(nullptr) nullptr_t;
 typedef struct { int quot, rem; } div_t;
 typedef struct { long quot, rem; } ldiv_t;
diff --git a/headers/string.h b/headers/string.h
index 5725393358..65ae9c4b94 100644
--- a/headers/string.h
+++ b/headers/string.h
@@ -2,10 +2,13 @@
 typedef long int ptrdiff_t;
 typedef long unsigned int size_t;
 typedef int wchar_t;
+#ifndef __CW2T_MAX_ALIGN_T_DEFINED
+#define __CW2T_MAX_ALIGN_T_DEFINED
 typedef struct {
   long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
   long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
 } max_align_t;
+#endif
   typedef __typeof__(nullptr) nullptr_t;
 extern void *memcpy(void * s1, const void * s2, size_t n);
 extern void *memmove(void *s1, const void *s2, size_t n);
diff --git a/headers/time.h b/headers/time.h
index 0ccb1c0dfc..348e69ed85 100644
--- a/headers/time.h
+++ b/headers/time.h
@@ -2,10 +2,13 @@
 typedef long int ptrdiff_t;
 typedef long unsigned int size_t;
 typedef int wchar_t;
+#ifndef __CW2T_MAX_ALIGN_T_DEFINED
+#define __CW2T_MAX_ALIGN_T_DEFINED
 typedef struct {
   long long __max_align_ll __attribute__((__aligned__(__alignof__(long long))));
   long double __max_align_ld __attribute__((__aligned__(__alignof__(long double))));
 } max_align_t;
+#endif
   typedef __typeof__(nullptr) nullptr_t;
 struct tm {
     int tm_sec;
diff --git a/main.py b/main.py
index 3dffe17d49..73e9512fa9 100644
--- a/main.py
+++ b/main.py
@@ -22,7 +22,7 @@
 import traceback
 import argparse
 
-from pycparser import parse_file, c_generator
+from pycparser import preprocess_file, CParser, c_generator
 
 from Exceptions import KnownErrorVerdict
 from tweaks import reach_error, fix_inline, fix_struct_def
@@ -51,12 +51,10 @@
 def translate_to_c(filename, witness, mode, timeout):
     """Apply the witness to the parsed AST, then compile and run the result."""
     try:
-        ast = parse_file(
-            filename,
-            use_cpp=True,
-            cpp_path="cpp",
-            cpp_args=["-I" + HEADERS_DIR] + CPP_GNU_COMPAT_ARGS,
+        text = preprocess_file(
+            filename, cpp_path="cpp", cpp_args=["-I" + HEADERS_DIR] + CPP_GNU_COMPAT_ARGS
         )
+        ast = CParser().parse(text, filename)
     except KnownErrorVerdict as e:
         print("Verdict: " + e.verdict)
         sys.exit(-1)
diff --git a/tweaks.py b/tweaks.py
index 6c25b36083..938b34e4a0 100644
--- a/tweaks.py
+++ b/tweaks.py
@@ -44,7 +44,8 @@ def fix_inline(ast):
         and "static" not in node.decl.storage
     ]
     for inline_def in inline_defs:
-        inline_def.decl.funcspec = ["extern", "inline"]
+        inline_def.decl.storage = ["extern"]
+        inline_def.decl.funcspec = ["inline"]
 
 
 # This is a problem with pycparser
@@ -55,6 +56,7 @@ def fix_struct_def(ast):
             isinstance(node, Decl)
             and isinstance(node.type, TypeDecl)
             and isinstance(node.type.type, Struct)
+            and node.type.type.name is not None  # anonymous structs are never repeats
         ):
             if node.type.type.name in struct_decls:
                 node.type.type = Struct(node.type.type.name, decls=None)

From b8abd484fc5481c40b1014745c5924ded9450e4e Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Sat, 20 Jun 2026 16:44:57 +0200
Subject: [PATCH 06/10] Added demo site

---
 .claude/settings.json         |  36 ++
 hacks.py                      |  74 +++
 main.py                       |  48 +-
 requirements.txt              |   2 +-
 svcomp.c                      |   4 +-
 tweaks.py                     |  17 +
 witness2ast.py                |  66 +--
 www-demo/Dockerfile           |  63 +++
 www-demo/README.md            | 131 +++++
 www-demo/app.js               | 951 ++++++++++++++++++++++++++++++++++
 www-demo/index.html           | 133 +++++
 www-demo/nginx.conf           |  42 ++
 www-demo/py/clang_ast_stub.py |  11 +
 www-demo/py/cwt/instrument.py |  61 +++
 www-demo/py/shim.py           |  62 +++
 www-demo/pyodide-worker.js    |  96 ++++
 www-demo/style.css            | 474 +++++++++++++++++
 www-demo/wasmer-run.js        |  76 +++
 18 files changed, 2269 insertions(+), 78 deletions(-)
 create mode 100644 .claude/settings.json
 create mode 100644 hacks.py
 create mode 100644 www-demo/Dockerfile
 create mode 100644 www-demo/README.md
 create mode 100644 www-demo/app.js
 create mode 100644 www-demo/index.html
 create mode 100644 www-demo/nginx.conf
 create mode 100644 www-demo/py/clang_ast_stub.py
 create mode 100644 www-demo/py/cwt/instrument.py
 create mode 100644 www-demo/py/shim.py
 create mode 100644 www-demo/pyodide-worker.js
 create mode 100644 www-demo/style.css
 create mode 100644 www-demo/wasmer-run.js

diff --git a/.claude/settings.json b/.claude/settings.json
new file mode 100644
index 0000000000..b7394ba3e7
--- /dev/null
+++ b/.claude/settings.json
@@ -0,0 +1,36 @@
+{
+  "permissions": {
+    "allow": [
+      "Bash(python3 -c \"import pycparser, os; print\\(pycparser.__file__\\)\")",
+      "Bash(find / -iname \"fake_libc_include\" -maxdepth 8)",
+      "Bash(./smoketest.sh)",
+      "Bash(python3 -)",
+      "Bash(*)",
+      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/regen.c svcomp.c -o /tmp/regen_bin)",
+      "Bash(echo \"exit: $?\")",
+      "Bash(cpp -I headers -D'__attribute__\\(x\\)=' /home/levente/Documents/University/sv-benchmarks/c/goblint-coreutils/instrumented_dd_comb.c)",
+      "Bash(echo \"smoketest exit: $?\")",
+      "Bash(./package.sh)",
+      "Bash(sed -n '760,770p' /usr/include/pthread.h)",
+      "Read(//usr/include/**)",
+      "Bash(python3 -c \"from pycparser import preprocess_file, CParser; print\\('ok'\\)\")",
+      "Bash(cd /home/levente/Documents/University/concurrency-witnesses/concurrentwitness2test *)",
+      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/szymanski_regen.c svcomp.c -o /tmp/szymanski_bin)",
+      "Bash(grep -c '\\\\$' /home/levente/Documents/University/theta/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/stdlib/stdatomic.h.kt)",
+      "Bash(grep -n \"typedef.*mode_t\\\\|mode_t.*;$\" /home/levente/Documents/University/sv-benchmarks/c/goblint-coreutils/instrumented_dd_comb.c)",
+      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/dd_comb_regen.c svcomp.c -o /tmp/dd_comb_bin)",
+      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/dd_comb_regen2.c svcomp.c -o /tmp/dd_comb_bin2)",
+      "Bash(curl -s --max-time 10 \"https://api.github.com/repos/sosy-lab/sv-benchmarks/contents/c\")",
+      "Bash(echo \"EXIT:$?\")",
+      "Bash(python3 -c \"import json,sys; d=json.load\\(sys.stdin\\); [print\\(x['name']\\) for x in d if x['type']=='dir' and \\('pthread' in x['name'].lower\\(\\) or 'thread' in x['name'].lower\\(\\) or 'concur' in x['name'].lower\\(\\)\\)]\")",
+      "Bash(curl -s --max-time 10 -I \"https://api.github.com/repos/sosy-lab/sv-benchmarks/contents/c/pthread\")",
+      "WebSearch",
+      "WebFetch(domain:wasmer.io)",
+      "WebFetch(domain:raw.githubusercontent.com)"
+    ],
+    "additionalDirectories": [
+      "/tmp",
+      "/home/levente/Documents/University/theta/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/stdlib"
+    ]
+  }
+}
diff --git a/hacks.py b/hacks.py
new file mode 100644
index 0000000000..30a5ca0b4d
--- /dev/null
+++ b/hacks.py
@@ -0,0 +1,74 @@
+"""
+Copyright 2023 Budapest University of Technology and Economics
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+"""
+
+import re
+
+
+def hacks(content):
+    """Blanks out GNU extensions and constructs pycparser can't handle
+    (inline asm, statement expressions, __attribute__), preserving line
+    numbers so witness locations still line up."""
+
+    def replace_with_spaces_str(match_str, offset=0):
+        parens = 0
+        for i, c in enumerate(match_str):
+            if c == "(":
+                parens = parens + 1
+            elif c == ")":
+                parens = parens - 1
+                if parens < 0:
+                    return " " * (i - offset) + match_str[i:]
+                elif parens == 0:
+                    return " " * (i - offset + 1) + match_str[i + 1 :]
+        return " " * (len(match_str) - offset)
+
+    def replace_with_spaces(match):
+        return replace_with_spaces_str(str(match.group(0)))
+
+    def replace_with_spaces_full(match):
+        # Unlike replace_with_spaces, blanks the *entire* match regardless of
+        # paren-balance. Comments can't contain trailing code that needs
+        # preserving (// is bounded by \n, /* */ by its own closing marker),
+        # so paren-counting here only misfires on a comment that happens to
+        # contain a balanced parenthesized expression, e.g.
+        # "// so 'if (x == 1)' is taken" -- replace_with_spaces would stop
+        # right after the ')', leaving a stray quote that fails to lex.
+        return " " * len(match.group(0))
+
+    def replace_with_zero_padded(match):
+        return "0" + replace_with_spaces_str(str(match.group(0)), 1)
+
+    last_content = ""
+    while last_content != content:
+        last_content = content
+        content = re.sub(r"//[^\n]*", replace_with_spaces_full, content)
+        content = re.sub(r"/\*.*\*/", replace_with_spaces_full, content)
+        content = re.sub(r"__attribute__[ \r\n]*\(.*\)", replace_with_spaces, content)
+        content = re.sub(r"__asm__[ \r\n]*\(.*\)", replace_with_spaces, content)
+        content = re.sub(r"asm volatile[ \r\n]*\(.*\)", replace_with_spaces, content)
+        content = re.sub(r"asm[ \r\n]*\(.*\)", replace_with_spaces, content)
+        content = re.sub(
+            r"__extension__[ \r\n]*\(.*\)", replace_with_zero_padded, content
+        )
+        content = re.sub(r"__extension__", replace_with_spaces, content)
+        content = re.sub(r"__inline", replace_with_spaces, content)
+        content = re.sub(r"__restrict", replace_with_spaces, content)
+        content = re.sub(r"__builtin_va_list", "int              ", content)
+        content = re.sub(r"__signed__", "  signed  ", content)
+        content = re.sub(
+            r"\([ \r\n]*\{.*}[ \r\n]*\)", replace_with_zero_padded, content
+        )
+    return content
diff --git a/main.py b/main.py
index 73e9512fa9..1e6f3d43e5 100644
--- a/main.py
+++ b/main.py
@@ -15,7 +15,6 @@
 """
 
 import os
-import re
 import subprocess
 import sys
 import tempfile
@@ -25,7 +24,8 @@
 from pycparser import preprocess_file, CParser, c_generator
 
 from Exceptions import KnownErrorVerdict
-from tweaks import reach_error, fix_inline, fix_struct_def
+from hacks import hacks
+from tweaks import reach_error, fix_inline, fix_struct_def, declare_schedule_functions
 from witness2ast import apply_witness
 
 HEADERS_DIR = os.path.dirname(os.path.abspath(sys.argv[0])) + os.sep + "headers"
@@ -83,6 +83,7 @@ def translate_to_c(filename, witness, mode, timeout):
         fix_inline(ast)
         fix_struct_def(ast)
         reach_error(ast)
+        declare_schedule_functions(ast)
         generator = c_generator.CGenerator()
         with tempfile.NamedTemporaryFile(suffix=".c", delete=False) as tmp:
             tmp.write(generator.visit(ast).encode())
@@ -184,49 +185,6 @@ def translate_to_c(filename, witness, mode, timeout):
         sys.exit(-1)
 
 
-def hacks(content):
-    def replace_with_spaces_str(match_str, offset=0):
-        parens = 0
-        for i, c in enumerate(match_str):
-            if c == "(":
-                parens = parens + 1
-            elif c == ")":
-                parens = parens - 1
-                if parens < 0:
-                    return " " * (i - offset) + match_str[i:]
-                elif parens == 0:
-                    return " " * (i - offset + 1) + match_str[i + 1 :]
-        return " " * (len(match_str) - offset)
-
-    def replace_with_spaces(match):
-        return replace_with_spaces_str(str(match.group(0)))
-
-    def replace_with_zero_padded(match):
-        return "0" + replace_with_spaces_str(str(match.group(0)), 1)
-
-    last_content = ""
-    while last_content != content:
-        last_content = content
-        content = re.sub(r"//[^\n]*", replace_with_spaces, content)
-        content = re.sub(r"/\*.*\*/", replace_with_spaces, content)
-        content = re.sub(r"__attribute__[ \r\n]*\(.*\)", replace_with_spaces, content)
-        content = re.sub(r"__asm__[ \r\n]*\(.*\)", replace_with_spaces, content)
-        content = re.sub(r"asm volatile[ \r\n]*\(.*\)", replace_with_spaces, content)
-        content = re.sub(r"asm[ \r\n]*\(.*\)", replace_with_spaces, content)
-        content = re.sub(
-            r"__extension__[ \r\n]*\(.*\)", replace_with_zero_padded, content
-        )
-        content = re.sub(r"__extension__", replace_with_spaces, content)
-        content = re.sub(r"__inline", replace_with_spaces, content)
-        content = re.sub(r"__restrict", replace_with_spaces, content)
-        content = re.sub(r"__builtin_va_list", "int              ", content)
-        content = re.sub(r"__signed__", "  signed  ", content)
-        content = re.sub(
-            r"\([ \r\n]*\{.*}[ \r\n]*\)", replace_with_zero_padded, content
-        )
-    return content
-
-
 def perform_hacks(filename, func):
     with open(filename, "r") as f:
         with tempfile.NamedTemporaryFile(suffix=".c", delete=False) as tmp:
diff --git a/requirements.txt b/requirements.txt
index b5178a97f7..bf06b17729 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1,3 +1,3 @@
-pycparser==2.20
+pycparser==2.22
 networkx==3.4.2
 PyYAML==6.0.2
diff --git a/svcomp.c b/svcomp.c
index 2785042b9c..6fcde0a3bd 100644
--- a/svcomp.c
+++ b/svcomp.c
@@ -47,7 +47,7 @@ static void c2tt_initialize(void) {
     printf("Initialized variables\n");
 }
 
-void yield(int target_value, int threadid) {
+void __concurrentwit2test_yield(int target_value, int threadid) {
     call_once(&c2tt_once, c2tt_initialize);
     mtx_lock(&c2tt_mtx);
 
@@ -66,7 +66,7 @@ void yield(int target_value, int threadid) {
     printf("Resumed thread %d at %d\n", threadid, target_value);
 }
 
-void release(int target_value, int threadid) {
+void __concurrentwit2test_release(int target_value, int threadid) {
     call_once(&c2tt_once, c2tt_initialize);
     mtx_lock(&c2tt_mtx);
     if (atomic_load(&c2tt_global_counter) > target_value) {
diff --git a/tweaks.py b/tweaks.py
index 938b34e4a0..4315d873fc 100644
--- a/tweaks.py
+++ b/tweaks.py
@@ -14,9 +14,25 @@
 limitations under the License.
 """
 
+from pycparser import CParser
 from pycparser.c_ast import FuncDef, Decl, Struct, TypeDecl
 
 
+def declare_schedule_functions(ast):
+    """Add explicit prototypes for the schedule-point functions.
+
+    They are otherwise called without ever being declared in the
+    instrumented file (their definition only exists in svcomp.c, compiled
+    separately), which relies on implicit-function-declaration being
+    tolerated by the compiler.
+    """
+    prototypes = CParser().parse(
+        "void __concurrentwit2test_yield(int, int);\n"
+        "void __concurrentwit2test_release(int, int);\n"
+    ).ext
+    ast.ext[0:0] = prototypes
+
+
 def reach_error(ast):
     for node in ast.ext:
         if isinstance(node, FuncDef) and node.decl.name == "reach_error":
@@ -24,6 +40,7 @@ def reach_error(ast):
             extern_decl = Decl(
                 name=func_name,
                 quals=[],
+                align=[],
                 storage=["extern"],
                 funcspec=[],
                 type=node.decl.type,
diff --git a/witness2ast.py b/witness2ast.py
index 73ed436a6b..04cd8f559d 100644
--- a/witness2ast.py
+++ b/witness2ast.py
@@ -22,15 +22,17 @@
 * steps carrying an ``assumption`` over a ``__VERIFIER_nondet_*()``
   assignment replace the nondeterministic call with the assumed constant;
 * steps where the executing thread changes become *schedule points*: a
-  ``yield(slot, tid)``/``release(slot, tid)`` pair (implemented in
-  ``svcomp.c``) that blocks the thread until all earlier schedule points
-  have been passed, realizing the witness' cross-thread ordering.
+  ``__concurrentwit2test_yield(slot, tid)``/``__concurrentwit2test_release(slot, tid)``
+  pair (implemented in ``svcomp.c``) that blocks the thread until all
+  earlier schedule points have been passed, realizing the witness' cross-thread
+  ordering. The functions are prefixed to avoid accidentally colliding with
+  identifiers in the instrumented program.
 
 For a ``no-data-race`` witness the racing accesses (the ``target``
 waypoints of the final multi-follow segment) are special: they must stay
-unsynchronized, so they share a single slot and only ``yield`` on it --
-a ``release`` between them would create a happens-before edge that hides
-the race from the thread sanitizer.
+unsynchronized, so they share a single slot and only ``__concurrentwit2test_yield``
+on it -- a ``__concurrentwit2test_release`` between them would create a
+happens-before edge that hides the race from the thread sanitizer.
 """
 
 import re
@@ -54,10 +56,11 @@
 from witnessparser import parse_witness, FORMAT_YAML
 
 
-def find_nondet_assignment_on_line(ast, target_line):
+def find_nondet_assignment_on_line(ast, target_line, target_file):
     class LineVisitor(NodeVisitor):
-        def __init__(self, target_line):
+        def __init__(self, target_line, target_file):
             self.target_line = target_line
+            self.target_file = target_file
             self.found = False
             self.statement = None
             self.parent = None
@@ -74,6 +77,7 @@ def visit_Compound(self, node):
                     line = stmt.coord.line
                     if (
                         line >= self.target_line
+                        and stmt.coord.file == self.target_file
                         and type(stmt) == Assignment
                         and type(stmt.rvalue) == FuncCall
                         and "__VERIFIER_nondet" in stmt.rvalue.name.name
@@ -84,7 +88,7 @@ def visit_Compound(self, node):
                         return
                 self.generic_visit(stmt)
 
-    line_visitor = LineVisitor(target_line)
+    line_visitor = LineVisitor(target_line, target_file)
     line_visitor.visit(ast)
 
     if line_visitor.statement:
@@ -93,7 +97,7 @@ def visit_Compound(self, node):
         return None, None
 
 
-def find_last_nondet_assignment_before_line(ast, target_line, varnames):
+def find_last_nondet_assignment_before_line(ast, target_line, varnames, target_file):
     """Find the last `var = __VERIFIER_nondet_*()` with var in `varnames`
     at or before `target_line`."""
 
@@ -105,6 +109,7 @@ def __init__(self):
         def visit_Assignment(self, node):
             if (
                 node.coord
+                and node.coord.file == target_file
                 and self.line < node.coord.line <= target_line
                 and type(node.rvalue) == FuncCall
                 and type(node.rvalue.name) == ID
@@ -120,10 +125,11 @@ def visit_Assignment(self, node):
     return line_visitor.statement
 
 
-def find_first_statement_on_line(ast, target_line):
+def find_first_statement_on_line(ast, target_line, target_file):
     class LineVisitor(NodeVisitor):
-        def __init__(self, target_line):
+        def __init__(self, target_line, target_file):
             self.target_line = target_line
+            self.target_file = target_file
             self.found = False
             self.statement = None
             self.parent = None
@@ -138,14 +144,14 @@ def visit_Compound(self, node):
             for stmt in node.block_items if node.block_items else [node]:
                 if hasattr(stmt, "coord") and stmt.coord:
                     line = stmt.coord.line
-                    if line >= self.target_line:
+                    if line >= self.target_line and stmt.coord.file == self.target_file:
                         self.statement = stmt
                         self.parent = node
                         self.found = True
                         return
                 self.generic_visit(stmt)
 
-    line_visitor = LineVisitor(target_line)
+    line_visitor = LineVisitor(target_line, target_file)
     line_visitor.visit(ast)
 
     if line_visitor.statement:
@@ -185,7 +191,7 @@ def visit_Compound(self, node):
 assumption_pattern = r"([^\s]*)\s*==\s*([^\s]*)"
 
 
-def apply_assumption(ast, line, assumption, anchored_after=False):
+def apply_assumption(ast, line, assumption, target_file, anchored_after=False):
     """Fix the value of a __VERIFIER_nondet_*() assignment near `line`.
 
     If the assumption constrains the assigned variable to a constant
@@ -201,10 +207,10 @@ def apply_assumption(ast, line, assumption, anchored_after=False):
     assumptions = dict(re.findall(assumption_pattern, assumption))
     if anchored_after:
         nondet_assign_node = find_last_nondet_assignment_before_line(
-            ast, line, set(assumptions)
+            ast, line, set(assumptions), target_file
         )
     else:
-        nondet_assign_node, _ = find_nondet_assignment_on_line(ast, line)
+        nondet_assign_node, _ = find_nondet_assignment_on_line(ast, line, target_file)
     if nondet_assign_node is None:
         return
 
@@ -229,16 +235,16 @@ def make_schedule_call(name, slot, threadid):
     )
 
 
-def insert_schedule_point(ast, line, slot, threadid, release=True):
+def insert_schedule_point(ast, line, slot, threadid, target_file, release=True):
     """Instrument the statement at (or first after) `line` as a schedule point.
 
-    A yield(slot, threadid) call before the statement blocks the thread
-    until all earlier schedule points have released their slot; a
-    release(slot, threadid) call afterwards lets the next schedule point
-    proceed. For control statements the release goes to the start of the
-    body/branches (so it happens only once the statement is really being
-    executed), and for a return statement it goes before the statement
-    (code after a return would never run).
+    A __concurrentwit2test_yield(slot, threadid) call before the statement
+    blocks the thread until all earlier schedule points have released their
+    slot; a __concurrentwit2test_release(slot, threadid) call afterwards lets
+    the next schedule point proceed. For control statements the release goes
+    to the start of the body/branches (so it happens only once the statement
+    is really being executed), and for a return statement it goes before the
+    statement (code after a return would never run).
 
     With release=False only the yield is inserted and the slot is not
     consumed; this keeps racing accesses of a data-race witness free of
@@ -246,16 +252,16 @@ def insert_schedule_point(ast, line, slot, threadid, release=True):
 
     Returns the slot the next schedule point should use.
     """
-    statement, parent = find_first_statement_on_line(ast, line)
+    statement, parent = find_first_statement_on_line(ast, line, target_file)
 
-    yield_func = make_schedule_call("yield", slot, threadid)
+    yield_func = make_schedule_call("__concurrentwit2test_yield", slot, threadid)
     first_index = parent.block_items.index(statement)
     parent.block_items.insert(first_index, yield_func)
 
     if not release:
         return slot
 
-    release_func = make_schedule_call("release", slot, threadid)
+    release_func = make_schedule_call("__concurrentwit2test_release", slot, threadid)
     if isinstance(statement, Return):
         parent.block_items.insert(first_index + 1, release_func)
     elif isinstance(statement, Compound):
@@ -287,7 +293,7 @@ def apply_witness(ast, c_file, witnessfile):
         usable_coords = coords and "startline" in coords
         if "assumption" in data and usable_coords:
             apply_assumption(
-                ast, coords["startline"], data["assumption"], anchored_after
+                ast, coords["startline"], data["assumption"], c_file, anchored_after
             )
 
         step_threadid = data["threadId"] if "threadId" in data else threadid
@@ -295,7 +301,7 @@ def apply_witness(ast, c_file, witnessfile):
             threadid = step_threadid
             release = not (witness.data_race and data.get("type") == "target")
             slot = insert_schedule_point(
-                ast, coords["startline"], slot, threadid, release
+                ast, coords["startline"], slot, threadid, c_file, release
             )
 
     return witness
diff --git a/www-demo/Dockerfile b/www-demo/Dockerfile
new file mode 100644
index 0000000000..771cf90d00
--- /dev/null
+++ b/www-demo/Dockerfile
@@ -0,0 +1,63 @@
+# Build context is the ConcurrentWitness2Test repo root (one level up from
+# this file): `docker build -f www-demo/Dockerfile -t cwt-demo .` from there,
+# or `docker build -f Dockerfile -t cwt-demo ..` from inside www-demo/.
+# Nothing under www-demo/ duplicates files tracked elsewhere in this repo or
+# in sv-witnesses -- everything is fetched/copied fresh at build time.
+
+# --- Monaco editor, vendored via npm ---
+FROM node:22-alpine AS monaco
+WORKDIR /build
+RUN npm install monaco-editor@0.55.1 --no-save
+
+# --- Wasmer JS SDK, vendored via npm. Drives a real clang (the "clang/clang"
+# Wasmer registry package, fetched lazily at runtime like Pyodide -- it's
+# ~100MB, too big to vendor here) compiling to wasm32-wasix, then runs the
+# result with real multithreading (Web Workers + SharedArrayBuffer), not a
+# simulation. Used by "Compile & Run" for unreach-call witnesses only. ---
+FROM node:22-alpine AS wasmersdk
+WORKDIR /build
+RUN npm install @wasmer/sdk@0.10.0 --no-save
+
+# --- sv-witnesses' linter + format schemas + examples, straight from GitLab.
+# The concurrency extension (thread_id, memory_model, format 2.2) only
+# exists on this branch -- main is still at format 2.1 and has no
+# thread_id, so the branch is required, not just a source of "nicer"
+# examples. ---
+FROM alpine:3 AS svwitnesses
+RUN apk add --no-cache git
+RUN git clone --depth 1 -b concurrent-sc-violation-witnesses \
+    https://gitlab.com/sosy-lab/benchmarking/sv-witnesses.git /sv-witnesses
+
+# --- pcpp: pure-python C preprocessor, drop-in for `cpp` (no compiler in wasm) ---
+FROM alpine:3 AS pywheels
+RUN apk add --no-cache curl
+WORKDIR /wheels
+RUN curl -sLO https://files.pythonhosted.org/packages/01/ca/ada7f39c5a0977893e0ef809b1617b259b2d76f6382a7abad00dd6d77904/pcpp-1.30-py2.py3-none-any.whl
+
+# --- Assemble the python tree the Pyodide worker fetches as one archive ---
+FROM alpine:3 AS pytree
+RUN apk add --no-cache zip
+WORKDIR /py
+# ConcurrentWitness2Test's own pure-python modules (this repo)
+COPY witnessparser.py witness2ast.py tweaks.py Exceptions.py hacks.py ./cwt/
+COPY headers/ ./cwt/headers/
+COPY www-demo/py/cwt/instrument.py ./cwt/instrument.py
+# sv-witnesses' linter + schemas (clang_ast.py replaced: no libclang in wasm,
+# only used by --strictChecking, which yaml_linter.py already degrades from)
+COPY --from=svwitnesses /sv-witnesses/linter/witnesslint/ ./witnesslint/
+COPY --from=svwitnesses /sv-witnesses/format/schemas/ ./schemas/
+COPY www-demo/py/clang_ast_stub.py ./witnesslint/clang_ast.py
+COPY www-demo/py/shim.py ./shim.py
+RUN find . -name "__pycache__" -type d -exec rm -rf {} + 2>/dev/null; \
+    cd / && zip -rq py.zip py
+
+# --- Final image: nginx serving the static site ---
+FROM nginx:alpine
+COPY www-demo/nginx.conf /etc/nginx/conf.d/default.conf
+COPY www-demo/index.html www-demo/style.css www-demo/app.js www-demo/pyodide-worker.js www-demo/wasmer-run.js /usr/share/nginx/html/
+COPY svcomp.c /usr/share/nginx/html/svcomp.c
+COPY --from=pytree /py.zip /usr/share/nginx/html/py.zip
+COPY --from=monaco /build/node_modules/monaco-editor/min/vs /usr/share/nginx/html/vendor/monaco/vs
+COPY --from=wasmersdk /build/node_modules/@wasmer/sdk/dist /usr/share/nginx/html/vendor/wasmer
+COPY --from=pywheels /wheels/ /usr/share/nginx/html/vendor/pypi/
+EXPOSE 80
diff --git a/www-demo/README.md b/www-demo/README.md
new file mode 100644
index 0000000000..1e8f665129
--- /dev/null
+++ b/www-demo/README.md
@@ -0,0 +1,131 @@
+# www-demo
+
+A fully static, browser-only playground for the sv-witnesses concurrency
+extension: a C editor and a YAML violation-witness editor side by side,
+example programs from a local bundle and live from
+[sv-benchmarks](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks),
+live linting against the real `witnesslint`, and a button that runs the
+real `ConcurrentWitness2Test` instrumentation pipeline — all in-browser via
+[Pyodide](https://pyodide.org), no backend.
+
+Nothing under `www-demo/` duplicates files tracked elsewhere: the
+`Dockerfile` is a multi-stage build that fetches Monaco (npm), `pcpp` (PyPI),
+and the sv-witnesses linter/schemas/examples (`git clone`, branch
+`concurrent-sc-violation-witnesses` — see below) fresh every build, and
+copies `ConcurrentWitness2Test`'s own pure-Python modules straight from the
+repo root. The only files checked in here are genuinely new:
+`index.html`/`style.css`/`app.js`/`pyodide-worker.js`, `Dockerfile`/
+`nginx.conf`, and three small Python entry points (`py/shim.py`,
+`py/clang_ast_stub.py`, `py/cwt/instrument.py`).
+
+## Running locally
+
+```sh
+docker build -f www-demo/Dockerfile -t cwt-demo .   # from the repo root
+docker run --rm -p 8088:80 cwt-demo
+```
+
+(or `docker build -f Dockerfile -t cwt-demo .. && docker run ...` from
+inside `www-demo/`). Open `http://localhost:8088`.
+
+This is also meant to work as a plain static site with no Docker/build step
+at all (e.g. GitHub Pages) — but since the Dockerfile is what assembles
+`vendor/` and `py.zip` at build time, deploying without Docker currently
+means running the equivalent fetch/copy steps yourself (see the Dockerfile)
+before publishing the directory.
+
+## How it works
+
+- **Monaco** provides both editors (vendored from npm at build time).
+- **Pyodide** (loaded from the jsdelivr CDN at runtime — not vendored, see
+  `pyodide-worker.js` for why) runs in a Web Worker and exposes two Python
+  entry points from `py/shim.py`:
+  - `lint(witness_path, program_path)` calls the real `witnesslint`
+    (cloned from `sv-witnesses/linter/` at build time) against files
+    written into Pyodide's virtual filesystem.
+  - `instrument(c_path, witness_path)` mirrors `main.py:translate_to_c`
+    from this project, minus the compile/execute step (no C compiler
+    exists in-browser, and the task is just to show the instrumented
+    source, not run it). It swaps the real `cpp` subprocess for
+    [pcpp](https://github.com/ned14/pcpp), a pure-Python preprocessor —
+    verified byte-for-byte equivalent to the real CLI's output on
+    sv-witnesses' regression examples. "Download instrumented program" bundles the result
+    together with `svcomp.c` (copied from the repo root at build time) and
+    a generated `Makefile` into a hand-rolled, store-only `.zip` (no
+    compression library needed for source-sized files) so the download is
+    immediately buildable with `make && make run`.
+- The sidebar's live sv-benchmarks browser talks directly to the GitLab
+  API (`/repository/tree`, `/repository/files/.../raw`), which sends
+  permissive CORS headers — no proxy needed.
+- **"Compile & Run"** (unreach-call only) compiles the C editor's *current*
+  contents verbatim — not re-instrumented — together with `svcomp.c`,
+  using the [Wasmer JS SDK](https://github.com/wasmerio/wasmer-js)'s real
+  `clang` (the `clang/clang` Wasmer registry package, ~100MB, fetched
+  lazily at runtime like Pyodide, not vendored) targeting `wasm32-wasix`,
+  then runs the result via Wasmer's WASIX runtime with real multithreading
+  (Web Workers + `SharedArrayBuffer`), not a single-threaded simulation.
+  This needs cross-origin isolation (`nginx.conf` sets
+  `Cross-Origin-Opener-Policy`/`Cross-Origin-Embedder-Policy`); every
+  cross-origin resource this app loads already sends a compatible CORS or
+  `Cross-Origin-Resource-Policy` header, so this doesn't break anything
+  else. Gated to `unreach-call` because that's the only property a plain
+  exit code can confirm (`reach_error()` calls `exit(74)`); `no-data-race`
+  would need ThreadSanitizer and `no-overflow` UBSan, neither wired in.
+
+## Why the `concurrent-sc-violation-witnesses` branch
+
+`sv-witnesses`' `main` branch is still at witness format **2.1** and has no
+`thread_id`/`memory_model` support at all — the concurrency extension this
+whole repo is about only exists on the `concurrent-sc-violation-witnesses`
+branch (the one backing [MR
+!108](https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/-/merge_requests/108)).
+The Dockerfile clones that branch specifically; cloning `main` would make
+every witness using `thread_id` fail schema validation. It's also the
+sidebar's default ref for live-browsing `sv-witnesses`' `examples/`
+directory (user-editable via the "Branch/tag" field).
+
+## Known limitations
+
+- `--strictChecking`'s clang-AST cross-check is unavailable (no libclang in
+  wasm); `py/clang_ast_stub.py` is installed over the real
+  `witnesslint/clang_ast.py` and raises, which the linter already catches
+  and degrades gracefully from.
+- Instrumentation only transforms the source; it doesn't compile or run it
+  itself — that's what "Compile & Run" is for (see above), and the CLI
+  (`../start.sh`) remains the option for the other two properties.
+- "Compile & Run"'s *compilation* step was verified directly against the
+  real `clang/clang` Wasmer package (valid wasm output, exit code 0) from
+  a Node script using `@wasmer/sdk`'s Node entrypoint. The *execution*
+  step (and specifically real multithreading) could not be verified the
+  same way: running the compiled module through that same Node entrypoint
+  consistently exited the process early without resolving, in a way that
+  looks like a Node-specific SDK issue rather than anything about the
+  approach itself — Wasmer's threading model targets the browser (Web
+  Workers + `SharedArrayBuffer`), which is also this feature's actual
+  runtime, not Node. This needs real-browser testing to confirm.
+
+## Bugs found and fixed upstream while building this
+
+Two pre-existing `ConcurrentWitness2Test` bugs were blocking the bundled
+sv-witnesses examples and got fixed in the actual source (not just worked
+around here), each reproduced and verified against the real, unmodified
+CLI before and after:
+
+- `hacks()` (now its own module, `../hacks.py`) blanked `//` comments using
+  a paren-balance scanner meant for `__attribute__(...)`-style constructs;
+  a comment containing a balanced parenthesized expression (e.g. `// so
+  'if (x == 1)' is taken`) stopped the blanking early, leaving a stray `'`
+  that failed to lex. Fixed by giving comments their own full-blank
+  callback instead of reusing the paren-aware one.
+- `witness2ast.py`'s line-matching (`find_first_statement_on_line` and
+  friends) searched the *entire* AST for the first statement at or past a
+  target line, ignoring which file it came from. For a raw `.c` file with
+  `#include`d headers, if the witness's target line was smaller than some
+  header-injected function body's line (headers restart line numbering
+  from 1), instrumentation silently attached to the wrong statement
+  instead. Fixed by threading the witness's own `c_file` through those
+  functions and requiring `node.coord.file == c_file` — pycparser already
+  tracks per-node origin file correctly via the preprocessor's `#line`
+  markers, so this is a strict improvement with no behavioral change for
+  the previously-working cases (verified byte-identical output on the
+  existing examples before/after).
diff --git a/www-demo/app.js b/www-demo/app.js
new file mode 100644
index 0000000000..79793aa745
--- /dev/null
+++ b/www-demo/app.js
@@ -0,0 +1,951 @@
+// Wires the two Monaco editors, the live example sidebar (sv-witnesses
+// examples + sv-benchmarks, both via the GitLab API) and the Pyodide
+// worker (live linting, one-shot instrumentation).
+
+const GITLAB_PROJECT = "sosy-lab%2Fbenchmarking%2Fsv-benchmarks";
+const GITLAB_API = `https://gitlab.com/api/v4/projects/${GITLAB_PROJECT}`;
+
+const SV_WITNESSES_PROJECT = "sosy-lab%2Fbenchmarking%2Fsv-witnesses";
+const SV_WITNESSES_API = `https://gitlab.com/api/v4/projects/${SV_WITNESSES_PROJECT}`;
+
+// Both refs are user-editable via the sidebar's "Branch/tag" inputs --
+// "concurrent-sc-violation-witnesses" is just the default, since examples/
+// on sv-witnesses' main only has format-2.1-and-earlier witnesses.
+function getSvBenchmarksRef() {
+  const input = document.getElementById("sv-benchmarks-ref");
+  return (input && input.value.trim()) || "main";
+}
+
+function getSvWitnessesRef() {
+  const input = document.getElementById("sv-witnesses-ref");
+  return (input && input.value.trim()) || "concurrent-sc-violation-witnesses";
+}
+
+// Fallback text if the live fetch from sv-benchmarks' c/properties/*.prp
+// fails (offline, rate-limited, etc.) -- kept in sync with the real files.
+const SPEC_FALLBACK = {
+  "unreach-call": "CHECK( init(main()), LTL(G ! call(reach_error())) )",
+  "no-data-race": "CHECK( init(main()), LTL(G ! data-race) )",
+  "no-overflow": "CHECK( init(main()), LTL(G ! overflow) )",
+};
+const specTextCache = new Map();
+
+async function getSpecificationText(property) {
+  if (specTextCache.has(property)) return specTextCache.get(property);
+  try {
+    const url = `${GITLAB_API}/repository/files/${encodeURIComponent(
+      `c/properties/${property}.prp`
+    )}/raw?ref=${getSvBenchmarksRef()}`;
+    const resp = await fetch(url);
+    if (!resp.ok) throw new Error(`HTTP ${resp.status}`);
+    const text = (await resp.text()).trim();
+    specTextCache.set(property, text);
+    return text;
+  } catch (err) {
+    return SPEC_FALLBACK[property] || property;
+  }
+}
+
+const outputPanels = {
+  linter: document.getElementById("output-linter"),
+  instrument: document.getElementById("output-instrument"),
+  clang: document.getElementById("output-clang"),
+};
+const outputPanel = document.getElementById("output-panel");
+const outputResizer = document.getElementById("output-resizer");
+const outputToggleBtn = document.getElementById("output-toggle");
+const lintStatus = document.getElementById("lint-status");
+const pyodideStatus = document.getElementById("pyodide-status");
+const instrumentBtn = document.getElementById("instrument-btn");
+const instrumentCaret = document.getElementById("instrument-caret");
+const instrumentMenu = document.getElementById("instrument-menu");
+const cFilename = document.getElementById("c-filename");
+const cursorPos = document.getElementById("cursor-pos");
+const specSelect = document.getElementById("spec-select");
+const addWaypointBtn = document.getElementById("add-waypoint-btn");
+const compileRunBtn = document.getElementById("compile-run-btn");
+
+function setStatus(el, cls, text) {
+  el.className = `status status-${cls}`;
+  el.textContent = text;
+}
+
+// Output panel: only auto-opens on its own; once the user explicitly hides
+// it, it stays hidden even as new output comes in (they can still re-open).
+let outputHiddenByUser = false;
+
+// panel is one of "linter" | "instrument" | "clang", matching the three
+// output sources (the linter, ConcurrentWitness2Test's instrumentation
+// pipeline, and clang/Compile & Run).
+function logOutput(panel, text) {
+  outputPanels[panel].textContent = text;
+  if (!outputHiddenByUser) {
+    outputPanel.classList.remove("collapsed");
+    outputResizer.classList.remove("collapsed");
+  }
+}
+
+function setOutputCollapsed(collapsed) {
+  outputHiddenByUser = collapsed;
+  outputPanel.classList.toggle("collapsed", collapsed);
+  outputResizer.classList.toggle("collapsed", collapsed);
+  outputToggleBtn.textContent = collapsed ? "Show" : "Hide";
+}
+
+outputToggleBtn.addEventListener("click", () => {
+  setOutputCollapsed(!outputPanel.classList.contains("collapsed"));
+});
+for (const btn of document.querySelectorAll(".output-clear-btn")) {
+  btn.addEventListener("click", () => {
+    outputPanels[btn.dataset.target].textContent = "";
+  });
+}
+
+// ---------------------------------------------------------------------------
+// Resizable panels
+// ---------------------------------------------------------------------------
+
+function makeResizer(resizerEl, { axis, min, max, getSize, setSize, invert = false }) {
+  resizerEl.addEventListener("mousedown", (downEvent) => {
+    downEvent.preventDefault();
+    const start = axis === "x" ? downEvent.clientX : downEvent.clientY;
+    const startSize = getSize();
+    document.body.classList.add(axis === "x" ? "resizing-h" : "resizing-v");
+
+    function onMove(moveEvent) {
+      const cur = axis === "x" ? moveEvent.clientX : moveEvent.clientY;
+      const delta = invert ? start - cur : cur - start;
+      const next = Math.min(max(), Math.max(min(), startSize + delta));
+      setSize(next);
+    }
+    function onUp() {
+      document.removeEventListener("mousemove", onMove);
+      document.removeEventListener("mouseup", onUp);
+      document.body.classList.remove("resizing-h", "resizing-v");
+    }
+    document.addEventListener("mousemove", onMove);
+    document.addEventListener("mouseup", onUp);
+  });
+}
+
+const sidebarEl = document.getElementById("sidebar");
+const editorsEl = document.getElementById("editors");
+const cPaneEl = document.getElementById("c-pane");
+
+makeResizer(document.getElementById("sidebar-resizer"), {
+  axis: "x",
+  min: () => 160,
+  max: () => 600,
+  getSize: () => sidebarEl.getBoundingClientRect().width,
+  setSize: (w) => {
+    sidebarEl.style.width = `${w}px`;
+  },
+});
+
+makeResizer(document.getElementById("pane-resizer"), {
+  axis: "x",
+  min: () => 240,
+  max: () => editorsEl.getBoundingClientRect().width - 240,
+  getSize: () => cPaneEl.getBoundingClientRect().width,
+  setSize: (w) => {
+    cPaneEl.style.flex = `0 0 ${w}px`;
+  },
+});
+
+makeResizer(outputResizer, {
+  axis: "y",
+  invert: true, // the resizer sits above the panel, so dragging up (cursor
+  // moving to smaller clientY) must grow it, not shrink it
+  min: () => 80,
+  max: () => window.innerHeight - 160,
+  getSize: () => outputPanel.getBoundingClientRect().height,
+  setSize: (h) => {
+    outputPanel.style.height = `${h}px`;
+  },
+});
+
+// ---------------------------------------------------------------------------
+// Sidebar collapse (hamburger toggle in the top bar)
+// ---------------------------------------------------------------------------
+
+const sidebarHamburgerBtn = document.getElementById("sidebar-hamburger");
+
+// The collapsed flag lives on <body> (not #layout) so the hamburger icon
+// itself -- which sits in the topbar, a sibling of #layout -- can also be
+// styled off it with a plain CSS selector.
+sidebarHamburgerBtn.addEventListener("click", () => {
+  document.body.classList.toggle("sidebar-collapsed");
+});
+
+// ---------------------------------------------------------------------------
+// Dark/light theme toggle
+// ---------------------------------------------------------------------------
+
+const themeToggleBtn = document.getElementById("theme-toggle");
+
+function getTheme() {
+  return document.documentElement.dataset.theme === "light" ? "light" : "dark";
+}
+
+function getMonacoTheme() {
+  return getTheme() === "light" ? "vs" : "vs-dark";
+}
+
+function applyTheme(theme) {
+  document.documentElement.dataset.theme = theme;
+  localStorage.setItem("cwt-theme", theme);
+  themeToggleBtn.textContent = theme === "light" ? "☼" : "☽"; // sun / moon-ish glyph
+  if (window.monaco) monaco.editor.setTheme(getMonacoTheme());
+}
+
+themeToggleBtn.addEventListener("click", () => {
+  applyTheme(getTheme() === "light" ? "dark" : "light");
+});
+
+applyTheme(getTheme()); // sync the button glyph with the theme set by index.html's inline script
+
+// ---------------------------------------------------------------------------
+// Monaco setup
+// ---------------------------------------------------------------------------
+
+let cEditor, yamlEditor;
+let editorsReady = false;
+let pyodideReady = false;
+
+function updateInstrumentButton() {
+  const ready = editorsReady && pyodideReady;
+  instrumentBtn.disabled = !ready;
+  instrumentCaret.disabled = !ready;
+}
+
+// Compile & Run doesn't need Pyodide at all (it's a real clang/WASIX
+// pipeline, independent of the linting/instrumentation worker) -- only
+// gated on the editors existing and unreach-call being selected, since
+// that's the only property whose violation a plain compile+run (exit code
+// 74 from reach_error()) can confirm; no-data-race needs ThreadSanitizer
+// and no-overflow needs UBSan, neither of which is wired in here.
+function updateCompileRunButton() {
+  compileRunBtn.disabled = !editorsReady || specSelect.value !== "unreach-call";
+}
+
+const monacoReady = new Promise((resolve) => {
+  require.config({ paths: { vs: "vendor/monaco/vs" } });
+  require(["vs/editor/editor.main"], () => resolve());
+});
+
+// Before anything is picked from the sidebar, behave as if a fresh
+// "temp.c" was opened: a minimal program in the C editor, and the witness
+// editor pre-filled exactly as it would be for any other freshly loaded
+// program (auto-filled metadata, empty content list).
+const DEFAULT_C_FILENAME = "temp.c";
+const DEFAULT_C_CONTENT = `int main(void) {
+    return 0;
+}
+`;
+
+async function initEditors() {
+  await monacoReady;
+  cEditor = monaco.editor.create(document.getElementById("c-editor"), {
+    language: "c",
+    theme: getMonacoTheme(),
+    automaticLayout: true,
+    value: DEFAULT_C_CONTENT,
+    minimap: { enabled: false },
+  });
+  cFilename.textContent = DEFAULT_C_FILENAME;
+  yamlEditor = monaco.editor.create(document.getElementById("yaml-editor"), {
+    language: "yaml",
+    theme: getMonacoTheme(),
+    automaticLayout: true,
+    value: "",
+    minimap: { enabled: false },
+  });
+
+  cEditor.onDidChangeCursorPosition((e) => {
+    cursorPos.textContent = `Ln ${e.position.lineNumber}, Col ${e.position.column}`;
+  });
+  cEditor.onDidChangeModelContent(debounce(updateScheduleDecorations, 200));
+
+  cEditor.addAction({
+    id: "cwt.addWaypointAtCursor",
+    label: "Add witness waypoint at cursor",
+    contextMenuGroupId: "navigation",
+    contextMenuOrder: 1.5,
+    run: () => addWaypointAtCursor(),
+  });
+
+  yamlEditor.onDidChangeModelContent(debounce(runLint, 400));
+  addWaypointBtn.addEventListener("click", () => addWaypointAtCursor());
+
+  yamlEditor.setValue(
+    await buildWitnessSkeleton(DEFAULT_C_FILENAME, DEFAULT_C_CONTENT, specSelect.value)
+  );
+
+  editorsReady = true;
+  updateInstrumentButton();
+  updateCompileRunButton();
+}
+
+function debounce(fn, ms) {
+  let t = null;
+  return (...args) => {
+    clearTimeout(t);
+    t = setTimeout(() => fn(...args), ms);
+  };
+}
+
+// ---------------------------------------------------------------------------
+// __concurrentwit2test_yield()/__concurrentwit2test_release() decorations
+// ---------------------------------------------------------------------------
+
+let scheduleDecorations = [];
+
+function updateScheduleDecorations() {
+  if (!cEditor) return;
+  const model = cEditor.getModel();
+  const decorations = [];
+  const lineCount = model.getLineCount();
+  for (let line = 1; line <= lineCount; line++) {
+    const text = model.getLineContent(line);
+    const re = /\b(__concurrentwit2test_yield|__concurrentwit2test_release)\s*\([^)]*\)/g;
+    let match;
+    while ((match = re.exec(text))) {
+      decorations.push({
+        range: new monaco.Range(line, match.index + 1, line, match.index + 1 + match[0].length),
+        options: {
+          inlineClassName: match[1] === "__concurrentwit2test_yield" ? "cwt-yield-call" : "cwt-release-call",
+        },
+      });
+    }
+  }
+  scheduleDecorations = model.deltaDecorations(scheduleDecorations, decorations);
+}
+
+// ---------------------------------------------------------------------------
+// Witness metadata skeleton
+// ---------------------------------------------------------------------------
+
+async function sha256Hex(text) {
+  const bytes = new TextEncoder().encode(text);
+  const digest = await crypto.subtle.digest("SHA-256", bytes);
+  return Array.from(new Uint8Array(digest))
+    .map((b) => b.toString(16).padStart(2, "0"))
+    .join("");
+}
+
+async function buildWitnessSkeleton(filename, programText, property) {
+  const hash = await sha256Hex(programText);
+  const uuid = crypto.randomUUID();
+  const creationTime = new Date().toISOString().replace(/\.\d+Z$/, "Z");
+  const specification = await getSpecificationText(property);
+  return `# Auto-filled metadata (format 2.2). Please edit as needed.
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.2"
+    uuid: "${uuid}"
+    creation_time: "${creationTime}"
+    producer:
+      name: "www-demo playground"
+      version: "1.0"
+    task:
+      input_files:
+        - "${filename}"
+      input_file_hashes:
+        "${filename}": "${hash}"
+      specification: "${specification}"
+      data_model: "ILP32"
+      language: "C"
+  content: []
+`;
+}
+
+specSelect.addEventListener("change", async () => {
+  updateCompileRunButton();
+  if (!yamlEditor) return;
+  const specification = await getSpecificationText(specSelect.value);
+  const yaml = yamlEditor.getValue();
+  const updated = yaml.replace(
+    /specification:\s*".*"/,
+    `specification: "${specification.replace(/"/g, '\\"')}"`
+  );
+  if (updated !== yaml) yamlEditor.setValue(updated);
+});
+
+// ---------------------------------------------------------------------------
+// Add witness waypoint at cursor (placeholder scaffold)
+// ---------------------------------------------------------------------------
+
+function addWaypointAtCursor() {
+  if (!cEditor || !yamlEditor) return;
+  const pos = cEditor.getPosition();
+  if (!pos) return;
+  const filename = cFilename.textContent || "input.c";
+  const block = `  - segment:
+    - waypoint:
+        type: assumption # TODO: assumption | target | function_enter | function_return | branching
+        action: follow
+        thread_id: 0 # TODO: 0 = main thread, k = k-th spawned thread
+        constraint: # TODO: only valid for assumption/function_return waypoints
+          value: "TODO" # e.g. "x == 1"
+          format: c_expression
+        location:
+          file_name: "${filename}"
+          line: ${pos.lineNumber}
+          column: ${pos.column}
+          function: "TODO"
+`;
+  let yaml = yamlEditor.getValue();
+  yaml = yaml.replace(/content:\s*\[\]\s*$/m, "content:");
+  if (!yaml.endsWith("\n")) yaml += "\n";
+  const insertLine = yaml.split("\n").length; // 1-indexed line the block will start on
+  yaml += block;
+  yamlEditor.setValue(yaml);
+  yamlEditor.revealLineInCenter(insertLine);
+  yamlEditor.setPosition({ lineNumber: insertLine, column: 1 });
+  yamlEditor.focus();
+}
+
+// ---------------------------------------------------------------------------
+// Pyodide worker
+// ---------------------------------------------------------------------------
+
+const worker = new Worker("pyodide-worker.js");
+let workerReady = false;
+let nextRequestId = 1;
+const pending = new Map();
+
+// Without this, a worker-startup failure (e.g. a blocked cross-origin
+// subresource) shows up only as the page silently never leaving "Loading
+// Python runtime..." -- no console output, since errors *inside* a worker
+// don't otherwise surface on the main thread.
+worker.onerror = (event) => {
+  setStatus(pyodideStatus, "err", "Python runtime failed to load");
+  const msg = `Pyodide worker failed to start:\n${event.message || event}`;
+  logOutput("linter", msg);
+  logOutput("instrument", msg);
+};
+
+worker.onmessage = (event) => {
+  const data = event.data;
+  if (data.cmd === "ready") {
+    workerReady = true;
+    pyodideReady = true;
+    setStatus(pyodideStatus, "ok", "Python runtime ready");
+    updateInstrumentButton();
+    runLint();
+    return;
+  }
+  if (data.cmd === "error" && data.id === undefined) {
+    setStatus(pyodideStatus, "err", "Python runtime failed to load");
+    const msg = `Pyodide failed to initialize:\n${data.error}`;
+    logOutput("linter", msg);
+    logOutput("instrument", msg);
+    return;
+  }
+  const resolver = pending.get(data.id);
+  if (resolver) {
+    pending.delete(data.id);
+    resolver(data);
+  }
+};
+
+function callWorker(cmd, payload) {
+  const id = nextRequestId++;
+  return new Promise((resolve) => {
+    pending.set(id, resolve);
+    worker.postMessage({ id, cmd, ...payload });
+  });
+}
+
+async function runLint() {
+  if (!workerReady || !yamlEditor) return;
+  setStatus(lintStatus, "loading", "Lint: running…");
+  const yaml = yamlEditor.getValue();
+  const c = cEditor ? cEditor.getValue() : null;
+  const response = await callWorker("lint", { yaml, c });
+  if (!response.ok) {
+    setStatus(lintStatus, "err", "Lint: error");
+    logOutput("linter", `Linter failed to run:\n${response.error}`);
+    return;
+  }
+  const { exit_code, output } = response.result;
+  if (exit_code === 0) {
+    setStatus(lintStatus, "ok", "Lint: valid");
+  } else {
+    setStatus(lintStatus, "warn", `Lint: exit ${exit_code}`);
+  }
+  logOutput("linter", output);
+}
+
+async function runInstrumentPipeline() {
+  const c = cEditor.getValue();
+  const yaml = yamlEditor.getValue();
+  const response = await callWorker("instrument", { c, yaml });
+  if (!response.ok) {
+    logOutput("instrument", `Instrumentation failed to run:\n${response.error}`);
+    return null;
+  }
+  const { ok, source, error, log, data_race } = response.result;
+  if (!ok) {
+    logOutput("instrument", `Instrumentation failed:\n${error}\n${log || ""}`);
+    return null;
+  }
+  logOutput(
+    "instrument",
+    `Instrumented successfully${data_race ? " (data-race witness: compile with -fsanitize=thread)" : ""}.`
+  );
+  return { source, dataRace: !!data_race };
+}
+
+// ---------------------------------------------------------------------------
+// "Download instrumented program": bundles instrumented.c + the project's
+// svcomp.c scheduler/stub harness + a Makefile into a .zip (hand-rolled,
+// store-only -- no compression library needed for source-sized files).
+// ---------------------------------------------------------------------------
+
+let svcompSourceCache = null;
+
+async function getSvcompSource() {
+  if (svcompSourceCache === null) {
+    const resp = await fetch("svcomp.c");
+    svcompSourceCache = await resp.text();
+  }
+  return svcompSourceCache;
+}
+
+function buildMakefile(dataRace) {
+  const extraFlags = dataRace ? " -fsanitize=thread -g" : "";
+  const runCmd = dataRace
+    ? 'TSAN_OPTIONS="halt_on_error=1 exitcode=74" ./$(TARGET)'
+    : "./$(TARGET)";
+  return `CC ?= gcc
+CFLAGS ?= -w -Wno-implicit-function-declaration -pthread${extraFlags}
+TARGET ?= a.out
+SRCS = instrumented.c svcomp.c
+
+.PHONY: all run clean
+
+all: $(TARGET)
+
+$(TARGET): $(SRCS)
+	$(CC) $(CFLAGS) $(SRCS) -o $(TARGET)
+
+run: $(TARGET)
+	${runCmd}
+
+clean:
+	rm -f $(TARGET)
+`;
+}
+
+function crc32(bytes) {
+  let crc = ~0;
+  for (let i = 0; i < bytes.length; i++) {
+    crc ^= bytes[i];
+    for (let j = 0; j < 8; j++) {
+      crc = (crc >>> 1) ^ (0xedb88320 & -(crc & 1));
+    }
+  }
+  return ~crc >>> 0;
+}
+
+// Minimal store-only (uncompressed) ZIP writer: local file headers + central
+// directory + end record, per the ZIP spec. Verified against `unzip` while
+// building this.
+function makeZip(files) {
+  const localParts = [];
+  const centralParts = [];
+  const records = [];
+  let offset = 0;
+
+  for (const f of files) {
+    const nameBytes = f.nameBytes;
+    const data = f.data;
+    const crc = crc32(data);
+    const size = data.length;
+
+    const local = new DataView(new ArrayBuffer(30));
+    local.setUint32(0, 0x04034b50, true);
+    local.setUint16(4, 20, true);
+    local.setUint16(6, 0, true);
+    local.setUint16(8, 0, true);
+    local.setUint16(10, 0, true);
+    local.setUint16(12, 0x21, true); // DOS date 1980-01-01; time unused
+    local.setUint32(14, crc, true);
+    local.setUint32(18, size, true);
+    local.setUint32(22, size, true);
+    local.setUint16(26, nameBytes.length, true);
+    local.setUint16(28, 0, true);
+    const localBytes = new Uint8Array(local.buffer);
+
+    localParts.push(localBytes, nameBytes, data);
+    records.push({ nameBytes, crc, size, offset });
+    offset += localBytes.length + nameBytes.length + data.length;
+  }
+
+  const centralOffset = offset;
+  for (const rec of records) {
+    const central = new DataView(new ArrayBuffer(46));
+    central.setUint32(0, 0x02014b50, true);
+    central.setUint16(4, 20, true);
+    central.setUint16(6, 20, true);
+    central.setUint16(8, 0, true);
+    central.setUint16(10, 0, true);
+    central.setUint16(12, 0, true);
+    central.setUint16(14, 0x21, true);
+    central.setUint32(16, rec.crc, true);
+    central.setUint32(20, rec.size, true);
+    central.setUint32(24, rec.size, true);
+    central.setUint16(28, rec.nameBytes.length, true);
+    central.setUint16(30, 0, true);
+    central.setUint16(32, 0, true);
+    central.setUint16(34, 0, true);
+    central.setUint16(36, 0, true);
+    central.setUint32(38, 0, true);
+    central.setUint32(42, rec.offset, true);
+    centralParts.push(new Uint8Array(central.buffer), rec.nameBytes);
+    offset += 46 + rec.nameBytes.length;
+  }
+  const centralSize = offset - centralOffset;
+
+  const end = new DataView(new ArrayBuffer(22));
+  end.setUint32(0, 0x06054b50, true);
+  end.setUint16(4, 0, true);
+  end.setUint16(6, 0, true);
+  end.setUint16(8, records.length, true);
+  end.setUint16(10, records.length, true);
+  end.setUint32(12, centralSize, true);
+  end.setUint32(16, centralOffset, true);
+  end.setUint16(20, 0, true);
+
+  return new Blob([...localParts, ...centralParts, new Uint8Array(end.buffer)], {
+    type: "application/zip",
+  });
+}
+
+function makeZipFromTexts(textFiles) {
+  const encoder = new TextEncoder();
+  return makeZip(
+    textFiles.map((f) => ({ nameBytes: encoder.encode(f.name), data: encoder.encode(f.content) }))
+  );
+}
+
+function downloadBlob(filename, blob) {
+  const url = URL.createObjectURL(blob);
+  const a = document.createElement("a");
+  a.href = url;
+  a.download = filename;
+  a.click();
+  URL.revokeObjectURL(url);
+}
+
+let instrumentMode = "inplace";
+
+async function runInstrument(mode) {
+  if (!workerReady || !cEditor || !yamlEditor) return;
+  instrumentBtn.disabled = true;
+  instrumentCaret.disabled = true;
+  const originalLabel = instrumentBtn.textContent;
+  instrumentBtn.textContent = "Instrumenting…";
+  try {
+    const result = await runInstrumentPipeline();
+    if (result === null) return;
+    const { source, dataRace } = result;
+    if (mode === "download") {
+      const svcompSource = await getSvcompSource();
+      const zipBlob = makeZipFromTexts([
+        { name: "instrumented.c", content: source },
+        { name: "svcomp.c", content: svcompSource },
+        { name: "Makefile", content: buildMakefile(dataRace) },
+      ]);
+      const name = (cFilename.textContent || "instrumented").replace(/\.[ci]$/, "") + "-bundle.zip";
+      downloadBlob(name, zipBlob);
+    } else {
+      cEditor.setValue(source);
+    }
+  } finally {
+    instrumentBtn.disabled = false;
+    instrumentCaret.disabled = false;
+    instrumentBtn.textContent = originalLabel;
+  }
+}
+
+instrumentBtn.addEventListener("click", () => runInstrument(instrumentMode));
+instrumentCaret.addEventListener("click", (e) => {
+  e.stopPropagation();
+  instrumentMenu.hidden = !instrumentMenu.hidden;
+});
+document.addEventListener("click", (e) => {
+  if (!instrumentMenu.hidden && !e.target.closest("#instrument-split")) {
+    instrumentMenu.hidden = true;
+  }
+});
+for (const item of instrumentMenu.querySelectorAll("button[data-mode]")) {
+  item.addEventListener("click", () => {
+    instrumentMode = item.dataset.mode;
+    instrumentBtn.textContent = item.dataset.mode === "download" ? "Download instrumented program" : "Instrument in-place";
+    instrumentMenu.hidden = true;
+  });
+}
+
+// ---------------------------------------------------------------------------
+// Compile & Run: takes the C editor's *current* contents verbatim (no
+// re-instrumentation -- whatever's in the editor, instrumented or not, is
+// what gets compiled) and runs it for real via clang/WASIX, with actual
+// multithreading (Web Workers + SharedArrayBuffer), not a simulation.
+// ---------------------------------------------------------------------------
+
+compileRunBtn.addEventListener("click", async () => {
+  if (compileRunBtn.disabled || !cEditor) return;
+  const originalLabel = compileRunBtn.textContent;
+  compileRunBtn.disabled = true;
+  try {
+    const { compileAndRun } = await import("./wasmer-run.js");
+    const cSource = cEditor.getValue();
+    const svcompSource = await getSvcompSource();
+    const result = await compileAndRun(cSource, svcompSource, (status) => {
+      compileRunBtn.textContent = status;
+      logOutput("clang", status);
+    });
+
+    if (result.stage === "compile") {
+      logOutput(
+        "clang",
+        `Compilation failed (exit code ${result.code}):\n\n${result.stderr || result.stdout || "(no output)"}`
+      );
+      return;
+    }
+
+    let verdict;
+    if (result.code === 74) {
+      verdict = "Property VIOLATED: reach_error() was called (exit code 74) -- the witness's execution was reproduced.";
+    } else {
+      verdict = `Program exited with code ${result.code} without calling reach_error() -- this run did not reproduce the witness's violation.`;
+    }
+    logOutput(
+      "clang",
+      `${verdict}\n\n--- stdout ---\n${result.stdout || "(empty)"}\n--- stderr ---\n${result.stderr || "(empty)"}`
+    );
+  } catch (err) {
+    logOutput("clang", `Compile & Run failed:\n${err && err.stack ? err.stack : err}`);
+  } finally {
+    compileRunBtn.textContent = originalLabel;
+    updateCompileRunButton();
+  }
+});
+
+// ---------------------------------------------------------------------------
+// Sidebar: live sv-benchmarks browser (GitLab API)
+// ---------------------------------------------------------------------------
+
+async function fetchCategoryEntries(category) {
+  const path = encodeURIComponent(`c/${category}`);
+  const url = `${GITLAB_API}/repository/tree?path=${path}&ref=${getSvBenchmarksRef()}&per_page=100`;
+  const resp = await fetch(url);
+  if (!resp.ok) throw new Error(`GitLab API returned ${resp.status}`);
+  const entries = await resp.json();
+  return entries
+    .filter((e) => e.type === "blob" && e.name.endsWith(".yml"))
+    .sort((a, b) => a.name.localeCompare(b.name));
+}
+
+async function fetchRawFile(category, filename) {
+  const encodedPath = encodeURIComponent(`c/${category}/${filename}`);
+  const url = `${GITLAB_API}/repository/files/${encodedPath}/raw?ref=${getSvBenchmarksRef()}`;
+  const resp = await fetch(url);
+  if (!resp.ok) throw new Error(`GitLab API returned ${resp.status}`);
+  return resp.text();
+}
+
+// SV-COMP task .yml files declare their program(s) as a scalar
+// (`input_files: 'foo.c'`), a flow sequence (`input_files: [foo.c]`), or a
+// block sequence (`input_files:\n  - foo.c`). We only need the first.
+function extractFirstInputFile(taskYaml) {
+  // Scalar or flow-sequence form, kept on input_files:'s own line.
+  let m = taskYaml.match(/input_files:[ \t]*\[?[ \t]*['"]?([^'",\]\s][^'",\]\n]*)/);
+  if (m) return m[1].trim();
+  // Block-sequence form: the value is on the following line(s).
+  m = taskYaml.match(/input_files:\s*\n\s*-\s*['"]?([^'",\]\s]+)/);
+  return m ? m[1] : null;
+}
+
+async function loadSvBenchmarkEntry(category, entry) {
+  const taskYaml = await fetchRawFile(category, entry.name);
+  const programName = extractFirstInputFile(taskYaml);
+  if (!programName) {
+    throw new Error(`Could not find input_files in ${entry.name}`);
+  }
+  const text = await fetchRawFile(category, programName);
+  cEditor.setValue(text);
+  cFilename.textContent = programName;
+  yamlEditor.setValue(await buildWitnessSkeleton(programName, text, specSelect.value));
+}
+
+async function fetchAllSvBenchmarksCategories() {
+  const categories = [];
+  let page = 1;
+  for (;;) {
+    const url = `${GITLAB_API}/repository/tree?path=c&ref=${getSvBenchmarksRef()}&per_page=100&page=${page}`;
+    const resp = await fetch(url);
+    if (!resp.ok) throw new Error(`GitLab API returned ${resp.status}`);
+    const entries = await resp.json();
+    categories.push(...entries.filter((e) => e.type === "tree").map((e) => e.name));
+    const totalPages = parseInt(resp.headers.get("x-total-pages") || "1", 10);
+    if (entries.length === 0 || page >= totalPages) break;
+    page++;
+  }
+  return categories.sort((a, b) => a.localeCompare(b));
+}
+
+async function renderSvBenchmarksCategories() {
+  const list = document.getElementById("sv-benchmarks-categories");
+  list.innerHTML = '<li class="loading">Loading categories&hellip;</li>';
+  let categories;
+  try {
+    categories = await fetchAllSvBenchmarksCategories();
+  } catch (err) {
+    list.innerHTML = "";
+    const errLi = document.createElement("li");
+    errLi.className = "empty";
+    errLi.textContent = `Failed to list categories: ${err.message}`;
+    list.appendChild(errLi);
+    return;
+  }
+  list.innerHTML = "";
+  for (const category of categories) {
+    const li = document.createElement("li");
+    li.className = "category";
+    li.textContent = `c/${category}`;
+    let expanded = false;
+    let entriesList = null;
+    li.addEventListener("click", async () => {
+      expanded = !expanded;
+      li.classList.toggle("open", expanded);
+      if (!expanded) {
+        if (entriesList) entriesList.remove();
+        entriesList = null;
+        return;
+      }
+      entriesList = document.createElement("ul");
+      entriesList.className = "example-list";
+      const loadingLi = document.createElement("li");
+      loadingLi.className = "loading";
+      loadingLi.textContent = "Loading…";
+      entriesList.appendChild(loadingLi);
+      li.after(entriesList);
+      try {
+        const entries = await fetchCategoryEntries(category);
+        entriesList.innerHTML = "";
+        if (entries.length === 0) {
+          const emptyLi = document.createElement("li");
+          emptyLi.className = "empty";
+          emptyLi.textContent = "(no .yml task files)";
+          entriesList.appendChild(emptyLi);
+        }
+        for (const entry of entries) {
+          const fileLi = document.createElement("li");
+          fileLi.className = "file";
+          fileLi.textContent = entry.name;
+          fileLi.addEventListener("click", (ev) => {
+            ev.stopPropagation();
+            loadSvBenchmarkEntry(category, entry).catch((err) =>
+              logOutput("linter", `Failed to load ${entry.name}:\n${err}`)
+            );
+          });
+          entriesList.appendChild(fileLi);
+        }
+      } catch (err) {
+        entriesList.innerHTML = "";
+        const errLi = document.createElement("li");
+        errLi.className = "empty";
+        errLi.textContent = `Failed to list: ${err.message}`;
+        entriesList.appendChild(errLi);
+      }
+    });
+    list.appendChild(li);
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Sidebar: live sv-witnesses examples browser (GitLab API)
+// ---------------------------------------------------------------------------
+
+async function fetchSvWitnessesExamples() {
+  const url = `${SV_WITNESSES_API}/repository/tree?path=examples&ref=${getSvWitnessesRef()}&per_page=100`;
+  const resp = await fetch(url);
+  if (!resp.ok) throw new Error(`GitLab API returned ${resp.status}`);
+  const entries = await resp.json();
+  return entries
+    .filter((e) => e.type === "blob" && e.name.endsWith(".yml"))
+    .sort((a, b) => a.name.localeCompare(b.name));
+}
+
+async function fetchSvWitnessesRawFile(filename) {
+  const encodedPath = encodeURIComponent(`examples/${filename}`);
+  const url = `${SV_WITNESSES_API}/repository/files/${encodedPath}/raw?ref=${getSvWitnessesRef()}`;
+  const resp = await fetch(url);
+  if (!resp.ok) throw new Error(`GitLab API returned ${resp.status}`);
+  return resp.text();
+}
+
+async function loadSvWitnessExample(entry) {
+  const witnessYaml = await fetchSvWitnessesRawFile(entry.name);
+  const programRef = extractFirstInputFile(witnessYaml);
+  if (!programRef) {
+    throw new Error(`Could not find task.input_files in ${entry.name}`);
+  }
+  // These examples reference siblings within the same examples/ directory,
+  // sometimes as "./foo.c" -- only the basename is ever needed.
+  const programName = programRef.replace(/^\.\//, "").split("/").pop();
+  const programText = await fetchSvWitnessesRawFile(programName);
+  cEditor.setValue(programText);
+  cFilename.textContent = programName;
+  yamlEditor.setValue(witnessYaml);
+}
+
+async function renderSvWitnessesExamples() {
+  const list = document.getElementById("sv-witnesses-examples");
+  list.innerHTML = '<li class="loading">Loading examples&hellip;</li>';
+  let entries;
+  try {
+    entries = await fetchSvWitnessesExamples();
+  } catch (err) {
+    list.innerHTML = "";
+    const errLi = document.createElement("li");
+    errLi.className = "empty";
+    errLi.textContent = `Failed to list examples: ${err.message}`;
+    list.appendChild(errLi);
+    return;
+  }
+  list.innerHTML = "";
+  for (const entry of entries) {
+    const li = document.createElement("li");
+    li.className = "file";
+    li.textContent = entry.name;
+    li.addEventListener("click", () => {
+      loadSvWitnessExample(entry).catch((err) =>
+        logOutput("linter", `Failed to load ${entry.name}:\n${err}`)
+      );
+    });
+    list.appendChild(li);
+  }
+}
+
+// ---------------------------------------------------------------------------
+// Boot
+// ---------------------------------------------------------------------------
+
+function wireRefPicker(inputId, onChange) {
+  const input = document.getElementById(inputId);
+  input.addEventListener("change", onChange);
+  input.addEventListener("keydown", (e) => {
+    if (e.key === "Enter") input.blur(); // triggers the change listener above
+  });
+}
+
+wireRefPicker("sv-witnesses-ref", () => renderSvWitnessesExamples());
+wireRefPicker("sv-benchmarks-ref", () => renderSvBenchmarksCategories());
+
+renderSvWitnessesExamples();
+renderSvBenchmarksCategories();
+initEditors();
diff --git a/www-demo/index.html b/www-demo/index.html
new file mode 100644
index 0000000000..f2e570bdd1
--- /dev/null
+++ b/www-demo/index.html
@@ -0,0 +1,133 @@
+<!doctype html>
+<html lang="en">
+<head>
+<meta charset="utf-8" />
+<meta name="viewport" content="width=device-width, initial-scale=1" />
+<title>ConcurrentWitness2Test / sv-witnesses playground</title>
+<link rel="stylesheet" href="style.css" />
+<script>
+  // Applied before first paint to avoid a flash of the wrong theme.
+  document.documentElement.dataset.theme = localStorage.getItem("cwt-theme") || "dark";
+</script>
+</head>
+<body>
+  <header id="topbar">
+    <div class="topbar-left">
+      <button id="sidebar-hamburger" class="hamburger-btn" title="Toggle sidebar" aria-label="Toggle sidebar">
+        <span></span><span></span><span></span>
+      </button>
+      <h1>Concurrent Violation Witness Playground</h1>
+    </div>
+    <div class="topbar-right">
+      <span id="pyodide-status" class="status status-loading">Loading Python runtime&hellip;</span>
+      <a class="guide-link"
+         href="https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/-/blob/concurrent-sc-violation-witnesses/user-guide/Witness-Format.md"
+         target="_blank" rel="noopener">Witness Format Guide &#8599;</a>
+      <button id="theme-toggle" class="theme-toggle" title="Toggle dark/light mode" aria-label="Toggle dark/light mode">&#9789;</button>
+    </div>
+  </header>
+
+  <div id="layout">
+    <nav id="sidebar">
+      <section>
+        <h2>sv-witnesses examples (live, GitLab)</h2>
+        <p class="hint">All YAML witness examples from
+          <a href="https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/-/tree/concurrent-sc-violation-witnesses/examples" target="_blank" rel="noopener">sv-witnesses</a>'
+          <code>examples/</code> directory. Clicking one loads the witness and
+          resolves its own <code>task.input_files</code> to load the matching program.</p>
+        <div class="ref-picker">
+          <label for="sv-witnesses-ref">Branch/tag:</label>
+          <input type="text" id="sv-witnesses-ref" value="concurrent-sc-violation-witnesses" spellcheck="false" />
+        </div>
+        <ul id="sv-witnesses-examples" class="example-list">
+          <li class="loading">Loading examples&hellip;</li>
+        </ul>
+      </section>
+      <section>
+        <h2>sv-benchmarks (live, GitLab)</h2>
+        <p class="hint">All categories under <code>c/</code> in
+          <a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks" target="_blank" rel="noopener">sv-benchmarks</a>.
+          Lists each category's task (.yml) files; clicking one resolves its
+          <code>input_files</code> and loads that program. No witness exists
+          upstream for these.</p>
+        <div class="ref-picker">
+          <label for="sv-benchmarks-ref">Branch/tag:</label>
+          <input type="text" id="sv-benchmarks-ref" value="main" spellcheck="false" />
+        </div>
+        <ul id="sv-benchmarks-categories" class="example-list">
+          <li class="loading">Loading categories&hellip;</li>
+        </ul>
+      </section>
+    </nav>
+    <div id="sidebar-resizer" class="resizer resizer-v"></div>
+
+    <main id="editors">
+      <div class="pane" id="c-pane">
+        <div class="pane-toolbar">
+          <span class="pane-title">C program</span>
+          <span id="c-filename" class="filename"></span>
+          <span id="cursor-pos" class="cursor-pos">Ln 1, Col 1</span>
+          <button id="add-waypoint-btn" title="Insert a witness waypoint stub at the cursor's line/column (also available via right-click)">+ Waypoint</button>
+          <select id="spec-select" title="Property; changes the witness's task.specification to match">
+            <option value="unreach-call">unreach-call</option>
+            <option value="no-data-race">no-data-race</option>
+            <option value="no-overflow">no-overflow</option>
+          </select>
+          <div class="split-button" id="instrument-split">
+            <button id="instrument-btn" disabled title="Run ConcurrentWitness2Test's instrumentation pipeline in-browser">Instrument in-place</button>
+            <button id="instrument-caret" disabled title="Choose instrument action">&#9662;</button>
+            <div class="split-menu" id="instrument-menu" hidden>
+              <button type="button" data-mode="inplace">Instrument in-place</button>
+              <button type="button" data-mode="download">Download instrumented program</button>
+            </div>
+          </div>
+          <button id="compile-run-btn" disabled title="unreach-call only: compiles the editor's current C source (unmodified) with svcomp.c via clang/WASIX and runs it with real multithreading, in-browser">Compile &amp; Run</button>
+        </div>
+        <div id="c-editor" class="monaco-container"></div>
+      </div>
+      <div id="pane-resizer" class="resizer resizer-v"></div>
+      <div class="pane" id="yaml-pane">
+        <div class="pane-toolbar">
+          <span class="pane-title">Violation witness (YAML 2.2)</span>
+          <span id="lint-status" class="status status-idle">Lint: idle</span>
+        </div>
+        <div id="yaml-editor" class="monaco-container"></div>
+      </div>
+    </main>
+  </div>
+
+  <div id="output-resizer" class="resizer resizer-h"></div>
+  <section id="output-panel">
+    <div class="output-toolbar">
+      <span>Output</span>
+      <button id="output-toggle">Hide</button>
+    </div>
+    <div id="output-panes">
+      <div class="output-pane">
+        <div class="output-pane-header">
+          <span>Linter</span>
+          <button class="output-clear-btn" data-target="linter">Clear</button>
+        </div>
+        <pre class="output-content" id="output-linter"></pre>
+      </div>
+      <div class="output-pane">
+        <div class="output-pane-header">
+          <span>ConcurrentWitness2Test</span>
+          <button class="output-clear-btn" data-target="instrument">Clear</button>
+        </div>
+        <pre class="output-content" id="output-instrument"></pre>
+      </div>
+      <div class="output-pane">
+        <div class="output-pane-header">
+          <span>Clang / Compile &amp; Run</span>
+          <button class="output-clear-btn" data-target="clang">Clear</button>
+        </div>
+        <pre class="output-content" id="output-clang"></pre>
+      </div>
+    </div>
+  </section>
+
+  <script src="vendor/monaco/vs/loader.js"></script>
+  <script type="module" src="app.js"></script>
+</body>
+</html>
diff --git a/www-demo/nginx.conf b/www-demo/nginx.conf
new file mode 100644
index 0000000000..afff8f69a4
--- /dev/null
+++ b/www-demo/nginx.conf
@@ -0,0 +1,42 @@
+server {
+    listen 80;
+    server_name _;
+    root /usr/share/nginx/html;
+    index index.html;
+
+    # Required for the Wasmer SDK's WASIX threads (real multithreading via
+    # Web Workers + SharedArrayBuffer) in "Compile & Run" -- both headers
+    # are needed to make the page cross-origin isolated, which is what
+    # unlocks SharedArrayBuffer. "credentialless" (not "require-corp") is
+    # deliberate: require-corp blocks any cross-origin subresource lacking
+    # a Cross-Origin-Resource-Policy header, and that blocking is often
+    # silent (Network tab only, no Console error) -- it broke Pyodide
+    # loading here even though jsdelivr does send that header for the
+    # files actually checked. credentialless still yields a cross-origin
+    # isolated page without requiring every third-party response to opt in;
+    # none of this app's cross-origin resources need credentials anyway.
+    add_header Cross-Origin-Opener-Policy "same-origin" always;
+    add_header Cross-Origin-Embedder-Policy "credentialless" always;
+
+    location / {
+        try_files $uri $uri/ =404;
+    }
+
+    location /vendor/ {
+        add_header Cache-Control "public, max-age=604800";
+        add_header Cross-Origin-Opener-Policy "same-origin" always;
+        add_header Cross-Origin-Embedder-Policy "credentialless" always;
+    }
+
+    # nginx's bundled mime.types has no .mjs entry (only .js); without this,
+    # the Wasmer SDK's ES module files would be served as
+    # application/octet-stream and rejected by the browser's module loader.
+    # A regex location wins over the /vendor/ prefix location above, so its
+    # headers are repeated here rather than inherited.
+    location ~* \.mjs$ {
+        default_type application/javascript;
+        add_header Cache-Control "public, max-age=604800";
+        add_header Cross-Origin-Opener-Policy "same-origin" always;
+        add_header Cross-Origin-Embedder-Policy "credentialless" always;
+    }
+}
diff --git a/www-demo/py/clang_ast_stub.py b/www-demo/py/clang_ast_stub.py
new file mode 100644
index 0000000000..ba0ffd02f5
--- /dev/null
+++ b/www-demo/py/clang_ast_stub.py
@@ -0,0 +1,11 @@
+# Stubbed for the browser/Pyodide build: no libclang is available in-wasm.
+# witnesslint/yaml_linter/yaml_linter.py already wraps the one call site
+# (get_stmt_locations_from_source, used only by --strictChecking) in a
+# try/except that logs a warning and continues with ast_nodes=None, so this
+# stub simply needs to fail loudly without an import-time crash. Installed
+# over the real witnesslint/clang_ast.py at Docker build time.
+def get_stmt_locations_from_source(program):
+    raise NotImplementedError(
+        "clang AST cross-checking (--strictChecking) is not available "
+        "in the browser build of witnesslint."
+    )
diff --git a/www-demo/py/cwt/instrument.py b/www-demo/py/cwt/instrument.py
new file mode 100644
index 0000000000..bf09e755e4
--- /dev/null
+++ b/www-demo/py/cwt/instrument.py
@@ -0,0 +1,61 @@
+"""
+Browser entrypoint mirroring main.py:translate_to_c, minus the gcc
+compile/execute step (out of scope in-browser, no compiler in wasm).
+Swaps the real `cpp` subprocess for pcpp (pure-python C preprocessor),
+which has been verified byte-for-byte equivalent on the bundled examples
+(see www-demo's plan/verification notes).
+"""
+
+import io
+
+from pcpp.preprocessor import Preprocessor
+from pycparser import CParser, c_generator
+
+from tweaks import reach_error, declare_schedule_functions, fix_inline, fix_struct_def
+from witness2ast import apply_witness
+
+# Mirrors main.py's CPP_GNU_COMPAT_ARGS, expressed as pcpp #define bodies
+# instead of `-D` gcc flags.
+CPP_GNU_COMPAT_DEFINES = [
+    "__attribute__(x)",
+    "__extension__",
+    "__restrict",
+    "__restrict__",
+    "__inline inline",
+    "__inline__ inline",
+    "__const const",
+    "__signed__ signed",
+    "__volatile__ volatile",
+    "__typeof__(x) void*",
+    "__builtin_va_list void*",
+]
+
+
+def instrument(c_path: str, witness_path: str, headers_dir: str) -> str:
+    """Reads the C source at c_path (already hacks()-applied and written to
+    the virtual FS by the caller), preprocesses with pcpp, parses with
+    pycparser, applies the witness, regenerates C source. Returns the
+    instrumented source as a string, or raises KnownErrorVerdict / a normal
+    exception on failure (the caller is expected to surface these as text)."""
+    with open(c_path, "r") as f:
+        src = f.read()
+
+    pre = Preprocessor()
+    pre.add_path(headers_dir)
+    for define in CPP_GNU_COMPAT_DEFINES:
+        pre.define(define)
+    pre.parse(src, c_path)
+    out = io.StringIO()
+    pre.write(out)
+    text = out.getvalue()
+
+    ast = CParser().parse(text, c_path)
+    parsed_witness = apply_witness(ast, c_path, witness_path)
+
+    fix_inline(ast)
+    fix_struct_def(ast)
+    reach_error(ast)
+    declare_schedule_functions(ast)
+
+    generator = c_generator.CGenerator()
+    return generator.visit(ast), parsed_witness.data_race
diff --git a/www-demo/py/shim.py b/www-demo/py/shim.py
new file mode 100644
index 0000000000..ada64ab63c
--- /dev/null
+++ b/www-demo/py/shim.py
@@ -0,0 +1,62 @@
+"""
+Entry points called from pyodide-worker.js. Kept dependency-light and
+side-effect-free per call (re-clears witnesslint's module-level logging
+handlers each time, since they're created once and would otherwise pin to
+the first call's redirected stdout/stderr).
+"""
+
+import contextlib
+import io
+import logging
+import sys
+
+sys.path.insert(0, "/py/cwt")
+sys.path.insert(0, "/py")
+
+
+def lint(witness_path: str, program_path: str | None, strict: bool = False) -> dict:
+    from witnesslint import main as witnesslint_main
+
+    for name in ("with_position", "without_position"):
+        logging.getLogger(name).handlers.clear()
+
+    argv = ["--witness", witness_path]
+    if program_path:
+        argv.append(program_path)
+    if strict:
+        argv.append("--strictChecking")
+
+    buf = io.StringIO()
+    exit_code = None
+    with contextlib.redirect_stdout(buf), contextlib.redirect_stderr(buf):
+        try:
+            witnesslint_main.main(argv)
+        except SystemExit as e:
+            exit_code = e.code if isinstance(e.code, int) else 1
+        except Exception as e:  # noqa: BLE001 - surfaced to the UI, not swallowed
+            buf.write("\nINTERNAL ERROR: {}: {}\n".format(type(e).__name__, e))
+            exit_code = -1
+    return {"exit_code": exit_code, "output": buf.getvalue()}
+
+
+def instrument(c_path: str, witness_path: str) -> dict:
+    from hacks import hacks
+    from instrument import instrument as run_instrument
+
+    headers_dir = "/py/cwt/headers"
+    buf = io.StringIO()
+    try:
+        with open(c_path, "r") as f:
+            src = f.read()
+        hacked = hacks(src)
+        with open(c_path, "w") as f:
+            f.write(hacked)
+
+        source, data_race = run_instrument(c_path, witness_path, headers_dir)
+        return {"ok": True, "source": source, "data_race": data_race, "log": buf.getvalue()}
+    except Exception as e:  # noqa: BLE001 - surfaced to the UI, not swallowed
+        return {
+            "ok": False,
+            "error": "{}: {}".format(type(e).__name__, e),
+            "log": buf.getvalue(),
+        }
diff --git a/www-demo/pyodide-worker.js b/www-demo/pyodide-worker.js
new file mode 100644
index 0000000000..43447b7054
--- /dev/null
+++ b/www-demo/pyodide-worker.js
@@ -0,0 +1,96 @@
+// Web Worker owning the Pyodide runtime. Both the live linter and the
+// instrumenter run here so the UI thread (and Monaco) never blocks.
+//
+// Pyodide itself is loaded from the jsdelivr CDN at runtime rather than
+// vendored: the site already depends on network access for the live
+// sv-benchmarks browser (GitLab API), and the full Pyodide distribution
+// (~400MB) is impractical to vendor, while pyodide-core lacks the
+// pyyaml/lxml/jsonschema builds we need. Monaco is vendored locally since
+// it is the primary UI and reasonably sized.
+const PYODIDE_VERSION = "0.29.4";
+const PYODIDE_INDEX_URL = `https://cdn.jsdelivr.net/pyodide/v${PYODIDE_VERSION}/full/`;
+
+importScripts(PYODIDE_INDEX_URL + "pyodide.js");
+
+let pyodideReadyPromise = null;
+
+async function initPyodide() {
+  const pyodide = await loadPyodide({ indexURL: PYODIDE_INDEX_URL });
+  await pyodide.loadPackage([
+    "pyyaml",
+    "lxml",
+    "jsonschema",
+    "pycparser",
+    "networkx",
+    "micropip",
+  ]);
+
+  const micropip = pyodide.pyimport("micropip");
+  const wheelUrl = new URL(
+    "vendor/pypi/pcpp-1.30-py2.py3-none-any.whl",
+    self.location.href
+  ).toString();
+  await micropip.install(wheelUrl);
+
+  const zipResp = await fetch(new URL("py.zip", self.location.href));
+  const zipBuf = await zipResp.arrayBuffer();
+  pyodide.unpackArchive(zipBuf, "zip", { extractDir: "/" });
+
+  pyodide.FS.mkdirTree("/work");
+  await pyodide.runPythonAsync(`
+import sys
+for p in ("/py", "/py/cwt"):
+    if p not in sys.path:
+        sys.path.insert(0, p)
+import shim  # noqa: F401  (import once now so later calls are fast)
+`);
+
+  return pyodide;
+}
+
+function getPyodide() {
+  if (!pyodideReadyPromise) {
+    pyodideReadyPromise = initPyodide();
+  }
+  return pyodideReadyPromise;
+}
+
+// Kick off loading immediately so it's ready by the time the user acts.
+getPyodide().then(
+  () => postMessage({ cmd: "ready" }),
+  (err) => postMessage({ cmd: "error", error: String(err) })
+);
+
+self.onmessage = async (event) => {
+  const { id, cmd } = event.data;
+  try {
+    const pyodide = await getPyodide();
+    const shim = pyodide.pyimport("shim");
+
+    if (cmd === "lint") {
+      const { yaml, c, strict } = event.data;
+      pyodide.FS.writeFile("/work/witness.yml", yaml);
+      let programPath = null;
+      if (c !== null && c !== undefined) {
+        pyodide.FS.writeFile("/work/program.c", c);
+        programPath = "/work/program.c";
+      }
+      const result = shim.lint("/work/witness.yml", programPath, !!strict).toJs({
+        dict_converter: Object.fromEntries,
+      });
+      postMessage({ id, cmd, ok: true, result });
+    } else if (cmd === "instrument") {
+      const { c, yaml } = event.data;
+      pyodide.FS.writeFile("/work/input.c", c);
+      pyodide.FS.writeFile("/work/witness.yml", yaml);
+      const result = shim.instrument("/work/input.c", "/work/witness.yml").toJs({
+        dict_converter: Object.fromEntries,
+      });
+      postMessage({ id, cmd, ok: true, result });
+    } else {
+      postMessage({ id, cmd, ok: false, error: `Unknown command: ${cmd}` });
+    }
+  } catch (err) {
+    postMessage({ id, cmd, ok: false, error: String(err && err.message ? err.message : err) });
+  }
+};
diff --git a/www-demo/style.css b/www-demo/style.css
new file mode 100644
index 0000000000..113beea794
--- /dev/null
+++ b/www-demo/style.css
@@ -0,0 +1,474 @@
+:root {
+  --bg: #1e1e1e;
+  --panel: #252526;
+  --border: #3c3c3c;
+  --text: #d4d4d4;
+  --text-muted: #999;
+  --text-faint: #777;
+  --accent: #0e639c;
+  --accent-hover: #1177bb;
+  --accent-text: #ffffff;
+  --control-bg: #333333;
+  --control-hover: #3e3e3e;
+  --hover-bg: #2a2d2e;
+  --menu-bg: #2d2d2d;
+  --output-bg: #181818;
+  --shadow: rgba(0, 0, 0, 0.4);
+  --ok: #3fb950;
+  --ok-hover: #56d367;
+  --warn: #d29922;
+  --err: #f85149;
+  font-family: -apple-system, "Segoe UI", Roboto, Helvetica, Arial, sans-serif;
+}
+
+:root[data-theme="light"] {
+  --bg: #ffffff;
+  --panel: #f3f3f3;
+  --border: #d4d4d4;
+  --text: #1e1e1e;
+  --text-muted: #5f5f5f;
+  --text-faint: #8a8a8a;
+  --accent: #0e639c;
+  --accent-hover: #0b5a8a;
+  --accent-text: #ffffff;
+  --control-bg: #e8e8e8;
+  --control-hover: #dcdcdc;
+  --hover-bg: #e4e4e4;
+  --menu-bg: #ffffff;
+  --output-bg: #f5f5f5;
+  --shadow: rgba(0, 0, 0, 0.15);
+  --ok: #1a7f37;
+  --ok-hover: #15642c;
+  --warn: #9a6700;
+  --err: #cf222e;
+}
+
+* { box-sizing: border-box; }
+
+html, body {
+  margin: 0;
+  height: 100%;
+  background: var(--bg);
+  color: var(--text);
+  font-size: 14px;
+}
+
+body {
+  display: flex;
+  flex-direction: column;
+  height: 100vh;
+}
+
+body.resizing-h { cursor: col-resize; user-select: none; }
+body.resizing-v { cursor: row-resize; user-select: none; }
+
+#topbar {
+  display: flex;
+  align-items: center;
+  justify-content: space-between;
+  padding: 8px 16px;
+  background: var(--panel);
+  border-bottom: 1px solid var(--border);
+  flex-shrink: 0;
+}
+
+#topbar h1 {
+  font-size: 15px;
+  font-weight: 600;
+  margin: 0;
+}
+
+.topbar-left {
+  display: flex;
+  align-items: center;
+  gap: 12px;
+}
+
+.topbar-right {
+  display: flex;
+  align-items: center;
+  gap: 14px;
+}
+
+.hamburger-btn {
+  display: flex;
+  flex-direction: column;
+  justify-content: center;
+  align-items: center;
+  gap: 4px;
+  width: 30px;
+  height: 30px;
+  padding: 0;
+  background: transparent;
+  border: 1px solid transparent;
+}
+.hamburger-btn:hover:not(:disabled) {
+  background: var(--control-bg);
+  border-color: var(--border);
+}
+.hamburger-btn span {
+  display: block;
+  width: 16px;
+  height: 2px;
+  background: var(--text);
+  border-radius: 1px;
+}
+
+.theme-toggle {
+  font-size: 15px;
+  line-height: 1;
+  padding: 4px 8px;
+}
+
+.guide-link {
+  font-size: 12.5px;
+  color: var(--accent-hover);
+  text-decoration: none;
+}
+.guide-link:hover { text-decoration: underline; }
+
+.status {
+  font-size: 12px;
+  padding: 3px 10px;
+  border-radius: 12px;
+  border: 1px solid var(--border);
+  white-space: nowrap;
+}
+
+.status-loading { color: var(--warn); border-color: var(--warn); }
+.status-idle { color: var(--text-muted); }
+.status-ok { color: var(--ok); border-color: var(--ok); }
+.status-warn { color: var(--warn); border-color: var(--warn); }
+.status-err { color: var(--err); border-color: var(--err); }
+
+#layout {
+  display: flex;
+  flex: 1;
+  min-height: 0;
+  position: relative;
+}
+
+#sidebar {
+  width: 300px;
+  flex: 0 0 auto;
+  background: var(--panel);
+  border-right: 1px solid var(--border);
+  overflow-y: auto;
+  padding: 8px;
+  position: relative;
+}
+
+body.sidebar-collapsed #sidebar,
+body.sidebar-collapsed #sidebar-resizer {
+  display: none;
+}
+
+#sidebar h2 {
+  font-size: 12px;
+  text-transform: uppercase;
+  letter-spacing: 0.05em;
+  color: var(--text-muted);
+  margin: 16px 0 6px;
+}
+
+#sidebar .hint {
+  font-size: 11px;
+  color: var(--text-muted);
+  margin: 0 0 6px;
+  line-height: 1.4;
+}
+
+#sidebar .hint a { color: var(--accent-hover); }
+#sidebar .hint code { color: var(--text-muted); }
+
+.ref-picker {
+  display: flex;
+  align-items: center;
+  gap: 6px;
+  margin: 0 0 8px;
+}
+
+.ref-picker label {
+  font-size: 11px;
+  color: var(--text-muted);
+  white-space: nowrap;
+}
+
+.ref-picker input {
+  flex: 1;
+  min-width: 0;
+  font-size: 11px;
+  padding: 2px 6px;
+  font-family: "SF Mono", Consolas, Menlo, monospace;
+}
+
+.example-list {
+  list-style: none;
+  margin: 0;
+  padding: 0;
+}
+
+.example-list li {
+  padding: 4px 6px;
+  border-radius: 4px;
+  cursor: pointer;
+  font-size: 12.5px;
+  white-space: normal;
+  overflow-wrap: anywhere;
+  line-height: 1.35;
+}
+
+.example-list li:hover {
+  background: var(--hover-bg);
+}
+
+.example-list li.category {
+  font-weight: 600;
+  color: var(--text);
+  white-space: nowrap;
+}
+
+.example-list li.category::before {
+  content: "\25B8 ";
+  display: inline-block;
+  width: 12px;
+}
+
+.example-list li.category.open::before {
+  content: "\25BE ";
+}
+
+.example-list li.file {
+  padding-left: 22px;
+  color: var(--text-muted);
+}
+
+.example-list li.loading,
+.example-list li.empty {
+  padding-left: 22px;
+  color: var(--text-faint);
+  font-style: italic;
+  cursor: default;
+}
+
+/* Drag handles between resizable panels */
+.resizer {
+  flex-shrink: 0;
+  background: var(--border);
+}
+.resizer-v {
+  width: 4px;
+  cursor: col-resize;
+}
+.resizer-v:hover { background: var(--accent); }
+.resizer-h {
+  height: 4px;
+  cursor: row-resize;
+}
+.resizer-h:hover { background: var(--accent); }
+
+#editors {
+  flex: 1;
+  display: flex;
+  min-width: 0;
+}
+
+.pane {
+  flex: 1;
+  display: flex;
+  flex-direction: column;
+  min-width: 0;
+}
+
+.pane-toolbar {
+  display: flex;
+  align-items: center;
+  gap: 8px;
+  padding: 6px 10px;
+  background: var(--panel);
+  border-bottom: 1px solid var(--border);
+  flex-shrink: 0;
+  flex-wrap: wrap;
+}
+
+.pane-title {
+  font-weight: 600;
+  font-size: 12.5px;
+}
+
+.filename {
+  font-size: 11.5px;
+  color: var(--text-muted);
+  flex: 1;
+  overflow: hidden;
+  text-overflow: ellipsis;
+  white-space: nowrap;
+}
+
+.cursor-pos {
+  font-size: 11px;
+  color: var(--text-muted);
+  font-family: "SF Mono", Consolas, Menlo, monospace;
+  white-space: nowrap;
+}
+
+button, select, input[type="text"] {
+  background: var(--control-bg);
+  color: var(--text);
+  border: 1px solid var(--border);
+  border-radius: 4px;
+  padding: 4px 10px;
+  font-size: 12px;
+}
+
+button { cursor: pointer; }
+button:hover:not(:disabled) { background: var(--control-hover); }
+button:disabled { opacity: 0.5; cursor: default; }
+input[type="text"]:focus {
+  outline: 1px solid var(--accent);
+  outline-offset: -1px;
+}
+
+/* Split button (GitHub merge-button style): main action + caret + menu */
+.split-button {
+  display: flex;
+  position: relative;
+}
+.split-button #instrument-btn {
+  background: var(--accent);
+  color: var(--accent-text);
+  border-color: var(--accent);
+  border-radius: 4px 0 0 4px;
+  border-right: 1px solid rgba(0, 0, 0, 0.2);
+  white-space: nowrap;
+}
+.split-button #instrument-btn:hover:not(:disabled) { background: var(--accent-hover); }
+.split-button #instrument-caret {
+  background: var(--accent);
+  color: var(--accent-text);
+  border-color: var(--accent);
+  border-radius: 0 4px 4px 0;
+  padding: 4px 6px;
+}
+.split-button #instrument-caret:hover:not(:disabled) { background: var(--accent-hover); }
+.split-menu {
+  position: absolute;
+  top: 100%;
+  right: 0;
+  margin-top: 4px;
+  background: var(--menu-bg);
+  border: 1px solid var(--border);
+  border-radius: 4px;
+  box-shadow: 0 4px 12px var(--shadow);
+  z-index: 10;
+  min-width: 220px;
+  overflow: hidden;
+}
+.split-menu button {
+  display: block;
+  width: 100%;
+  text-align: left;
+  background: transparent;
+  color: var(--text);
+  border: none;
+  border-radius: 0;
+  padding: 8px 12px;
+}
+.split-menu button:hover { background: var(--accent); color: var(--accent-text); }
+
+#compile-run-btn {
+  background: var(--ok);
+  color: var(--accent-text);
+  border-color: var(--ok);
+  white-space: nowrap;
+}
+#compile-run-btn:hover:not(:disabled) {
+  background: var(--ok-hover);
+  border-color: var(--ok-hover);
+}
+
+.monaco-container {
+  flex: 1;
+  min-height: 0;
+}
+
+/* Decorations marking instrumentation calls in the C editor */
+.cwt-yield-call {
+  background: rgba(214, 158, 46, 0.28);
+  border-radius: 2px;
+}
+.cwt-release-call {
+  background: rgba(46, 160, 110, 0.28);
+  border-radius: 2px;
+}
+
+#output-panel {
+  flex-shrink: 0;
+  height: 220px;
+  display: flex;
+  flex-direction: column;
+  border-top: 1px solid var(--border);
+  background: var(--output-bg);
+}
+
+#output-panel.collapsed {
+  height: auto;
+}
+
+#output-resizer.collapsed {
+  display: none;
+}
+
+.output-toolbar {
+  display: flex;
+  align-items: center;
+  gap: 8px;
+  padding: 4px 10px;
+  font-size: 11.5px;
+  color: var(--text-muted);
+  border-bottom: 1px solid var(--border);
+}
+
+.output-toolbar button { padding: 2px 8px; }
+
+#output-panes {
+  flex: 1;
+  display: flex;
+  min-height: 0;
+}
+
+.output-pane {
+  flex: 1;
+  min-width: 0;
+  display: flex;
+  flex-direction: column;
+  border-right: 1px solid var(--border);
+}
+
+.output-pane:last-child { border-right: none; }
+
+.output-pane-header {
+  display: flex;
+  align-items: center;
+  justify-content: space-between;
+  gap: 8px;
+  padding: 3px 10px;
+  font-size: 11px;
+  font-weight: 600;
+  color: var(--text-muted);
+  border-bottom: 1px solid var(--border);
+}
+
+.output-pane-header button { padding: 1px 6px; font-size: 10.5px; font-weight: 400; }
+
+.output-content {
+  margin: 0;
+  padding: 8px 12px;
+  overflow: auto;
+  font-family: "SF Mono", Consolas, Menlo, monospace;
+  font-size: 12px;
+  white-space: pre-wrap;
+  flex: 1;
+}
+
+#output-panel.collapsed #output-panes { display: none; }
diff --git a/www-demo/wasmer-run.js b/www-demo/wasmer-run.js
new file mode 100644
index 0000000000..01e8118d4b
--- /dev/null
+++ b/www-demo/wasmer-run.js
@@ -0,0 +1,76 @@
+// Compiles and runs the C editor's *current* contents (verbatim -- the
+// caller must not re-instrument it) together with svcomp.c, using the
+// Wasmer JS SDK's WASIX runtime: real clang (the "clang/clang" Wasmer
+// registry package) compiles to wasm32-wasix, and the resulting module
+// runs with real multithreading (Web Workers + SharedArrayBuffer), not a
+// single-threaded simulation. Both the SDK and clang's wasm itself are
+// fetched lazily on first use -- clang in particular is ~100MB and comes
+// straight from Wasmer's registry, not vendored, mirroring how Pyodide is
+// loaded from a CDN at runtime elsewhere in this app.
+
+let sdkModulePromise = null;
+let clangPackagePromise = null;
+
+async function getSdk() {
+  if (!sdkModulePromise) {
+    sdkModulePromise = (async () => {
+      const mod = await import("./vendor/wasmer/index.mjs");
+      // setWorkerUrl reaches into the wasm-bindgen exports object, which
+      // only exists once init() has loaded and instantiated the wasm --
+      // calling it first throws (exports object is still undefined).
+      await mod.init();
+      mod.setWorkerUrl(new URL("./vendor/wasmer/worker.mjs", import.meta.url).toString());
+      return mod;
+    })();
+  }
+  return sdkModulePromise;
+}
+
+async function getClang(mod) {
+  if (!clangPackagePromise) {
+    clangPackagePromise = mod.Wasmer.fromRegistry("clang/clang");
+  }
+  return clangPackagePromise;
+}
+
+// onStatus(text) is called with short progress updates as compilation
+// proceeds through its stages (first run is slow: SDK init + ~100MB clang
+// package fetch). Returns { stage: "compile"|"run", code, stdout, stderr }.
+export async function compileAndRun(cSource, svcompSource, onStatus) {
+  onStatus?.("Loading Wasmer SDK…");
+  const mod = await getSdk();
+
+  onStatus?.("Fetching clang (≈100MB on first run, cached after)…");
+  const clang = await getClang(mod);
+
+  const project = new mod.Directory();
+  await project.writeFile("program.c", cSource);
+  await project.writeFile("svcomp.c", svcompSource);
+
+  onStatus?.("Compiling with clang (-pthread, wasm32-wasix)…");
+  const compile = await clang.entrypoint.run({
+    args: ["/project/program.c", "/project/svcomp.c", "-pthread", "-o", "/project/a.wasm"],
+    mount: { "/project": project },
+  });
+  const compileResult = await compile.wait();
+  if (compileResult.code !== 0) {
+    return {
+      stage: "compile",
+      code: compileResult.code,
+      stdout: compileResult.stdout,
+      stderr: compileResult.stderr,
+    };
+  }
+
+  onStatus?.("Running with real multithreading…");
+  const wasmBytes = await project.readFile("a.wasm");
+  const program = await mod.Wasmer.fromFile(wasmBytes);
+  const instance = await program.entrypoint.run();
+  const runResult = await instance.wait();
+  return {
+    stage: "run",
+    code: runResult.code,
+    stdout: runResult.stdout,
+    stderr: runResult.stderr,
+  };
+}

From 59d471866c7d090d37f50d0d309611ee96084df0 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Sat, 20 Jun 2026 16:47:46 +0200
Subject: [PATCH 07/10] added worfklow

---
 .claude/settings.json          | 36 -------------------
 .github/workflows/gh-pages.yml | 64 ++++++++++++++++++++++++++++++++++
 www-demo/README.md             | 19 ++++++++++
 3 files changed, 83 insertions(+), 36 deletions(-)
 delete mode 100644 .claude/settings.json
 create mode 100644 .github/workflows/gh-pages.yml

diff --git a/.claude/settings.json b/.claude/settings.json
deleted file mode 100644
index b7394ba3e7..0000000000
--- a/.claude/settings.json
+++ /dev/null
@@ -1,36 +0,0 @@
-{
-  "permissions": {
-    "allow": [
-      "Bash(python3 -c \"import pycparser, os; print\\(pycparser.__file__\\)\")",
-      "Bash(find / -iname \"fake_libc_include\" -maxdepth 8)",
-      "Bash(./smoketest.sh)",
-      "Bash(python3 -)",
-      "Bash(*)",
-      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/regen.c svcomp.c -o /tmp/regen_bin)",
-      "Bash(echo \"exit: $?\")",
-      "Bash(cpp -I headers -D'__attribute__\\(x\\)=' /home/levente/Documents/University/sv-benchmarks/c/goblint-coreutils/instrumented_dd_comb.c)",
-      "Bash(echo \"smoketest exit: $?\")",
-      "Bash(./package.sh)",
-      "Bash(sed -n '760,770p' /usr/include/pthread.h)",
-      "Read(//usr/include/**)",
-      "Bash(python3 -c \"from pycparser import preprocess_file, CParser; print\\('ok'\\)\")",
-      "Bash(cd /home/levente/Documents/University/concurrency-witnesses/concurrentwitness2test *)",
-      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/szymanski_regen.c svcomp.c -o /tmp/szymanski_bin)",
-      "Bash(grep -c '\\\\$' /home/levente/Documents/University/theta/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/stdlib/stdatomic.h.kt)",
-      "Bash(grep -n \"typedef.*mode_t\\\\|mode_t.*;$\" /home/levente/Documents/University/sv-benchmarks/c/goblint-coreutils/instrumented_dd_comb.c)",
-      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/dd_comb_regen.c svcomp.c -o /tmp/dd_comb_bin)",
-      "Bash(gcc -w -Wno-implicit-function-declaration -pthread /tmp/dd_comb_regen2.c svcomp.c -o /tmp/dd_comb_bin2)",
-      "Bash(curl -s --max-time 10 \"https://api.github.com/repos/sosy-lab/sv-benchmarks/contents/c\")",
-      "Bash(echo \"EXIT:$?\")",
-      "Bash(python3 -c \"import json,sys; d=json.load\\(sys.stdin\\); [print\\(x['name']\\) for x in d if x['type']=='dir' and \\('pthread' in x['name'].lower\\(\\) or 'thread' in x['name'].lower\\(\\) or 'concur' in x['name'].lower\\(\\)\\)]\")",
-      "Bash(curl -s --max-time 10 -I \"https://api.github.com/repos/sosy-lab/sv-benchmarks/contents/c/pthread\")",
-      "WebSearch",
-      "WebFetch(domain:wasmer.io)",
-      "WebFetch(domain:raw.githubusercontent.com)"
-    ],
-    "additionalDirectories": [
-      "/tmp",
-      "/home/levente/Documents/University/theta/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/stdlib"
-    ]
-  }
-}
diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml
new file mode 100644
index 0000000000..f2cecc83ef
--- /dev/null
+++ b/.github/workflows/gh-pages.yml
@@ -0,0 +1,64 @@
+name: Deploy www-demo to GitHub Pages
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'www-demo/**'
+      - 'witnessparser.py'
+      - 'witness2ast.py'
+      - 'tweaks.py'
+      - 'Exceptions.py'
+      - 'hacks.py'
+      - 'headers/**'
+      - 'svcomp.c'
+      - '.github/workflows/gh-pages.yml'
+  workflow_dispatch:
+
+# Only one Pages deployment at a time; a newer push supersedes an in-flight one.
+concurrency:
+  group: pages
+  cancel-in-progress: false
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build:
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
+
+      # The Dockerfile is the single source of truth for assembling the
+      # static site (vendoring Monaco/Wasmer SDK, cloning sv-witnesses'
+      # linter+schemas+examples, building py.zip, etc.) -- build it here and
+      # extract the result rather than re-implementing those steps in YAML.
+      - name: Build www-demo image
+        run: docker build -f www-demo/Dockerfile -t cwt-demo .
+
+      - name: Extract static site from image
+        run: |
+          docker create --name cwt-demo-extract cwt-demo
+          mkdir -p ./pages-dist
+          docker cp cwt-demo-extract:/usr/share/nginx/html/. ./pages-dist/
+          docker rm cwt-demo-extract
+
+      - name: Upload Pages artifact
+        uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3
+        with:
+          path: ./pages-dist
+
+  deploy:
+    needs: build
+    runs-on: ubuntu-24.04
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - name: Configure Pages
+        uses: actions/configure-pages@983d7736d9b0ae728b81ab479565c72886d7745b # v5
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4
diff --git a/www-demo/README.md b/www-demo/README.md
index 1e8f665129..1a87d26056 100644
--- a/www-demo/README.md
+++ b/www-demo/README.md
@@ -103,6 +103,25 @@ directory (user-editable via the "Branch/tag" field).
   approach itself — Wasmer's threading model targets the browser (Web
   Workers + `SharedArrayBuffer`), which is also this feature's actual
   runtime, not Node. This needs real-browser testing to confirm.
+- On the GitHub Pages deployment (`.github/workflows/gh-pages.yml`),
+  "Compile & Run" loses real multithreading: `SharedArrayBuffer` needs the
+  page to be cross-origin isolated, which needs the
+  `Cross-Origin-Opener-Policy`/`Cross-Origin-Embedder-Policy` response
+  headers `nginx.conf` sets for the Docker deployment -- and GitHub Pages
+  has no mechanism to set custom response headers at all (no `_headers`
+  file support like Netlify/Cloudflare Pages). Everything else (linting,
+  instrumentation) is unaffected, since it doesn't depend on
+  cross-origin isolation. Self-host via Docker for full Compile & Run.
+
+## Deploying
+
+`.github/workflows/gh-pages.yml` builds the same Dockerfile used locally,
+extracts the resulting static tree (`docker create` + `docker cp`, no
+re-implementation of the vendoring steps), and publishes it via GitHub's
+official Pages actions. It runs on every push to `main` that touches
+`www-demo/` or the Python modules it vendors, plus manual dispatch. The
+repo's Pages source must be set to "GitHub Actions" once, under Settings →
+Pages → Build and deployment → Source.
 
 ## Bugs found and fixed upstream while building this
 

From 546572f2fc249f5aeaa156f1c364a1c12f477ea2 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Sat, 20 Jun 2026 16:48:32 +0200
Subject: [PATCH 08/10] black

---
 main.py   |  4 +++-
 tweaks.py | 12 ++++++++----
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/main.py b/main.py
index 1e6f3d43e5..407dce7ace 100644
--- a/main.py
+++ b/main.py
@@ -52,7 +52,9 @@ def translate_to_c(filename, witness, mode, timeout):
     """Apply the witness to the parsed AST, then compile and run the result."""
     try:
         text = preprocess_file(
-            filename, cpp_path="cpp", cpp_args=["-I" + HEADERS_DIR] + CPP_GNU_COMPAT_ARGS
+            filename,
+            cpp_path="cpp",
+            cpp_args=["-I" + HEADERS_DIR] + CPP_GNU_COMPAT_ARGS,
         )
         ast = CParser().parse(text, filename)
     except KnownErrorVerdict as e:
diff --git a/tweaks.py b/tweaks.py
index 4315d873fc..c8d58a1752 100644
--- a/tweaks.py
+++ b/tweaks.py
@@ -26,10 +26,14 @@ def declare_schedule_functions(ast):
     separately), which relies on implicit-function-declaration being
     tolerated by the compiler.
     """
-    prototypes = CParser().parse(
-        "void __concurrentwit2test_yield(int, int);\n"
-        "void __concurrentwit2test_release(int, int);\n"
-    ).ext
+    prototypes = (
+        CParser()
+        .parse(
+            "void __concurrentwit2test_yield(int, int);\n"
+            "void __concurrentwit2test_release(int, int);\n"
+        )
+        .ext
+    )
     ast.ext[0:0] = prototypes
 
 

From bae165599ff27bb97e6f6a5bbdec329c265af053 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Sat, 20 Jun 2026 16:49:19 +0200
Subject: [PATCH 09/10] black

---
 .../actions/zenodo-release/zenodo_release.py  | 129 ++++++++++--------
 www-demo/py/shim.py                           |   7 +-
 2 files changed, 75 insertions(+), 61 deletions(-)

diff --git a/.github/actions/zenodo-release/zenodo_release.py b/.github/actions/zenodo-release/zenodo_release.py
index 78ced4ca14..8654a1bc49 100644
--- a/.github/actions/zenodo-release/zenodo_release.py
+++ b/.github/actions/zenodo-release/zenodo_release.py
@@ -22,7 +22,7 @@ def __init__(self, token: str, record_id: str):
         self.base_url = "https://zenodo.org/api"
         self.headers = {
             "Authorization": f"Bearer {token}",
-            "Content-Type": "application/json"
+            "Content-Type": "application/json",
         }
 
     def _make_request(self, method: str, url: str, **kwargs) -> requests.Response:
@@ -33,7 +33,7 @@ def _make_request(self, method: str, url: str, **kwargs) -> requests.Response:
             return response
         except requests.exceptions.RequestException as e:
             print(f"Request failed: {e}")
-            if hasattr(e.response, 'text'):
+            if hasattr(e.response, "text"):
                 print(f"Response: {e.response.text}")
             raise
 
@@ -49,9 +49,9 @@ def get_draft_depositions(self) -> list:
         params = {"q": f"conceptrecid:{self.record_id}", "all_versions": "true"}
         response = self._make_request("GET", url, headers=self.headers, params=params)
         data = response.json()
-        
+
         # Filter for drafts only
-        drafts = [d for d in data if d.get('submitted') is False]
+        drafts = [d for d in data if d.get("submitted") is False]
         return drafts
 
     def delete_draft(self, deposition_id: str) -> None:
@@ -68,11 +68,11 @@ def cleanup_existing_drafts(self) -> None:
         """Clean up any existing draft versions that might be in limbo."""
         print("Checking for existing draft versions...")
         drafts = self.get_draft_depositions()
-        
+
         if drafts:
             print(f"Found {len(drafts)} existing draft(s). Cleaning up...")
             for draft in drafts:
-                draft_id = draft['id']
+                draft_id = draft["id"]
                 self.delete_draft(draft_id)
         else:
             print("No existing drafts found.")
@@ -80,56 +80,60 @@ def cleanup_existing_drafts(self) -> None:
     def create_new_version(self) -> Dict[str, Any]:
         """Create a new version of the record."""
         print(f"Creating new version for record {self.record_id}")
-        
+
         url = f"{self.base_url}/deposit/depositions/{self.record_id}/actions/newversion"
         response = self._make_request("POST", url, headers=self.headers)
         data = response.json()
-        
+
         # Get the latest draft URL from the response
-        latest_draft_url = data.get('links', {}).get('latest_draft')
+        latest_draft_url = data.get("links", {}).get("latest_draft")
         if not latest_draft_url:
             raise ValueError("Could not get latest draft URL from response")
-        
+
         # Fetch the draft to get the actual deposition data
-        draft_response = self._make_request("GET", latest_draft_url, headers=self.headers)
+        draft_response = self._make_request(
+            "GET", latest_draft_url, headers=self.headers
+        )
         draft_data = draft_response.json()
-        
+
         return draft_data
 
-    def update_metadata(self, deposition_data: Dict[str, Any], tool_name: str, metadata_file: Path) -> None:
+    def update_metadata(
+        self, deposition_data: Dict[str, Any], tool_name: str, metadata_file: Path
+    ) -> None:
         """Update the metadata for the deposition."""
-        deposition_id = deposition_data['id']
+        deposition_id = deposition_data["id"]
         print(f"Updating metadata for deposition {deposition_id}")
-        
+
         # Read the metadata template
-        with open(metadata_file, 'r') as f:
+        with open(metadata_file, "r") as f:
             metadata_template = json.load(f)
-        
+
         # Replace placeholders
-        today = date.today().strftime('%Y-%m-%d')
+        today = date.today().strftime("%Y-%m-%d")
         metadata_json = json.dumps(metadata_template)
-        metadata_json = metadata_json.replace('__TODAY__', today)
-        metadata_json = metadata_json.replace('__TOOL__', tool_name)
+        metadata_json = metadata_json.replace("__TODAY__", today)
+        metadata_json = metadata_json.replace("__TOOL__", tool_name)
         metadata = json.loads(metadata_json)
-        
+
         # Update the deposition
-        url = deposition_data['links']['self']
+        url = deposition_data["links"]["self"]
         response = self._make_request("PUT", url, headers=self.headers, json=metadata)
-        
+
         print(f"Metadata updated successfully (date := {today}, tool := {tool_name})")
         return response.json()
 
     def delete_existing_files(self, deposition_data: Dict[str, Any]) -> None:
         """Delete any existing files from the draft."""
-        files = deposition_data.get('files', [])
+        files = deposition_data.get("files", [])
         if not files:
             print("No existing files to delete.")
             return
-        
+
         print(f"Deleting {len(files)} existing file(s)...")
         for file_info in files:
-            file_id = file_info['id']
-            deposition_id = deposition_data['id']
+            file_id = file_info["id"]
+            deposition_id = deposition_data["id"]
             url = f"{self.base_url}/deposit/depositions/{deposition_id}/files/{file_id}"
             try:
                 self._make_request("DELETE", url, headers=self.headers)
@@ -139,88 +143,93 @@ def delete_existing_files(self, deposition_data: Dict[str, Any]) -> None:
 
     def upload_file(self, deposition_data: Dict[str, Any], file_path: Path) -> None:
         """Upload a file to the deposition."""
-        bucket_url = deposition_data['links']['bucket']
+        bucket_url = deposition_data["links"]["bucket"]
         filename = file_path.name
-        
-        print(f"Uploading file: {filename} ({file_path.stat().st_size / (1024*1024):.2f} MB)")
-        
+
+        print(
+            f"Uploading file: {filename} ({file_path.stat().st_size / (1024*1024):.2f} MB)"
+        )
+
         # Upload using the bucket API (streaming)
         upload_url = f"{bucket_url}/{filename}"
-        with open(file_path, 'rb') as f:
+        with open(file_path, "rb") as f:
             headers = {"Authorization": f"Bearer {self.token}"}
             response = self._make_request("PUT", upload_url, headers=headers, data=f)
-        
+
         print(f"Upload successful: {filename}")
 
     def publish(self, deposition_data: Dict[str, Any]) -> Dict[str, Any]:
         """Publish the deposition."""
-        publish_url = deposition_data['links']['publish']
+        publish_url = deposition_data["links"]["publish"]
         print(f"Publishing deposition...")
-        
+
         response = self._make_request("POST", publish_url, headers=self.headers)
         data = response.json()
-        
-        doi = data.get('doi', 'N/A')
-        doi_url = data.get('doi_url', 'N/A')
+
+        doi = data.get("doi", "N/A")
+        doi_url = data.get("doi_url", "N/A")
         print(f"Publish successful!")
         print(f"DOI: {doi}")
         print(f"DOI URL: {doi_url}")
-        
+
         return data
 
 
 def main():
-    parser = argparse.ArgumentParser(description='Create and publish a Zenodo release')
-    parser.add_argument('--token', required=True, help='Zenodo API token')
-    parser.add_argument('--record-id', required=True, help='Previous record ID')
-    parser.add_argument('--tool', required=True, help='Tool name')
-    parser.add_argument('--file', required=True, help='ZIP file to upload')
-    parser.add_argument('--metadata', required=True, help='Metadata JSON file')
-    parser.add_argument('--cleanup-drafts', action='store_true', 
-                       help='Clean up existing draft versions before creating new one')
-    
+    parser = argparse.ArgumentParser(description="Create and publish a Zenodo release")
+    parser.add_argument("--token", required=True, help="Zenodo API token")
+    parser.add_argument("--record-id", required=True, help="Previous record ID")
+    parser.add_argument("--tool", required=True, help="Tool name")
+    parser.add_argument("--file", required=True, help="ZIP file to upload")
+    parser.add_argument("--metadata", required=True, help="Metadata JSON file")
+    parser.add_argument(
+        "--cleanup-drafts",
+        action="store_true",
+        help="Clean up existing draft versions before creating new one",
+    )
+
     args = parser.parse_args()
-    
+
     # Validate file paths
     file_path = Path(args.file)
     if not file_path.exists():
         print(f"Error: File not found: {file_path}")
         sys.exit(1)
-    
+
     metadata_path = Path(args.metadata)
     if not metadata_path.exists():
         print(f"Error: Metadata file not found: {metadata_path}")
         sys.exit(1)
-    
+
     try:
         releaser = ZenodoReleaser(args.token, args.record_id)
-        
+
         # Optional: Clean up any existing drafts
         if args.cleanup_drafts:
             releaser.cleanup_existing_drafts()
-        
+
         # Create new version
         deposition = releaser.create_new_version()
-        
+
         # Update metadata
         deposition = releaser.update_metadata(deposition, args.tool, metadata_path)
-        
+
         # Delete any existing files from the draft
         releaser.delete_existing_files(deposition)
-        
+
         # Upload the file
         releaser.upload_file(deposition, file_path)
-        
+
         # Publish
         releaser.publish(deposition)
-        
+
         print("\n=== Release completed successfully! ===")
-        
+
     except Exception as e:
         print(f"\n=== Release failed ===")
         print(f"Error: {e}")
         sys.exit(1)
 
 
-if __name__ == '__main__':
+if __name__ == "__main__":
     main()
diff --git a/www-demo/py/shim.py b/www-demo/py/shim.py
index ada64ab63c..c2f3580e7d 100644
--- a/www-demo/py/shim.py
+++ b/www-demo/py/shim.py
@@ -53,7 +53,12 @@ def instrument(c_path: str, witness_path: str) -> dict:
             f.write(hacked)
 
         source, data_race = run_instrument(c_path, witness_path, headers_dir)
-        return {"ok": True, "source": source, "data_race": data_race, "log": buf.getvalue()}
+        return {
+            "ok": True,
+            "source": source,
+            "data_race": data_race,
+            "log": buf.getvalue(),
+        }
     except Exception as e:  # noqa: BLE001 - surfaced to the UI, not swallowed
         return {
             "ok": False,

From a19d02ac4592301116bf3c30a622e265107dfbde Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Sat, 20 Jun 2026 16:56:26 +0200
Subject: [PATCH 10/10] Updated sonar

---
 .github/workflows/sonar-check.yml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/sonar-check.yml b/.github/workflows/sonar-check.yml
index 948000aaf6..5f8262db65 100644
--- a/.github/workflows/sonar-check.yml
+++ b/.github/workflows/sonar-check.yml
@@ -24,9 +24,8 @@ jobs:
         run: |
           python -m pip install --upgrade pip
           pip install -r requirements.txt
-
-      - name: SonarCloud Scan
-        uses: sonarsource/sonarcloud-github-action@c25d2e7e3def96d0d1781000d3c429da22cd6252 #v2.0.2
+          
+      - name: SonarQube Scan
+        uses: SonarSource/sonarqube-scan-action@7006c4492b2e0ee0f816d36501671557c97f5995 # v8.1.0
         env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}