diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 65c9273f..1c19075b 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -6,9 +6,9 @@ on:
   workflow_dispatch:
 
 env:
-  SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64
-  WITNESS_CREATOR_VERSION: v0.1.1
-  WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814
+  # Python of the SV-COMP execution environment (SV-COMP 2027: Ubuntu 26.04).
+  SVCOMP_PYTHON_VERSION: '3.14'
+  SVCOMP_BASE_IMAGE: docker.io/ubuntu:26.04
 
 jobs:
   build:
@@ -85,23 +85,6 @@ jobs:
         mkdir -p libs/java-library-path
         cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \
           libs/java-library-path/java-smt-latest.jar
-    - name: Download WitnessCreator runtime
-      run: |
-        version="${WITNESS_CREATOR_VERSION}"
-        zip_name="witness-creator-${version#v}.zip"
-        zip_path="${RUNNER_TEMP}/${zip_name}"
-        runtime_dir="${RUNNER_TEMP}/witness-creator-runtime"
-
-        curl --fail --location --retry 3 \
-          --output "${zip_path}" \
-          "https://github.com/SWAT-project/WitnessCreator/releases/download/${version}/${zip_name}"
-        echo "${WITNESS_CREATOR_SHA256}  ${zip_path}" | sha256sum --check -
-
-        mkdir -p "${runtime_dir}"
-        unzip -q "${zip_path}" -d "${runtime_dir}"
-        test -f "${runtime_dir}/WitnessCreator/build/libs/WitnessCreator.jar"
-        test -f "${runtime_dir}/WitnessCreator/witnesses/default_violation.st"
-        test -f "${runtime_dir}/WitnessCreator/witnesses/witness.st"
     - name: Determine release channel
       id: meta
       run: |
@@ -148,24 +131,19 @@ jobs:
         } >> "${GITHUB_OUTPUT}"
     - name: Build SV-COMP Python runtime
       env:
-        VENV_DIR: ${{ runner.temp }}/svcomp-runtime/${{ env.SVCOMP_VENV_DIR_NAME }}
-      run: |
-        mkdir -p "$(dirname "${VENV_DIR}")"
-        /usr/bin/python3 -m venv --copies "${VENV_DIR}"
-        "${VENV_DIR}/bin/python3" -m pip install --no-deps -r scripts/svcomp-package/requirements.txt
-        "${VENV_DIR}/bin/python3" -m pip check
-        "${VENV_DIR}/bin/python3" -m pip freeze --all > "${VENV_DIR}/requirements.freeze.txt"
-        "${VENV_DIR}/bin/python3" -c "import fastapi, pydantic, z3"
+        SWAT_SVCOMP_PYTHON_VERSION: ${{ env.SVCOMP_PYTHON_VERSION }}
+      run: scripts/build-svcomp-python-runtime.sh "${RUNNER_TEMP}/svcomp-python"
     - name: Pack SV-COMP ZIP
       env:
         SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }}
         SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars
-        SWAT_SVCOMP_RUNTIME_DIR: ${{ runner.temp }}/svcomp-runtime
-        SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator
+        SWAT_SVCOMP_PYTHON_DIR: ${{ runner.temp }}/svcomp-python
         SWAT_SVCOMP_COMMIT: ${{ github.sha }}
         SWAT_SVCOMP_REF: ${{ github.ref_name }}
         SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }}
       run: scripts/package-svcomp.sh
+    - name: Check SV-COMP ZIP in competition base image
+      run: scripts/check-svcomp-package.sh "build/distributions/${{ steps.meta.outputs.zip-name }}" "${SVCOMP_BASE_IMAGE}"
     - name: Upload SV-COMP ZIP artifact
       uses: actions/upload-artifact@v4
       with:
diff --git a/.gitignore b/.gitignore
index 57b3d545..486a104a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,6 +29,8 @@ targets/sv-comp/wit4java/
 /.vscode/
 **/smt_files/
 **/witness/
+# ... but not the witness packages of the executor sources
+!symbolic-executor/src/**/witness/
 **/sv-comp/results/
 **/analysis/
 !targets/sv-comp/scripts/lib/analysis
diff --git a/scripts/build-svcomp-python-runtime.sh b/scripts/build-svcomp-python-runtime.sh
new file mode 100755
index 00000000..eaf49a40
--- /dev/null
+++ b/scripts/build-svcomp-python-runtime.sh
@@ -0,0 +1,86 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Builds the Python dependency directory that ships in the SV-COMP archive as
+# libs/python/. The archive runs SymbolicExplorer with the competition
+# machine's system python3 and puts this directory first on PYTHONPATH, so no
+# virtual environment (and no absolute interpreter path) is baked into the ZIP.
+#
+# Wheels are resolved for the *target* interpreter, not the one running pip,
+# so this works on any build host (e.g. an ubuntu-24.04 CI runner building for
+# the Ubuntu 26.04 / Python 3.14 competition image).
+#
+# Usage: scripts/build-svcomp-python-runtime.sh <output-dir>
+#
+# Environment:
+#   SWAT_SVCOMP_PYTHON_VERSION  target CPython "major.minor" (default: 3.14,
+#                               the python3 of Ubuntu 26.04 / SV-COMP 2027)
+#   SWAT_SVCOMP_PIP             pip command to use (default: "python3 -m pip")
+#   SWAT_SVCOMP_WITNESSCREATOR  replaces the pinned witnesscreator requirement
+#                               (git tag) with a local source directory or
+#                               wheel, for builds against an unreleased version
+
+ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+REQUIREMENTS="${ROOT_DIR}/scripts/svcomp-package/requirements.txt"
+PY_VERSION="${SWAT_SVCOMP_PYTHON_VERSION:-3.14}"
+PIP_CMD="${SWAT_SVCOMP_PIP:-python3 -m pip}"
+OUT_DIR="${1:?usage: $0 <output-dir>}"
+
+[[ "$PY_VERSION" =~ ^3\.[0-9]+$ ]] || { echo "error: invalid SWAT_SVCOMP_PYTHON_VERSION: ${PY_VERSION}" >&2; exit 1; }
+PY_TAG="cp${PY_VERSION/./}"
+
+if [[ -e "$OUT_DIR" ]] && [[ -n "$(ls -A "$OUT_DIR")" ]]; then
+  echo "error: output directory is not empty: ${OUT_DIR}" >&2
+  exit 1
+fi
+mkdir -p "$OUT_DIR"
+
+# witnesscreator (pure Python, stdlib only) is pinned to a git tag and built from
+# source below; everything else comes as wheels for the target interpreter.
+WHEEL_REQUIREMENTS="$(mktemp "${TMPDIR:-/tmp}/swat-svcomp-requirements.XXXXXX")"
+trap 'rm -f "$WHEEL_REQUIREMENTS"' EXIT
+grep -v '^witnesscreator' "$REQUIREMENTS" > "$WHEEL_REQUIREMENTS"
+WITNESSCREATOR_REQ="${SWAT_SVCOMP_WITNESSCREATOR:-$(grep '^witnesscreator' "$REQUIREMENTS")}"
+[[ -n "$WITNESSCREATOR_REQ" ]] || { echo "error: no witnesscreator requirement in ${REQUIREMENTS}" >&2; exit 1; }
+
+# --no-deps: requirements.txt is a complete, pinned closure.
+# --only-binary: never compile on the build host (would target the wrong ABI).
+# shellcheck disable=SC2086
+$PIP_CMD install \
+  --disable-pip-version-check \
+  --no-cache-dir \
+  --no-compile \
+  --no-deps \
+  --only-binary=:all: \
+  --implementation cp \
+  --python-version "$PY_VERSION" \
+  --abi "$PY_TAG" \
+  --abi abi3 \
+  --abi none \
+  --platform manylinux_2_17_x86_64 \
+  --platform manylinux2014_x86_64 \
+  --platform manylinux_2_28_x86_64 \
+  --platform manylinux_2_34_x86_64 \
+  --platform any \
+  --target "$OUT_DIR" \
+  -r "$WHEEL_REQUIREMENTS"
+
+# Pure-Python package: built on the host, valid for any CPython >= 3.10.
+# shellcheck disable=SC2086
+$PIP_CMD install \
+  --disable-pip-version-check \
+  --no-cache-dir \
+  --no-compile \
+  --no-deps \
+  --target "$OUT_DIR" \
+  "$WITNESSCREATOR_REQ"
+
+# Console-script wrappers carry the build host's interpreter path; unused.
+rm -rf "${OUT_DIR}/bin"
+find "$OUT_DIR" -name '__pycache__' -type d -prune -exec rm -rf {} +
+
+# Non-hidden marker (BenchExec skips hidden files when collecting tool files).
+echo "$PY_VERSION" > "${OUT_DIR}/PYTHON_VERSION"
+cp "$REQUIREMENTS" "${OUT_DIR}/requirements.txt"
+
+echo "Python runtime for CPython ${PY_VERSION} written to: ${OUT_DIR}"
diff --git a/scripts/check-svcomp-package.sh b/scripts/check-svcomp-package.sh
new file mode 100755
index 00000000..129bbefb
--- /dev/null
+++ b/scripts/check-svcomp-package.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Checks an SV-COMP ZIP built by scripts/package-svcomp.sh against the archive
+# requirements (single top-level directory, LICENSE, README, smoketest.sh,
+# one-line --version) and runs it in a bare competition base image with only
+# the fm-tools required_ubuntu_packages installed, like `fm-weck smoke-test`.
+#
+# Usage: scripts/check-svcomp-package.sh <zip> [base-image]
+# Requires docker. Default base image: docker.io/ubuntu:26.04 (SV-COMP 2027).
+
+ZIP_PATH="$(realpath "${1:?usage: $0 <zip> [base-image]}")"
+BASE_IMAGE="${2:-docker.io/ubuntu:26.04}"
+# Keep in sync with required_ubuntu_packages in fm-tools data/swat.yml.
+UBUNTU_PACKAGES="python3 openjdk-17-jdk-headless"
+
+fail() {
+  echo "error: $*" >&2
+  exit 1
+}
+
+echo "ZIP: ${ZIP_PATH} ($(stat -c %s "$ZIP_PATH") bytes)"
+
+top_dirs="$(unzip -Z1 "$ZIP_PATH" | cut -d/ -f1 | sort -u)"
+[[ "$(wc -l <<< "$top_dirs")" -eq 1 ]] || fail "ZIP must have a single top-level directory, found: ${top_dirs//$'\n'/ }"
+
+check_dir="$(mktemp -d "${TMPDIR:-/tmp}/swat-svcomp-check.XXXXXX")"
+unzip -q "$ZIP_PATH" -d "$check_dir"
+tool_dir="${check_dir}/${top_dirs}"
+for f in LICENSE README.md smoketest.sh run-swat.sh libs/python/PYTHON_VERSION; do
+  [[ -f "${tool_dir}/${f}" ]] || fail "missing ${f} in archive root ${top_dirs}/"
+done
+[[ -x "${tool_dir}/run-swat.sh" && -x "${tool_dir}/smoketest.sh" ]] || fail "run-swat.sh and smoketest.sh must be executable"
+
+echo "Running checks in ${BASE_IMAGE} (packages: ${UBUNTU_PACKAGES})"
+docker run --rm -v "${tool_dir}:/tool" -w /tool -e UBUNTU_PACKAGES="$UBUNTU_PACKAGES" "$BASE_IMAGE" bash -euc '
+  apt-get update -qq
+  DEBIAN_FRONTEND=noninteractive apt-get install -y -qq --no-install-recommends $UBUNTU_PACKAGES > /dev/null
+  echo "python3: $(python3 --version)"
+  echo "java: $(java -version 2>&1 | head -n 1)"
+  PYTHONPATH=libs/python python3 -c "import fastapi, pydantic, uvicorn, requests, yaml, z3, witnesscreator; print(\"z3:\", z3.get_version_string())"
+  version="$(./run-swat.sh --version)"
+  echo "version: ${version}"
+  [ -n "$version" ] && [ "$(printf "%s\n" "$version" | wc -l)" -eq 1 ] || { echo "error: --version must print one non-empty line" >&2; exit 1; }
+  [ "$(./run-swat.sh -v)" = "$version" ] || { echo "error: -v and --version differ" >&2; exit 1; }
+  ./smoketest.sh > smoketest.out 2>&1 || { cat smoketest.out; exit 1; }
+  echo "smoketest stdout: $(wc -c < smoketest.out) bytes"
+  [ -f witness/witness.yml ] && [ -f witness/witness.graphml ] || { echo "error: smoketest left no witness/witness.yml + witness.graphml" >&2; exit 1; }
+  tail -n 1 smoketest.out
+'
+echo "SV-COMP package check passed."
diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh
index c3a5e788..edf95e5e 100755
--- a/scripts/package-svcomp.sh
+++ b/scripts/package-svcomp.sh
@@ -10,18 +10,10 @@ set -euo pipefail
 #
 # - symbolic-executor/lib/symbolic-executor.jar
 #
-# Set SWAT_SVCOMP_WITNESS_CREATOR_DIR to the extracted WitnessCreator runtime
-# root from https://github.com/SWAT-project/WitnessCreator. The root must
-# contain:
-#
-# - build/libs/WitnessCreator.jar
-# - witnesses/default_violation.st
-# - witnesses/witness.st
-#
-# Set SWAT_SVCOMP_RUNTIME_DIR to a runtime package root that contains the
-# pinned SV-COMP Python environment:
-#
-# - .venv_ubuntu_24_04_1__x86_64/
+# Set SWAT_SVCOMP_PYTHON_DIR to the Python dependency directory produced by
+# scripts/build-svcomp-python-runtime.sh (it includes the witnesscreator
+# package that writes the witnesses). It is shipped as libs/python/ and used
+# with the competition machine's system python3 (no bundled venv).
 #
 # Z3 and JavaSMT are taken from the vendored files in this repository.
 #
@@ -38,19 +30,13 @@ PACKAGE_DIR="${WORK_DIR}/${PACKAGE_NAME}"
 DIST_DIR="${ROOT_DIR}/build/distributions"
 SUPPORT_DIR="${ROOT_DIR}/scripts/svcomp-package"
 ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)"
-RUNTIME_DIR="${SWAT_SVCOMP_RUNTIME_DIR:-${SWAT_SVCOMP_REFERENCE_DIR:-}}"
-WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_DIR:-}"
-VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}"
+PYTHON_DIR="${SWAT_SVCOMP_PYTHON_DIR:-}"
 LINUX_Z3_DIST="z3-4.15.4-x64-glibc-2.39"
 LINUX_Z3_ZIP="${ROOT_DIR}/libs/${LINUX_Z3_DIST}.zip"
 JAVA_SMT_JAR="${ROOT_DIR}/libs/java-library-path/java-smt-latest.jar"
 
-if [[ -n "$RUNTIME_DIR" ]]; then
-  RUNTIME_DIR="$(cd "$RUNTIME_DIR" && pwd)"
-fi
-
-if [[ -n "$WITNESS_CREATOR_DIR" ]]; then
-  WITNESS_CREATOR_DIR="$(cd "$WITNESS_CREATOR_DIR" && pwd)"
+if [[ -n "$PYTHON_DIR" ]]; then
+  PYTHON_DIR="$(cd "$PYTHON_DIR" && pwd)"
 fi
 
 fail() {
@@ -143,12 +129,6 @@ copy_artifact_file "$EXECUTOR_JAR" "$PACKAGE_DIR/symbolic-executor/lib/symbolic-
 
 copy_tree_files symbolic-explorer "$PACKAGE_DIR/symbolic-explorer"
 
-[[ -n "$WITNESS_CREATOR_DIR" ]] || fail "SWAT_SVCOMP_WITNESS_CREATOR_DIR must point to the extracted WitnessCreator runtime root"
-[[ -f "$WITNESS_CREATOR_DIR/build/libs/WitnessCreator.jar" ]] || fail "missing WitnessCreator JAR: ${WITNESS_CREATOR_DIR}/build/libs/WitnessCreator.jar"
-[[ -f "$WITNESS_CREATOR_DIR/witnesses/default_violation.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/default_violation.st"
-[[ -f "$WITNESS_CREATOR_DIR/witnesses/witness.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/witness.st"
-copy_artifact_tree "$WITNESS_CREATOR_DIR" "$PACKAGE_DIR/WitnessCreator"
-
 install_z3_runtime_file z3 0755
 install_z3_runtime_file libz3.so
 install_z3_runtime_file libz3java.so
@@ -159,8 +139,10 @@ copy_artifact_file "$JAVA_SMT_JAR" "$PACKAGE_DIR/libs/java-library-path/java-smt
 
 copy_tree_files "$SUPPORT_DIR/smoketest" "$PACKAGE_DIR/smoketest"
 
-[[ -n "$RUNTIME_DIR" ]] || fail "SWAT_SVCOMP_RUNTIME_DIR must point to a runtime package root containing ${VENV_DIR_NAME}"
-copy_artifact_tree "${RUNTIME_DIR}/${VENV_DIR_NAME}" "${PACKAGE_DIR}/${VENV_DIR_NAME}"
+[[ -n "$PYTHON_DIR" ]] || fail "SWAT_SVCOMP_PYTHON_DIR must point to the output of scripts/build-svcomp-python-runtime.sh"
+[[ -f "$PYTHON_DIR/PYTHON_VERSION" ]] || fail "missing ${PYTHON_DIR}/PYTHON_VERSION; build it with scripts/build-svcomp-python-runtime.sh"
+[[ -d "$PYTHON_DIR/witnesscreator" ]] || fail "missing witnesscreator package in ${PYTHON_DIR}; build it with scripts/build-svcomp-python-runtime.sh"
+copy_artifact_tree "$PYTHON_DIR" "${PACKAGE_DIR}/libs/python"
 
 mkdir -p "$DIST_DIR"
 ZIP_PATH="${DIST_DIR}/${PACKAGE_NAME}.zip"
diff --git a/scripts/svcomp-package/README.md b/scripts/svcomp-package/README.md
index 46852fdf..bf7fc7e2 100644
--- a/scripts/svcomp-package/README.md
+++ b/scripts/svcomp-package/README.md
@@ -4,13 +4,21 @@ This archive contains a runnable SWAT package for SV-COMP style Java verificatio
 
 Important entry points:
 
-- `run-swat.sh`: verifier entry point used by BenchExec.
+- `run-swat.sh`: verifier entry point used by BenchExec (`run-swat.sh --version`
+  or `-v` prints the version).
 - `compile-target.sh`: helper used by `run_swat.py` to compile Java benchmark sources.
-- `smoketest.sh`: runs SWAT on two bundled smoke-test targets.
+- `smoketest.sh`: runs SWAT on the bundled smoke-test target.
 - `sv-comp.cfg`: SWAT configuration for SV-COMP mode.
 
-The package expects Java 17 and the bundled `.venv_ubuntu_24_04_1__x86_64`
-Python environment. `run-swat.sh` intentionally uses only that environment.
+Requirements (SV-COMP 2027 environment, Ubuntu 26.04): `python3` (3.14) and
+Java 17 (`openjdk-17-jdk-headless`, which also provides `javac`).
+
+All Python dependencies are bundled in `libs/python/` and are used with the
+system `python3`; no virtual environment is needed. They are built for the
+Python version recorded in `libs/python/PYTHON_VERSION`, and `run-swat.sh`
+refuses to start with a different one. Set `SWAT_PYTHON` to use another
+interpreter of that version. The full tool log of the last run is in `out.log`;
+stdout is truncated if it would exceed SV-COMP's output limit.
 
 Example:
 
diff --git a/scripts/svcomp-package/requirements.txt b/scripts/svcomp-package/requirements.txt
index 5c32b0a4..b4eb8467 100644
--- a/scripts/svcomp-package/requirements.txt
+++ b/scripts/svcomp-package/requirements.txt
@@ -1,19 +1,21 @@
+annotated-doc==0.0.4
 annotated-types==0.7.0
-anyio==4.6.2.post1
-boto==2.49.0
-certifi==2025.11.12
+anyio==4.12.1
+certifi==2026.1.4
 charset-normalizer==3.4.4
-click==8.1.7
-fastapi==0.115.5
-h11==0.14.0
-idna==3.10
-pydantic==2.10.0
-pydantic_core==2.27.0
-PyYAML==6.0.2
+click==8.3.1
+fastapi==0.128.0
+h11==0.16.0
+idna==3.11
+pydantic==2.12.5
+pydantic_core==2.41.5
+PyYAML==6.0.3
 requests==2.32.5
 sniffio==1.3.1
-starlette==0.41.3
-typing_extensions==4.12.2
-urllib3==2.5.0
-uvicorn==0.32.1
+starlette==0.50.0
+typing-inspection==0.4.2
+typing_extensions==4.15.0
+urllib3==2.6.3
+uvicorn==0.40.0
+witnesscreator @ git+https://github.com/SWAT-project/WitnessCreator@v1.0.0
 z3-solver==4.15.4.0
diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh
index 424a3188..a10bb7b5 100755
--- a/scripts/svcomp-package/run-swat.sh
+++ b/scripts/svcomp-package/run-swat.sh
@@ -1,17 +1,13 @@
 #!/bin/bash
 
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
 
-# Check if the '-v' argument is among the arguments, indicating that the user wants to see the version
+# '-v' is what the BenchExec tool-info module passes; '--version' is the
+# SV-COMP archive convention. Both print a single version line.
 for arg in "$@"
 do
-  # Check if '-v' is among the arguments
-  if [ "$arg" == "-v" ]; then
-    # Execute the Java command with base dir of this script
-    pushd "$(dirname "$0")" > /dev/null
-    java -cp ./symbolic-executor/lib/symbolic-executor.jar de.uzl.its.swat.Version
-    popd > /dev/null
-    # Exit with status 0
-    exit 0
+  if [ "$arg" == "-v" ] || [ "$arg" == "--version" ]; then
+    exec java -cp "$SCRIPT_DIR/symbolic-executor/lib/symbolic-executor.jar" de.uzl.its.swat.Version
   fi
 done
 
@@ -27,46 +23,41 @@ if [ -f "$second_last_path/Main.java" ]; then
     set -- "${@:1:$(($#-2))}" "$last_path" "$second_last_path"
 fi
 
-# Loop through all provided paths and copy Java files preserving directory structure
-for path in "$@"; do
-  if [ -d "$path" ]; then
-    # Find all Java files and preserve relative directory structure
-    find "$path" -type f -name "*.java" | while read src; do
-      rel_path="${src#$path/}"
-      dst_dir="./WitnessCreator/$(dirname "$rel_path")"
-      mkdir -p "$dst_dir"
-      cp "$src" "$dst_dir/"
-    done
-    echo "Java files from $path copied successfully to ./WitnessCreator/"
-  elif [ -f "$path" ] && [[ "$path" == *.java ]]; then
-    # If the argument is a single Java file, copy it
-    cp "$path" ./WitnessCreator/
-    echo "File $path copied successfully to ./WitnessCreator/"
-  fi
-done
-
-# # copy Main.java for Witness creation
-# last_path="${@: -1}"
-# file_to_copy="${last_path}/Main.java"
-#
-# # Check if the file exists
-# if [ -f "$file_to_copy" ]; then
-#     # Copy the Main.java file to the current directory
-#     cp "$file_to_copy" ./WitnessCreator/.
-#     echo "File copied successfully to ./WitnessCreator/"
-# else
-#     echo "Error: File not found."
-# fi
-
-
-SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
-VENV_PYTHON="$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/python3"
-
-if [ ! -x "$VENV_PYTHON" ]; then
-    echo "Error: Python runtime not found at $VENV_PYTHON"
+# The violation witness is written by the explorer to witness/ from the given input paths.
+
+# Python dependencies are shipped in libs/python (built for one CPython
+# minor version, recorded in libs/python/PYTHON_VERSION) and used with the
+# system python3. Override the interpreter with SWAT_PYTHON if needed.
+PYTHON="${SWAT_PYTHON:-python3}"
+PYTHON_LIBS="$SCRIPT_DIR/libs/python"
+expected_py="$(cat "$PYTHON_LIBS/PYTHON_VERSION" 2>/dev/null)"
+actual_py="$("$PYTHON" -c 'import sys; print("%d.%d" % sys.version_info[:2])' 2>/dev/null)"
+if [ -z "$expected_py" ]; then
+    echo "Error: Python dependencies not found at $PYTHON_LIBS"
     exit 1
 fi
+if [ "$actual_py" != "$expected_py" ]; then
+    echo "Error: SWAT's Python dependencies were built for Python $expected_py, but '$PYTHON' is '${actual_py:-not runnable}'"
+    exit 1
+fi
+export PYTHONPATH="$PYTHON_LIBS${PYTHONPATH:+:$PYTHONPATH}"
+export PYTHONNOUSERSITE=1
 
 echo "Running SWAT with arguments: $@"
-"$VENV_PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1
-cat out.log
+"$PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1
+
+# SV-COMP requires tool output below 2 MB. Long explorations can log far more,
+# so past the cap print the head, every verdict line, and the tail (which holds
+# the final verdict and witness). The full log stays in out.log.
+MAX_STDOUT_BYTES=$((1536 * 1024))
+log_size="$(stat -c %s out.log)"
+if [ "$log_size" -le "$MAX_STDOUT_BYTES" ]; then
+    cat out.log
+else
+    head -c $((256 * 1024)) out.log
+    echo
+    echo "[run-swat.sh] output truncated: ${log_size} bytes total; verdict lines and tail follow"
+    grep -F '[VERDICT ' out.log | head -n 200 | cut -c1-500
+    echo "[run-swat.sh] ... tail ..."
+    tail -c $((1024 * 1024)) out.log
+fi
diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py
index 6b883330..dbeda389 100755
--- a/scripts/svcomp-package/run_swat.py
+++ b/scripts/svcomp-package/run_swat.py
@@ -1,5 +1,5 @@
 from contextlib import contextmanager
-import logging, os, enum, subprocess, sys, base64, uuid
+import logging, os, enum, shutil, subprocess, sys, uuid
 
 import concurrent.futures, json, datetime
 from typing import List, Optional
@@ -7,7 +7,10 @@
 logging.basicConfig(level=logging.INFO)
 logger = logging.getLogger(__name__)
 SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__))
-WITNESS_PATH = os.path.join(SCRIPT_DIR, 'WitnessCreator/build/libs/WitnessCreator.jar')
+ORIGINAL_CWD = os.getcwd()
+# The explorer writes the violation witness (witness.yml, witness.graphml) here; BenchExec collects
+# it via the `**/witness.*` result-files pattern of the benchmark definition.
+WITNESS_DIR = os.path.join(SCRIPT_DIR, 'witness')
 
 
 class ExecutionStatus(enum.Enum):
@@ -93,7 +96,9 @@ def run_command_with_timeout(cmd: list[str], timeout: int | None = None) -> tupl
 
 
 
-def generate_command(args, property_file: str):
+def generate_command(args, property_file: str, property_path: str, input_paths: List[str]):
+    """The explorer command; `property_path` and `input_paths` are the verifier's arguments as given
+    by BenchExec (relative to the original working directory) and end up in the witness."""
     config_file = 'sv-comp.cfg'
 
     agent_path = os.path.join(SCRIPT_DIR, 'symbolic-executor', 'lib', 'symbolic-executor.jar')
@@ -101,9 +106,8 @@ def generate_command(args, property_file: str):
     library_path = os.path.join(SCRIPT_DIR, 'libs', 'java-library-path')
     logging_dir =  os.path.join(SCRIPT_DIR, 'logs')
 
-    python3_path = os.path.join(SCRIPT_DIR, '.venv_ubuntu_24_04_1__x86_64/bin/python3')
-
-    base_command = [ python3_path, "-u", os.path.join(SCRIPT_DIR, 'symbolic-explorer', 'SymbolicExplorer.py'),
+    # Same interpreter (and PYTHONPATH, via the inherited environment) as run-swat.sh set up.
+    base_command = [ sys.executable, "-u", os.path.join(SCRIPT_DIR, 'symbolic-explorer', 'SymbolicExplorer.py'),
                      "-prp", property_file,
                      "--agent", agent_path,
                      "--config", config_path,
@@ -111,6 +115,11 @@ def generate_command(args, property_file: str):
                      "--logdir", logging_dir,
                      "--mode", "sv-comp",
                      '--port', "8000",
+                     "--witness-dir", WITNESS_DIR,
+                     "--witness-property", property_path,
+                     "--witness-base-dir", ORIGINAL_CWD,
+                     "--producer-version", swat_version(),
+                     "--witness-input", *input_paths,
                      "--classpath"]
     print("CP args: " + str(args))
     for arg in args[1:]:
@@ -145,30 +154,40 @@ def extract_last_round(out, marker="============================== ROUND"):
     return "\n ".join(out).split(marker)[-1]
 
 
-def extract_markers(out, marker):
+def extract_markers(out, markers):
+    if isinstance(markers, str):
+        markers = (markers,)
     res = []
     for line in out.split("\n"):
-        print(line)
-        if marker in line:
+        if any(marker in line for marker in markers):
             res.append(line)
     return res
 
-def generate_witness(witness):
-    witness_dir = os.path.join(SCRIPT_DIR, 'WitnessCreator/')
-    with pushd(witness_dir):
-        # base64 encode the string
-        enc = base64.b64encode(witness.encode())
-        cmd = [
-            'java',
-            '-jar',
-            WITNESS_PATH,
-            enc,
-            witness_dir
-        ]
-        print(cmd)
-        _, output = run_command_with_timeout(cmd)
-        print("WITNESS CREATED")
-        print(output)
+def swat_version():
+    """The package version from BUILD_INFO.txt, written by scripts/package-svcomp.sh."""
+    try:
+        with open(os.path.join(SCRIPT_DIR, 'BUILD_INFO.txt')) as f:
+            for line in f:
+                if line.startswith('version='):
+                    return line[len('version='):].strip()
+    except OSError:
+        pass
+    return 'unknown'
+
+def print_witness():
+    """Print the witness file contents for validation on the benchmark server."""
+    witness_file_path = os.path.join(WITNESS_DIR, 'witness.yml')
+    if os.path.exists(witness_file_path):
+        print("\n" + "="*80)
+        print("WITNESS FILE CONTENTS:")
+        print("="*80)
+        with open(witness_file_path, 'r') as f:
+            print(f.read())
+        print("="*80)
+        print("END OF WITNESS FILE")
+        print("="*80 + "\n")
+    else:
+        print(f"WARNING: Witness file not found at {witness_file_path}")
 
 def log_output(output: List[str]):
     for line in output:
@@ -180,9 +199,11 @@ def log_output(output: List[str]):
     # Look for property file in arguments
     # SV-COMP framework passes the .prp file directly as first argument
     property_file = None
+    property_path = None
     for arg in sys.argv[1:]:
         if arg.endswith('.prp'):
             property_file = os.path.basename(arg)
+            property_path = arg
             logger.info(f"Found property file in arguments: {property_file}")
             break
 
@@ -193,8 +214,13 @@ def log_output(output: List[str]):
 
     logger.info(f"Using property file: {property_file}")
 
+    # The task's input files/directories, as given (everything but the property file)
+    input_paths = [arg for arg in sys.argv[1:] if arg != property_path]
+
     target_dir = sys.argv[-1]
-    cmd = generate_command(sys.argv[1:], property_file)
+    cmd = generate_command(sys.argv[1:], property_file, property_path, input_paths)
+    # Exactly one witness per run: drop whatever an earlier run left behind
+    shutil.rmtree(WITNESS_DIR, ignore_errors=True)
     local_target_dir = copy_target(target_dir)
     compile_target(sys.argv[1:], local_target_dir)
 
@@ -218,22 +244,6 @@ def log_output(output: List[str]):
         out = extract_last_round(output)
         verdict = extract_markers(out, f'[VERDICT {property_file}]')
         if "== ERROR" in str(verdict):
-            witnesses = extract_markers(out, '[WITNESS]')
-            generate_witness("\n".join(witnesses))
-            print(f'Witnesses:\n {witnesses}')
-
-            # Print the generated witness file contents for validation on benchmark server
-            witness_file_path = os.path.join(SCRIPT_DIR, 'WitnessCreator', 'witness.graphml')
-            if os.path.exists(witness_file_path):
-                print("\n" + "="*80)
-                print("WITNESS FILE CONTENTS:")
-                print("="*80)
-                with open(witness_file_path, 'r') as f:
-                    witness_content = f.read()
-                    print(witness_content)
-                print("="*80)
-                print("END OF WITNESS FILE")
-                print("="*80 + "\n")
-            else:
-                print(f"WARNING: Witness file not found at {witness_file_path}")
+            # The explorer wrote the witness from the trace of the violating execution
+            print_witness()
         print(f'Verdict:\n {verdict}')
\ No newline at end of file
diff --git a/scripts/svcomp-package/smoketest.sh b/scripts/svcomp-package/smoketest.sh
index 95fb8c05..22228fae 100755
--- a/scripts/svcomp-package/smoketest.sh
+++ b/scripts/svcomp-package/smoketest.sh
@@ -1,12 +1,19 @@
 #!/bin/bash
 
 cd "$(dirname "$0")"
+rm -rf witness
 output="$("bash" "run-swat.sh" "../../sv-benchmarks/java/properties/valid-assert.prp" "smoketest/common" "smoketest")"
-if echo "$output" | grep -q "\[VERDICT valid-assert.prp\] == ERROR"; then
-    echo "Smoketest passed!"
-    exit 0
-else
-    echo "Smoketest failed!"
+if ! echo "$output" | grep -q "\[VERDICT valid-assert.prp\] == ERROR"; then
+    echo "Smoketest failed: no violation verdict!"
     exit 1
 fi
+# The violation must come with a YAML witness (format 2.3) with a target waypoint, written by
+# the explorer to witness/witness.yml
+if ! grep -q 'entry_type: "violation_sequence"' witness/witness.yml 2>/dev/null \
+    || ! grep -q 'type: "target"' witness/witness.yml; then
+    echo "Smoketest failed: no violation witness with a target waypoint in witness/witness.yml!"
+    exit 1
+fi
+echo "Smoketest passed!"
+exit 0
 
diff --git a/symbolic-executor/build.gradle b/symbolic-executor/build.gradle
index 94841476..3abdf970 100644
--- a/symbolic-executor/build.gradle
+++ b/symbolic-executor/build.gradle
@@ -50,10 +50,12 @@ test {
     systemProperty "java.library.path", "../libs/java-library-path"
     // Surface SWAT errors as exceptions instead of halting the test JVM
     systemProperty "exitOnError", "false"
-    
+
     useJUnitPlatform {
         excludeTags "slow"   // skip @Tag("slow") tests
     }
+    // Forked-agent specs need the built agent jar; they run via agentTest
+    exclude '**/*AgentSpec*'
 
     testLogging {
         // Show events for passed, skipped, and failed tests
@@ -63,6 +65,22 @@ test {
     }
 }
 
+// Forked-agent tests: run a small target with the real agent (solver.mode=PRINT) and check the
+// TraceDTO printed to stdout. Needs the agent jar in lib/, hence the copyJar dependency.
+tasks.register('agentTest', Test) {
+    dependsOn copyJar
+    description = 'Runs the *AgentSpec tests against the built agent jar'
+    group = 'verification'
+    useJUnitPlatform()
+    filter {
+        includeTestsMatching '*AgentSpec'
+    }
+    testLogging {
+        events "passed", "failed", "skipped"
+        showStandardStreams = false
+    }
+}
+
 tasks.register('testFull', Test) {
     systemProperty "java.library.path", "../libs/java-library-path"
     // Surface SWAT errors as exceptions instead of halting the test JVM
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java
index 48061c8f..f280c9ba 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java
@@ -4,7 +4,9 @@
 import com.sap.fontus.taintaware.unified.IASString;
 import de.uzl.its.swat.common.ErrorHandler;
 import de.uzl.its.swat.common.PrintBox;
+import com.fasterxml.jackson.core.JsonProcessingException;
 import de.uzl.its.swat.common.exceptions.NoThreadContextException;
+import de.uzl.its.swat.common.exceptions.NotImplementedException;
 import de.uzl.its.swat.common.exceptions.SWATAssert;
 import de.uzl.its.swat.common.exceptions.SWATException;
 import de.uzl.its.swat.common.exceptions.ThreadAlreadyDisabledException;
@@ -138,7 +140,7 @@ public static void terminate() {
                     break;
                 case PRINT:
                     if (!ThreadHandler.isThreadContextAborted(currentThread().getId())) {
-                        System.out.println(ThreadHandler.getSymbolicVisitor(currentThread().getId()).getSymbolicTraceHandler().getTraceDTO(ThreadHandler.getStatsStorage(currentThread().getId())));
+                        printTrace(currentThread().getId());
                     }
                     break;
                 case NONE:
@@ -162,6 +164,44 @@ public static void terminate() {
         }
     }
 
+    private static void printTrace(long threadId) throws NoThreadContextException, NotImplementedException, JsonProcessingException {
+        System.out.println(ThreadHandler.getSymbolicVisitor(threadId).getSymbolicTraceHandler().getTraceDTO(ThreadHandler.getStatsStorage(threadId), threadId));
+    }
+
+    /**
+     * Sends (HTTP) or prints (PRINT) the traces of target threads whose symbolic execution is still
+     * active when the JVM shuts down, i.e. the target ended the run abruptly (System.exit) before
+     * reaching the instrumented end of its entry method. Executions that terminated normally have
+     * removed their context already, so this is a no-op for them. Runs in the shutdown hook
+     * registered by the Transformer, hence on another thread than the target; errors are logged
+     * only.
+     */
+    public static void terminateOnShutdown() {
+        for (long threadId : ThreadHandler.getActiveThreadContextIds()) {
+            try {
+                logger.warn(
+                        "JVM shutdown with an active symbolic execution (thread {}), e.g. System.exit in the target: sending its trace",
+                        threadId);
+                ThreadHandler.disableThreadContext(threadId);
+                if (ThreadHandler.isThreadContextAborted(threadId)) {
+                    continue;
+                }
+                switch (config.getSolverMode()) {
+                    case HTTP:
+                        ThreadHandler.sendData(threadId);
+                        break;
+                    case PRINT:
+                        printTrace(threadId);
+                        break;
+                    default:
+                        break;
+                }
+            } catch (Throwable t) {
+                logger.error("Error sending the trace of thread {} on shutdown", threadId, t);
+            }
+        }
+    }
+
     public static void retrieveAssignments() {
         PrintBox printBox = new PrintBox(60, "Retrieving assignments");
         System.getProperties().forEach((key, value) -> {
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java
index 149e4855..bb29b91e 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java
@@ -37,6 +37,8 @@ public abstract class Transformer implements ClassFileTransformer {
     static {
         // register the hook as early as possible
         Runtime.getRuntime().addShutdownHook(new Thread(() -> {
+            // A target that ends the JVM abruptly (System.exit) must not lose its trace
+            Intrinsics.terminateOnShutdown();
             LoggerContext lc = (LoggerContext) LoggerFactory.getILoggerFactory();
             // this will flush and close all appenders (including your buffered FileAppender)
             lc.stop();
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java
index 8ed69119..798cac83 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java
@@ -1,6 +1,8 @@
 package de.uzl.its.swat.instrument.svcomp;
 
 import de.uzl.its.swat.common.Util;
+import java.util.HashMap;
+import java.util.Map;
 import org.objectweb.asm.ClassVisitor;
 import org.objectweb.asm.MethodVisitor;
 import org.objectweb.asm.Opcodes;
@@ -15,6 +17,15 @@ public class SVCompClassAdapter extends ClassVisitor {
 
     private final String cname;
 
+    /**
+     * Number of nondet calls seen so far per source line of this class. Shared by all method
+     * adapters so that the witness can tell apart several nondet calls on one line.
+     */
+    private final Map<Integer, Integer> nondetCallsPerLine = new HashMap<>();
+
+    /** The source file name of the class (SourceFile attribute), empty if unknown. */
+    private String sourceFile = "";
+
     /**
      * Constructor that calls the super from the default ClassVisitor
      *
@@ -25,6 +36,14 @@ public SVCompClassAdapter(ClassVisitor cv, String cname) {
         this.cname = cname;
     }
 
+    @Override
+    public void visitSource(String source, String debug) {
+        if (source != null) {
+            sourceFile = source;
+        }
+        super.visitSource(source, debug);
+    }
+
     /**
      * Visits a method of the class. This method must return a new MethodVisitor instance (or null)
      * each time it is called, i.e., it should not return a previously returned visitor. Addition:
@@ -55,7 +74,8 @@ public MethodVisitor visitMethod(
 
         if (!cname.equals("org/sosy_lab/sv_benchmarks/Verifier")) {
             SVCompTransformer.getPrintBox().addMsg("Method: " + name);
-            return new SVCompMethodAdapter(access, mv, cname, name, desc);
+            return new SVCompMethodAdapter(
+                    access, mv, cname, name, desc, sourceFile, nondetCallsPerLine);
         }
         return mv;
     }
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java
index df2a3877..e0471e47 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java
@@ -3,6 +3,8 @@
 import de.uzl.its.swat.instrument.InternalTransformerType;
 import de.uzl.its.swat.instrument.Intrinsics;
 import de.uzl.its.swat.instrument.Transformer;
+import java.util.Map;
+import java.util.Set;
 import org.objectweb.asm.Label;
 import org.objectweb.asm.MethodVisitor;
 import org.objectweb.asm.Opcodes;
@@ -16,6 +18,12 @@ public class SVCompMethodAdapter extends LocalVariablesSorter {
     private final String cname;
     private final String name;
     private final String desc;
+    private final String sourceFile;
+    private final Map<Integer, Integer> nondetCallsPerLine;
+
+    /** Return type descriptors of the nondet methods whose values are recorded for the witness. */
+    private static final Set<String> WITNESS_VALUE_TYPES =
+            Set.of("Z", "B", "S", "C", "I", "J", "F", "D", "Ljava/lang/String;");
 
     int lineNumber = 0;
     /**
@@ -24,14 +32,25 @@ public class SVCompMethodAdapter extends LocalVariablesSorter {
      * @param mv Parent MethodVisitor
      * @param name The method name
      * @param desc A string description of the parameters of the method
+     * @param sourceFile The source file name of the class (empty if unknown)
+     * @param nondetCallsPerLine Per-class counter of nondet calls per source line (shared between
+     *     the methods of the class)
      */
     public SVCompMethodAdapter(
-            int access, MethodVisitor mv, String cname, String name, String desc) {
+            int access,
+            MethodVisitor mv,
+            String cname,
+            String name,
+            String desc,
+            String sourceFile,
+            Map<Integer, Integer> nondetCallsPerLine) {
         super(Opcodes.ASM9, access, desc, mv);
         identifier = cname + "/" + name;
         this.desc = desc;
         this.cname = cname;
         this.name = name;
+        this.sourceFile = sourceFile;
+        this.nondetCallsPerLine = nondetCallsPerLine;
     }
 
     @Override
@@ -58,28 +77,39 @@ public void visitMethodInsn(
 
             String retType = descriptor.split("\\)")[1];
             long nextId = Verifier.getNextId();
+            // Index of this call among the nondet calls on the same source line (bytecode order
+            // follows the left-to-right evaluation order); lets the witness locate the call.
+            int callIndex = nondetCallsPerLine.merge(lineNumber, 1, Integer::sum) - 1;
             SVCompTransformer.getPrintBox().setContentPresent(true);
             SVCompTransformer.getPrintBox()
                     .addMsg("    => Found " + name + " in line " + lineNumber);
             SVCompTransformer.getPrintBox().addMsg("      => Assigning ID: " + nextId);
             mv.visitLdcInsn(nextId);
             mv.visitMethodInsn(opcode, newOwner, name, newDescriptor, isInterface);
-            if (retType.equals("D") || retType.equals("J")) {
-                visitInsn(Opcodes.DUP2);
-            } else {
-                visitInsn(Opcodes.DUP);
+            if (WITNESS_VALUE_TYPES.contains(retType)) {
+                // Record the returned value with the call location for the witness (trace data)
+                if (retType.equals("D") || retType.equals("J")) {
+                    visitInsn(Opcodes.DUP2);
+                } else {
+                    visitInsn(Opcodes.DUP);
+                }
+                mv.visitLdcInsn(name);
+                mv.visitLdcInsn(cname);
+                mv.visitLdcInsn(this.name + this.desc);
+                mv.visitLdcInsn(sourceFile);
+                mv.visitLdcInsn(lineNumber);
+                mv.visitLdcInsn(callIndex);
+                mv.visitMethodInsn(
+                        Opcodes.INVOKESTATIC,
+                        "de/uzl/its/swat/witness/Witness",
+                        "recordValue",
+                        "("
+                                + retType
+                                + "Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;II)V",
+                        false);
+                SVCompTransformer.getPrintBox().addMsg("      => Adding Witness recording");
             }
-            mv.visitLdcInsn(lineNumber);
-            mv.visitLdcInsn(cname);
-            mv.visitLdcInsn(this.name + this.desc);
-            mv.visitMethodInsn(
-                    Opcodes.INVOKESTATIC,
-                    "de/uzl/its/swat/witness/Witness",
-                    "recordValue",
-                    "(" + descriptor.substring(2) + "ILjava/lang/String;Ljava/lang/String;)V",
-                    false);
             mv.visitLdcInsn(nextId);
-            SVCompTransformer.getPrintBox().addMsg("      => Adding Witness recording");
             /*
             if (descriptor.equals("()D") || descriptor.equals("()J")) {
                 visitInsn(Opcodes.DUP2);
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java
index bc59a3f2..5d74772a 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java
@@ -67,8 +67,13 @@ private void addEndOfSurrounding() {
 
         visitInsn(Opcodes.DUP);
 
+        // Prints the stack trace and records the violating location for the witness
         visitMethodInsn(
-                Opcodes.INVOKEVIRTUAL, "java/lang/Throwable", "printStackTrace", "()V", false);
+                Opcodes.INVOKESTATIC,
+                "de/uzl/its/swat/witness/Witness",
+                "recordTarget",
+                "(Ljava/lang/Throwable;)V",
+                false);
 
         // Duplicate exception for instanceof check
         visitInsn(Opcodes.DUP);
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java
index e1156b95..c773811b 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java
@@ -16,6 +16,7 @@
 import de.uzl.its.swat.coverage.InstrCoverage;
 import de.uzl.its.swat.symbolic.trace.dto.*;
 import de.uzl.its.swat.thread.ThreadHandler;
+import de.uzl.its.swat.witness.Witness;
 import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.List;
@@ -35,10 +36,12 @@ class DTOBuilder {
      * Encodes the symbolic trace as a JSON string.
      *
      * @param symbolicTrace The symbolic trace to be encoded.
+     * @param statsStorage The per-execution statistics of the thread.
+     * @param threadId The thread whose solver context the formulas belong to.
      * @return The symbolic trace encoded as a JSON string.
      */
-    protected static String encodeTrace(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
-        return buildRequestBody(buildTraceDTO(symbolicTrace, statsStorage));
+    protected static String encodeTrace(SymbolicTrace symbolicTrace, StatsStorage statsStorage, long threadId) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
+        return buildRequestBody(buildTraceDTO(symbolicTrace, statsStorage, threadId));
     }
 
     /**
@@ -74,13 +77,13 @@ private static ArrayList<InvocationDTO> buildMissingInvocations(StatsStorage sta
      * @return A {@link TraceDTO ConstraintDTO} that contains relevant all relevant information
      *     to transfer symbolic traces
      */
-    private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, NotImplementedException {
+    private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage statsStorage, long threadId) throws NoThreadContextException, NotImplementedException {
         ArrayList<InputDTO> inputs = new ArrayList<>();
         ArrayList<UFDTO> ufs = new ArrayList<>();
         ArrayList<BranchDTO> trace = new ArrayList<>();
 
         FormulaManager fmgr =
-                ThreadHandler.getSolverContext(currentThread().getId()).getFormulaManager();
+                ThreadHandler.getSolverContext(threadId).getFormulaManager();
         for (InputElement ie : symbolicTrace.getInputs()) {
             String lowerBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(false)));
             String upperBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(true)));
@@ -134,7 +137,7 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage
                 trace.add(new BranchDTO(se.getIid(), se.getInst()));
             }
         }
-        return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange());
+        return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), Witness.getNondetReturns(), Witness.getViolation(), symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange());
     }
 
     protected static String encodeCoverage(InstrCoverage instrCoverage) throws JsonProcessingException {
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java
index 02119155..539abc72 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java
@@ -110,7 +110,15 @@ public List<BooleanFormula> getConstraints() {
      * @return The symbolic trace encoded as a JSON string.
      */
     public String getTraceDTO(StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
-        return DTOBuilder.encodeTrace(symbolicTrace, statsStorage);
+        return DTOBuilder.encodeTrace(symbolicTrace, statsStorage, Thread.currentThread().getId());
+    }
+
+    /**
+     * Encodes the trace with the solver context of the given thread, for callers running on
+     * another thread (the shutdown hook sending the trace of the target's main thread).
+     */
+    public String getTraceDTO(StatsStorage statsStorage, long threadId) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
+        return DTOBuilder.encodeTrace(symbolicTrace, statsStorage, threadId);
     }
 
     /**
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/FrameDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/FrameDTO.java
new file mode 100644
index 00000000..57f9572c
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/FrameDTO.java
@@ -0,0 +1,38 @@
+package de.uzl.its.swat.symbolic.trace.dto;
+
+/** One stack frame of the throwable that ended the execution (see {@link ViolationDTO}). */
+public class FrameDTO {
+    // The declaring class of the frame (dotted name)
+    private String className;
+    // The source file of the frame, empty if unknown
+    private String sourceFile;
+    // The source line of the frame, -1 if unknown
+    private int line;
+
+    public FrameDTO(String className, String sourceFile, int line) {
+        this.className = className;
+        this.sourceFile = sourceFile;
+        this.line = line;
+    }
+
+    /** Private default constructor for serialization */
+    @SuppressWarnings("unused")
+    private FrameDTO() {}
+
+    public String getClassName() {
+        return className;
+    }
+
+    public String getSourceFile() {
+        return sourceFile;
+    }
+
+    public int getLine() {
+        return line;
+    }
+
+    @Override
+    public String toString() {
+        return className + "(" + sourceFile + ":" + line + ")";
+    }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java
new file mode 100644
index 00000000..aa7928e5
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java
@@ -0,0 +1,111 @@
+package de.uzl.its.swat.symbolic.trace.dto;
+
+/**
+ * A value returned by a {@code Verifier.nondet*()} call together with the location of the call.
+ * The explorer turns the sequence of these into the {@code function_return} waypoints of an
+ * SV-COMP violation witness.
+ */
+public class NondetReturnDTO {
+    // The Verifier method name, e.g. nondetInt
+    private String function;
+    // The Java type of the value: boolean|byte|short|char|int|long|float|double|String
+    private String type;
+    // The value in its witness string form: integers decimal, char as its code point, float/double
+    // as Java's Float/Double.toString, boolean true/false, String the raw string.
+    private String value;
+    // Exact IEEE-754 bits of a float/double value as 0x-prefixed hex, null for other types
+    private String bits;
+    // The class containing the call (dotted name)
+    private String className;
+    // The method containing the call as name + descriptor, e.g. main([Ljava/lang/String;)V
+    private String method;
+    // The SourceFile attribute of that class, empty if unknown
+    private String sourceFile;
+    // The source line of the call
+    private int line;
+    // 0-based index among the nondet calls on that source line of that class (evaluation order)
+    private int callIndex;
+
+    public NondetReturnDTO(
+            String function,
+            String type,
+            String value,
+            String bits,
+            String className,
+            String method,
+            String sourceFile,
+            int line,
+            int callIndex) {
+        this.function = function;
+        this.type = type;
+        this.value = value;
+        this.bits = bits;
+        this.className = className;
+        this.method = method;
+        this.sourceFile = sourceFile;
+        this.line = line;
+        this.callIndex = callIndex;
+    }
+
+    /** Private default constructor for serialization */
+    @SuppressWarnings("unused")
+    private NondetReturnDTO() {}
+
+    public String getFunction() {
+        return function;
+    }
+
+    public String getType() {
+        return type;
+    }
+
+    public String getValue() {
+        return value;
+    }
+
+    public String getBits() {
+        return bits;
+    }
+
+    public String getClassName() {
+        return className;
+    }
+
+    public String getMethod() {
+        return method;
+    }
+
+    public String getSourceFile() {
+        return sourceFile;
+    }
+
+    public int getLine() {
+        return line;
+    }
+
+    public int getCallIndex() {
+        return callIndex;
+    }
+
+    @Override
+    public String toString() {
+        return "NondetReturnDTO{"
+                + function
+                + " -> "
+                + type
+                + " "
+                + value
+                + (bits == null ? "" : " (" + bits + ")")
+                + " at "
+                + className
+                + "."
+                + method
+                + "("
+                + sourceFile
+                + ":"
+                + line
+                + ")#"
+                + callIndex
+                + '}';
+    }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java
index 75eaf698..e4d3bfa2 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java
@@ -17,6 +17,14 @@ public class TraceDTO {
     @SuppressWarnings("unused")
     private ArrayList<InvocationDTO> missingInvocations;
 
+    // The values returned by Verifier.nondet*() calls with their call locations (witness data)
+    @SuppressWarnings("unused")
+    private ArrayList<NondetReturnDTO> nondetReturns;
+
+    // The throwable that escaped the entry method, null if the execution ended normally
+    @SuppressWarnings("unused")
+    private ViolationDTO violation;
+
     @SuppressWarnings("unused")
     private boolean symbolicContextLoss = false;
     @SuppressWarnings("unused")
@@ -24,11 +32,13 @@ public class TraceDTO {
     @SuppressWarnings("unused")
     private boolean referenceSemanticChange = false;
 
-    public TraceDTO(ArrayList<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, ArrayList<InvocationDTO> missingInvocations, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) {
+    public TraceDTO(ArrayList<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, ArrayList<InvocationDTO> missingInvocations, ArrayList<NondetReturnDTO> nondetReturns, ViolationDTO violation, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) {
         this.trace = trace;
         this.inputs = inputs;
         this.ufs = ufs;
         this.missingInvocations = missingInvocations;
+        this.nondetReturns = nondetReturns;
+        this.violation = violation;
         this.symbolicContextLoss = symbolicContextLoss;
         this.symbolicPrecisionLoss = symbolicPrecisionLoss;
         this.referenceSemanticChange = referenceSemanticChange;
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/ViolationDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/ViolationDTO.java
new file mode 100644
index 00000000..f9afd782
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/ViolationDTO.java
@@ -0,0 +1,37 @@
+package de.uzl.its.swat.symbolic.trace.dto;
+
+import java.util.List;
+
+/**
+ * The throwable that escaped the entry method, recorded by the surrounding try/catch of main. The
+ * explorer derives the target waypoint of a violation witness from the innermost frame that lies
+ * in the task sources.
+ */
+public class ViolationDTO {
+    // The class name of the throwable, e.g. java.lang.AssertionError
+    private String throwable;
+    // The stack frames, innermost first; JDK and SWAT frames are left out
+    private List<FrameDTO> frames;
+
+    public ViolationDTO(String throwable, List<FrameDTO> frames) {
+        this.throwable = throwable;
+        this.frames = frames;
+    }
+
+    /** Private default constructor for serialization */
+    @SuppressWarnings("unused")
+    private ViolationDTO() {}
+
+    public String getThrowable() {
+        return throwable;
+    }
+
+    public List<FrameDTO> getFrames() {
+        return frames;
+    }
+
+    @Override
+    public String toString() {
+        return "ViolationDTO{" + throwable + " " + frames + '}';
+    }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java
index 2ecdbac3..b83a3e8d 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java
@@ -17,7 +17,10 @@
 import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor;
 import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
 import de.uzl.its.swat.symbolic.value.Value;
+import java.util.ArrayList;
 import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
 import java.util.concurrent.ThreadLocalRandom;
 import java.util.logging.LogRecord;
 import java.util.logging.SimpleFormatter;
@@ -163,7 +166,7 @@ public static void sendData(long id) throws NoThreadContextException, JsonProces
             }
             if(!config.isCoverageOnly()) {
                 ConstraintRequest.sendConstraints(
-                        symbolicStateHandler.getTraceDTO(context.getStatsStorage()), endpointID, traceID);
+                        symbolicStateHandler.getTraceDTO(context.getStatsStorage(), id), endpointID, traceID);
             }
 
         } else {
@@ -175,6 +178,20 @@ public static int getThreadCount() {
         return threadContextHashMap.size();
     }
 
+    /**
+     * The ids of the target threads whose symbolic execution has started and not been terminated
+     * (the context of the instrumentation itself, id -1, is left out).
+     */
+    public static List<Long> getActiveThreadContextIds() {
+        List<Long> ids = new ArrayList<>();
+        for (Map.Entry<Long, ThreadContext> e : threadContextHashMap.entrySet()) {
+            if (e.getKey() != -1 && !e.getValue().isDisabled()) {
+                ids.add(e.getKey());
+            }
+        }
+        return ids;
+    }
+
     public static void removeSolverContext(long id) throws NoThreadContextException  {
         ThreadContext context = threadContextHashMap.get(id);
         if (context != null) {
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java
index 10e1e79d..5507f37f 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java
@@ -1,77 +1,190 @@
 package de.uzl.its.swat.witness;
 
-import java.math.BigDecimal;
-import java.util.Base64;
+import de.uzl.its.swat.symbolic.trace.dto.FrameDTO;
+import de.uzl.its.swat.symbolic.trace.dto.NondetReturnDTO;
+import de.uzl.its.swat.symbolic.trace.dto.ViolationDTO;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
 
-public class Witness {
-    public static void recordValue(boolean value, int lineNumber, String cname, String desc) {
-        String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+/**
+ * Records the data an SV-COMP violation witness is built from. The data travels to the explorer as
+ * part of the trace ({@code TraceDTO.nondetReturns} and {@code TraceDTO.violation}); nothing is
+ * printed for it.
+ *
+ * <ul>
+ *   <li>{@link #recordValue} is invoked by the SV-COMP instrumentation right after every {@code
+ *       Verifier.nondet*()} call with the returned value and the location of the call: the class,
+ *       the calling method (name + descriptor), the class' SourceFile attribute, the line and the
+ *       index of the call among the nondet calls on that line (bytecode order, which follows the
+ *       left-to-right evaluation order).
+ *   <li>{@link #recordTarget} is invoked by the surrounding try/catch of the entry method with the
+ *       throwable that escaped it; its stack trace locates the violating statement.
+ * </ul>
+ *
+ * <p>The state is static: every execution of the target runs in its own JVM, and the recording
+ * calls may happen before a thread context exists (e.g. in static initializers).
+ */
+public final class Witness {
+    /** Upper bound on the recorded stack frames of the violation (after dropping JDK/SWAT frames). */
+    static final int MAX_FRAMES = 32;
+
+    /** Class name prefixes of frames that cannot be the violating statement of the task. */
+    private static final String[] SKIPPED_FRAME_PREFIXES = {
+        "java.", "javax.", "jdk.", "sun.", "com.sun.", "de.uzl.its.swat.", "shadow.swat."
+    };
+
+    private static final List<NondetReturnDTO> nondetReturns =
+            Collections.synchronizedList(new ArrayList<>());
+    private static volatile ViolationDTO violation = null;
+
+    private Witness() {}
+
+    private static void record(
+            String function,
+            String type,
+            String value,
+            String bits,
+            String cname,
+            String method,
+            String sourceFile,
+            int line,
+            int callIndex) {
+        nondetReturns.add(
+                new NondetReturnDTO(
+                        function,
+                        type,
+                        value,
+                        bits,
+                        cname.replace('/', '.'),
+                        method,
+                        sourceFile == null ? "" : sourceFile,
+                        line,
+                        callIndex));
+    }
+
+    public static void recordValue(
+            boolean value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        record(function, "boolean", String.valueOf(value), null, cname, method, sourceFile, line, callIndex);
+    }
+
+    public static void recordValue(
+            byte value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        record(function, "byte", String.valueOf(value), null, cname, method, sourceFile, line, callIndex);
+    }
+
+    public static void recordValue(
+            short value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        record(function, "short", String.valueOf(value), null, cname, method, sourceFile, line, callIndex);
     }
 
-    public static void recordValue(byte value, int lineNumber, String cname, String desc) {
-        String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+    public static void recordValue(
+            char value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        // Chars travel as their (unsigned) code point; the witness renders the literal
+        record(function, "char", String.valueOf((int) value), null, cname, method, sourceFile, line, callIndex);
     }
 
-    public static void recordValue(char value, int lineNumber, String cname, String desc) {
-        int encVal = Integer.valueOf(value);
-        String witness = encVal + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+    public static void recordValue(
+            int value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        record(function, "int", String.valueOf(value), null, cname, method, sourceFile, line, callIndex);
     }
 
-    public static void recordValue(short value, int lineNumber, String cname, String desc) {
-        String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+    public static void recordValue(
+            long value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        record(function, "long", String.valueOf(value), null, cname, method, sourceFile, line, callIndex);
     }
 
-    public static void recordValue(int value, int lineNumber, String cname, String desc) {
-        String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+    public static void recordValue(
+            float value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        // Float.toString is exact enough to round-trip (incl. NaN, Infinity, -0.0); the raw bits
+        // let the witness reproduce the value bit for bit.
+        record(
+                function,
+                "float",
+                Float.toString(value),
+                "0x" + Integer.toHexString(Float.floatToRawIntBits(value)),
+                cname,
+                method,
+                sourceFile,
+                line,
+                callIndex);
     }
 
-    public static void recordValue(float value, int lineNumber, String cname, String desc) {
-        // Use BigDecimal to avoid scientific notation (e.g., -2.022784E-6)
-        // but handle special values (NaN, Infinity) which BigDecimal doesn't support
-        String valueStr;
-        if (Float.isNaN(value) || Float.isInfinite(value)) {
-            valueStr = Float.toString(value);
-        } else {
-            valueStr = BigDecimal.valueOf(value).toPlainString();
+    public static void recordValue(
+            double value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        record(
+                function,
+                "double",
+                Double.toString(value),
+                "0x" + Long.toHexString(Double.doubleToRawLongBits(value)),
+                cname,
+                method,
+                sourceFile,
+                line,
+                callIndex);
+    }
+
+    public static void recordValue(
+            String value, String function, String cname, String method, String sourceFile, int line, int callIndex) {
+        record(function, "String", value == null ? "" : value, null, cname, method, sourceFile, line, callIndex);
+    }
+
+    /**
+     * Records the throwable that escaped the entry method and prints its stack trace (the explorer
+     * derives the verdict from that output). The frames locate the violating statement for the
+     * witness' target waypoint.
+     *
+     * @param throwable the uncaught throwable
+     */
+    public static void recordTarget(Throwable throwable) {
+        throwable.printStackTrace();
+        violation = describe(throwable);
+    }
+
+    /**
+     * Builds the violation entry for a throwable: its class name and its stack frames, innermost
+     * first, without the JDK and SWAT frames (which cannot be the violating statement), capped at
+     * {@link #MAX_FRAMES}.
+     *
+     * @param throwable the throwable
+     * @return the violation entry
+     */
+    public static ViolationDTO describe(Throwable throwable) {
+        List<FrameDTO> frames = new ArrayList<>();
+        for (StackTraceElement frame : throwable.getStackTrace()) {
+            if (frames.size() >= MAX_FRAMES) break;
+            if (isSkipped(frame.getClassName())) continue;
+            frames.add(
+                    new FrameDTO(
+                            frame.getClassName(),
+                            frame.getFileName() == null ? "" : frame.getFileName(),
+                            frame.getLineNumber()));
         }
-        String witness = valueStr + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+        return new ViolationDTO(throwable.getClass().getName(), frames);
     }
 
-    public static void recordValue(long value, int lineNumber, String cname, String desc) {
-        String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+    private static boolean isSkipped(String className) {
+        for (String prefix : SKIPPED_FRAME_PREFIXES) {
+            if (className.startsWith(prefix)) return true;
+        }
+        return false;
     }
 
-    public static void recordValue(double value, int lineNumber, String cname, String desc) {
-        // Use BigDecimal to avoid scientific notation (e.g., 1.23E-10)
-        // but handle special values (NaN, Infinity) which BigDecimal doesn't support
-        String valueStr;
-        if (Double.isNaN(value) || Double.isInfinite(value)) {
-            valueStr = Double.toString(value);
-        } else {
-            valueStr = BigDecimal.valueOf(value).toPlainString();
+    /** The recorded nondet return values in execution order (a copy). */
+    public static ArrayList<NondetReturnDTO> getNondetReturns() {
+        synchronized (nondetReturns) {
+            return new ArrayList<>(nondetReturns);
         }
-        String witness = valueStr + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
     }
 
-    public static void recordValue(String value, int lineNumber, String cname, String desc) {
-        String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc;
-        String enc = Base64.getEncoder().encodeToString(witness.getBytes());
-        System.out.println("[WITNESS] " + enc);
+    /** The recorded violation, or null if no throwable escaped the entry method (yet). */
+    public static ViolationDTO getViolation() {
+        return violation;
+    }
+
+    /** Clears the recorded data (for tests; a target execution never needs this). */
+    public static void reset() {
+        nondetReturns.clear();
+        violation = null;
     }
 }
diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy
new file mode 100644
index 00000000..2d47c4a4
--- /dev/null
+++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy
@@ -0,0 +1,109 @@
+package de.uzl.its.swat.witness
+
+import com.fasterxml.jackson.databind.ObjectMapper
+import spock.lang.Shared
+import spock.lang.Specification
+
+import javax.tools.ToolProvider
+import java.nio.file.Files
+import java.nio.file.Path
+import java.util.concurrent.TimeUnit
+
+/**
+ * L2 (forked agent): the SV-COMP instrumentation records the witness data in the trace. A tiny
+ * SV-COMP style target is compiled and run with the agent in {@code solver.mode=PRINT}; the
+ * {@code TraceDTO} JSON printed to stdout must carry the nondet returns with their call locations
+ * and the violation with its frames. Runs via the {@code agentTest} Gradle task (needs the agent
+ * jar from {@code copyJar}).
+ */
+class SvcompWitnessAgentSpec extends Specification {
+
+    static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath()
+    static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath()
+    static final Path TARGET_SOURCES = Path.of("src", "test", "resources", "targets", "svcomp").toAbsolutePath()
+
+    @Shared Path classes
+    @Shared Map trace
+    @Shared String output
+
+    def setupSpec() {
+        assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}"
+        classes = Files.createTempDirectory("swat-witness-agent-spec")
+        compile(classes)
+        output = run(classes, ["-Dswat.input.I_0=3", "-Dswat.input.I_1=4"])
+        trace = parseTrace(output)
+    }
+
+    def cleanupSpec() {
+        classes?.toFile()?.deleteDir()
+    }
+
+    def "the trace carries every nondet return with its call location"() {
+        expect:
+        trace.nondetReturns.size() == 4
+        trace.nondetReturns*.function == ["nondetInt", "nondetInt", "nondetDouble", "nondetString"]
+        trace.nondetReturns*.type == ["int", "int", "double", "String"]
+        trace.nondetReturns*.value == ["3", "4", "0.0", "fixed"]
+        trace.nondetReturns*.className == ["Main"] * 4
+        trace.nondetReturns*.method == ["main([Ljava/lang/String;)V"] * 4
+        trace.nondetReturns*.sourceFile == ["Main.java"] * 4
+        trace.nondetReturns*.line == [14, 14, 15, 16]
+        trace.nondetReturns*.callIndex == [0, 1, 0, 0]
+        trace.nondetReturns[2].bits == "0x0"
+        trace.nondetReturns[0].bits == null
+    }
+
+    def "the trace carries the violation with the frames of the task innermost first"() {
+        expect:
+        trace.violation != null
+        trace.violation.throwable == "java.lang.AssertionError"
+        trace.violation.frames*.className == ["Main", "Main"]
+        trace.violation.frames*.sourceFile == ["Main.java", "Main.java"]
+        trace.violation.frames*.line == [9, 18]
+    }
+
+    def "the inputs of the trace still correspond to the nondet returns"() {
+        expect:
+        trace.inputs.size() == 4
+        trace.inputs*.name.findAll { it.startsWith("I_") }.size() == 2
+    }
+
+    def "nothing is printed for the witness besides the trace"() {
+        expect:
+        !output.contains("[WITNESS]")
+        !output.contains("[WITNESS_TARGET]")
+    }
+
+    private static void compile(Path outDir) {
+        def sources = Files.walk(TARGET_SOURCES).filter { it.toString().endsWith(".java") }.collect { it.toString() }
+        def args = ["-source", "1.8", "-target", "1.8", "-g", "-d", outDir.toString()] + sources
+        def err = new ByteArrayOutputStream()
+        int rc = ToolProvider.getSystemJavaCompiler().run(null, null, err, args as String[])
+        assert rc == 0: "javac failed: ${err}"
+    }
+
+    private static String run(Path classes, List<String> inputs) {
+        def java = Path.of(System.getProperty("java.home"), "bin", "java").toString()
+        def cmd = [java,
+                   "-javaagent:${AGENT_JAR}".toString(),
+                   "-Djava.library.path=${NATIVE_LIBS}".toString(),
+                   "-Dconfig.path=/nonexistent/swat.cfg",
+                   "-Dinstrumentation.transformer=SV_COMP",
+                   "-Dsolver.mode=PRINT",
+                   "-DexitOnError=false",
+                   "-DlogShadowStateToConsole=false"] + inputs +
+                  ["-cp", classes.toString(), "-ea", "Main"]
+        def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start()
+        def out = proc.inputStream.text
+        assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}"
+        return out
+    }
+
+    /** The TraceDTO is the single pretty-printed JSON object whose braces start at column 0. */
+    private static Map parseTrace(String out) {
+        int start = out.indexOf("\n{\n")
+        int end = out.indexOf("\n}\n", start)
+        assert start >= 0 && end > start: "no trace JSON in output:\n${out}"
+        return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map)
+    }
+}
diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy
new file mode 100644
index 00000000..fc859254
--- /dev/null
+++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy
@@ -0,0 +1,145 @@
+package de.uzl.its.swat.witness
+
+import de.uzl.its.swat.symbolic.trace.dto.NondetReturnDTO
+import de.uzl.its.swat.symbolic.trace.dto.ViolationDTO
+import spock.lang.Specification
+
+/**
+ * L0: the witness recorder renders nondet return values and the violation's stack frames in the
+ * form the witness library expects (see the witnesscreator API contract).
+ */
+class WitnessSpec extends Specification {
+
+    def setup() {
+        Witness.reset()
+    }
+
+    def cleanup() {
+        Witness.reset()
+    }
+
+    def "a nondet return value is recorded with its call location"() {
+        when:
+        Witness.recordValue(42, "nondetInt", "pkg/Main", "main([Ljava/lang/String;)V", "Main.java", 12, 1)
+        List<NondetReturnDTO> recorded = Witness.getNondetReturns()
+
+        then:
+        recorded.size() == 1
+        with(recorded[0]) {
+            function == "nondetInt"
+            type == "int"
+            value == "42"
+            bits == null
+            className == "pkg.Main"
+            method == "main([Ljava/lang/String;)V"
+            sourceFile == "Main.java"
+            line == 12
+            callIndex == 1
+        }
+    }
+
+    def "values are rendered in their witness string form (#type #description)"() {
+        when:
+        Witness.recordValue(*args)
+        NondetReturnDTO recorded = Witness.getNondetReturns()[0]
+
+        then:
+        recorded.type == type
+        recorded.value == expectedValue
+        recorded.bits == expectedBits
+
+        where:
+        description     | args                                                                     | type      | expectedValue  | expectedBits
+        "true"          | [true, "nondetBoolean", "Main", "main()V", "Main.java", 1, 0]                       | "boolean" | "true"         | null
+        "negative"      | [(byte) -5, "nondetByte", "Main", "main()V", "Main.java", 1, 0]                     | "byte"    | "-5"           | null
+        "min"           | [Short.MIN_VALUE, "nondetShort", "Main", "main()V", "Main.java", 1, 0]              | "short"   | "-32768"       | null
+        "code point"    | [(char) 'A', "nondetChar", "Main", "main()V", "Main.java", 1, 0]                    | "char"    | "65"           | null
+        "high code"     | [(char) 0xFFFF, "nondetChar", "Main", "main()V", "Main.java", 1, 0]                 | "char"    | "65535"        | null
+        "min"           | [Integer.MIN_VALUE, "nondetInt", "Main", "main()V", "Main.java", 1, 0]              | "int"     | "-2147483648"  | null
+        "max"           | [Long.MAX_VALUE, "nondetLong", "Main", "main()V", "Main.java", 1, 0]                | "long"    | "9223372036854775807" | null
+        "plain"         | [0.1f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0]                         | "float"   | "0.1"          | "0x3dcccccd"
+        "small"         | [-2.022784E-6f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0]                | "float"   | "-2.022784E-6" | "0x" + Integer.toHexString(Float.floatToRawIntBits(-2.022784E-6f))
+        "negative zero" | [-0.0f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0]                        | "float"   | "-0.0"         | "0x80000000"
+        "NaN"           | [Float.NaN, "nondetFloat", "Main", "main()V", "Main.java", 1, 0]                    | "float"   | "NaN"          | "0x7fc00000"
+        "infinity"      | [Float.NEGATIVE_INFINITY, "nondetFloat", "Main", "main()V", "Main.java", 1, 0]      | "float"   | "-Infinity"    | "0xff800000"
+        "plain"         | [1.23E-10d, "nondetDouble", "Main", "main()V", "Main.java", 1, 0]                   | "double"  | "1.23E-10"     | "0x" + Long.toHexString(Double.doubleToRawLongBits(1.23E-10d))
+        "negative zero" | [-0.0d, "nondetDouble", "Main", "main()V", "Main.java", 1, 0]                       | "double"  | "-0.0"         | "0x8000000000000000"
+        "infinity"      | [Double.POSITIVE_INFINITY, "nondetDouble", "Main", "main()V", "Main.java", 1, 0]    | "double"  | "Infinity"     | "0x7ff0000000000000"
+        "raw"           | ["a \"quoted\"\\n", "nondetString", "Main", "main()V", "Main.java", 1, 0]           | "String"  | "a \"quoted\"\\n" | null
+        "null"          | [(String) null, "nondetString", "Main", "main()V", "Main.java", 1, 0]               | "String"  | ""             | null
+    }
+
+    def "float and double strings round-trip to the recorded value"() {
+        when:
+        Witness.recordValue(f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0)
+        Witness.recordValue(d, "nondetDouble", "Main", "main()V", "Main.java", 1, 0)
+        def recorded = Witness.getNondetReturns()
+
+        then:
+        Float.floatToRawIntBits(Float.parseFloat(recorded[0].value)) == Float.floatToRawIntBits(f)
+        Double.doubleToRawLongBits(Double.parseDouble(recorded[1].value)) == Double.doubleToRawLongBits(d)
+
+        where:
+        f << [0.33333334f, Float.MIN_VALUE, 16777217.0f, -3.4028235E38f]
+        d << [0.3333333333333333d, Double.MIN_VALUE, 9007199254740993.0d, 1.7976931348623157E308d]
+    }
+
+    def "nondet returns keep their execution order"() {
+        when:
+        Witness.recordValue(1, "nondetInt", "Main", "main()V", "Main.java", 5, 0)
+        Witness.recordValue(2, "nondetInt", "Main", "main()V", "Main.java", 5, 1)
+        Witness.recordValue(3L, "nondetLong", "Main", "main()V", "Main.java", 6, 0)
+
+        then:
+        Witness.getNondetReturns()*.value == ["1", "2", "3"]
+        Witness.getNondetReturns()*.callIndex == [0, 1, 0]
+    }
+
+    def "the violation records the throwable and its frames innermost first without JDK and SWAT frames"() {
+        given:
+        def throwable = new AssertionError("boom")
+        throwable.setStackTrace([
+                new StackTraceElement("java.lang.Integer", "parseInt", "Integer.java", 652),
+                new StackTraceElement("de.uzl.its.swat.instrument.Intrinsics", "init", "Intrinsics.java", 1),
+                new StackTraceElement("pkg.Helper", "check", "Helper.java", 20),
+                new StackTraceElement("jdk.internal.reflect.NativeMethodAccessorImpl", "invoke0", null, -2),
+                new StackTraceElement("Main", "main", "Main.java", 8),
+        ] as StackTraceElement[])
+
+        when:
+        ViolationDTO violation = Witness.describe(throwable)
+
+        then:
+        violation.throwable == "java.lang.AssertionError"
+        violation.frames*.className == ["pkg.Helper", "Main"]
+        violation.frames*.sourceFile == ["Helper.java", "Main.java"]
+        violation.frames*.line == [20, 8]
+    }
+
+    def "the violation frames are capped"() {
+        given:
+        def throwable = new RuntimeException()
+        throwable.setStackTrace((1..(Witness.MAX_FRAMES + 10)).collect {
+            new StackTraceElement("pkg.Rec", "rec", "Rec.java", it)
+        } as StackTraceElement[])
+
+        expect:
+        Witness.describe(throwable).frames.size() == Witness.MAX_FRAMES
+        Witness.describe(throwable).frames[0].line == 1
+    }
+
+    def "an unknown source file is recorded as empty"() {
+        given:
+        def throwable = new RuntimeException()
+        throwable.setStackTrace([new StackTraceElement("Main", "main", null, -1)] as StackTraceElement[])
+
+        expect:
+        Witness.describe(throwable).frames[0].sourceFile == ""
+        Witness.describe(throwable).frames[0].line == -1
+    }
+
+    def "no violation is recorded until a throwable escapes"() {
+        expect:
+        Witness.getViolation() == null
+    }
+}
diff --git a/symbolic-executor/src/test/resources/targets/svcomp/Main.java b/symbolic-executor/src/test/resources/targets/svcomp/Main.java
new file mode 100644
index 00000000..0356b322
--- /dev/null
+++ b/symbolic-executor/src/test/resources/targets/svcomp/Main.java
@@ -0,0 +1,21 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * SV-COMP style target for the agent test of the witness data in the trace: nondet calls of
+ * several types, two of them on one line, and an assertion that fails in a helper method.
+ */
+public class Main {
+  static int check(int a, int b) {
+    assert a + b != 7 : "witness target";
+    return a + b;
+  }
+
+  public static void main(String[] args) {
+    int a = Verifier.nondetInt(), b = Verifier.nondetInt();
+    double d = Verifier.nondetDouble();
+    String s = Verifier.nondetString();
+    if (d < 0.5 && s.length() > 3) {
+      check(a, b);
+    }
+  }
+}
diff --git a/symbolic-executor/src/test/resources/targets/svcomp/org/sosy_lab/sv_benchmarks/Verifier.java b/symbolic-executor/src/test/resources/targets/svcomp/org/sosy_lab/sv_benchmarks/Verifier.java
new file mode 100644
index 00000000..2dcbc9ac
--- /dev/null
+++ b/symbolic-executor/src/test/resources/targets/svcomp/org/sosy_lab/sv_benchmarks/Verifier.java
@@ -0,0 +1,46 @@
+package org.sosy_lab.sv_benchmarks;
+
+/** Minimal stand-in for the sv-benchmarks Verifier; the SV-COMP transformer redirects the calls. */
+public final class Verifier {
+  public static void assume(boolean condition) {
+    if (!condition) {
+      Runtime.getRuntime().halt(1);
+    }
+  }
+
+  public static boolean nondetBoolean() {
+    return false;
+  }
+
+  public static byte nondetByte() {
+    return 0;
+  }
+
+  public static char nondetChar() {
+    return 0;
+  }
+
+  public static short nondetShort() {
+    return 0;
+  }
+
+  public static int nondetInt() {
+    return 0;
+  }
+
+  public static long nondetLong() {
+    return 0;
+  }
+
+  public static float nondetFloat() {
+    return 0;
+  }
+
+  public static double nondetDouble() {
+    return 0;
+  }
+
+  public static String nondetString() {
+    return "";
+  }
+}
diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py
index c2bdf135..4cdd428d 100755
--- a/symbolic-explorer/SymbolicExplorer.py
+++ b/symbolic-explorer/SymbolicExplorer.py
@@ -132,6 +132,17 @@ def init_args(parser: argparse.ArgumentParser):
     parser.add_argument("--optimize", action="store_true", help="Enable Z3 optimizer to minimize variable values (slower but may produce simpler solutions)", default=False)
     parser.add_argument("--log-smt-formulas", action="store_true", help="Log SMT formulas and models to disk for debugging", default=False)
 
+    # SV-COMP witness arguments: the explorer writes the violation witness from the trace of the
+    # violating execution (needs the task's input files and property file as given to the verifier)
+    parser.add_argument("--witness-dir", default="witness",
+                        help="Directory for witness.yml/witness.graphml, relative to the working directory (sv-comp mode)")
+    parser.add_argument("--witness-input", nargs='+', default=[],
+                        help="The task's input files/directories exactly as given to the verifier")
+    parser.add_argument("--witness-property", help="Path to the property file of the task")
+    parser.add_argument("--witness-base-dir",
+                        help="Directory relative witness input paths are resolved against (default: the working directory)")
+    parser.add_argument("--producer-version", default="unknown", help="Producer version recorded in the witness")
+
     # HTTP-specific arguments
     parser.add_argument("--host", help="HTTP target host", default="localhost")  
     parser.add_argument("--http-port", help="HTTP target port", type=int, default=8080)
diff --git a/symbolic-explorer/constraint/ConstraintController.py b/symbolic-explorer/constraint/ConstraintController.py
index 7b205a09..666c6cd8 100755
--- a/symbolic-explorer/constraint/ConstraintController.py
+++ b/symbolic-explorer/constraint/ConstraintController.py
@@ -42,6 +42,8 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str
         symbolicContextLoss = request.symbolicContextLoss
         symbolicPrecisionLoss = request.symbolicPrecisionLoss
         referenceSemanticChange = request.referenceSemanticChange
+        nondetReturns = request.nondetReturns
+        violation = request.violation
 
         # Start a new thread to add constraints
         thread = threading.Thread(target=ConstraintService.add_constraints, kwargs={
@@ -53,7 +55,9 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str
             'missing_invocations': missingInvocations,
             'symbolic_context_loss': symbolicContextLoss,
             'symbolic_precision_loss': symbolicPrecisionLoss,
-            'reference_semantic_change': referenceSemanticChange})
+            'reference_semantic_change': referenceSemanticChange,
+            'nondet_returns': nondetReturns,
+            'violation': violation})
         thread.start()
         thread.join() # To ensure trace is added in SV-Comp mode
         # Return a response indicating that the request has been accepted
diff --git a/symbolic-explorer/constraint/ConstraintService.py b/symbolic-explorer/constraint/ConstraintService.py
index 14cee249..20fc8b5a 100755
--- a/symbolic-explorer/constraint/ConstraintService.py
+++ b/symbolic-explorer/constraint/ConstraintService.py
@@ -1,10 +1,10 @@
-from typing import List
+from typing import List, Optional
 from data.Database import Database
 from parse.TraceParser import Parser
 from data.trace.Input import Input
 from data.trace.UF import UF
 
-from parse.DataTransferObjects import TraceItem, InputItem, UFItem, InvocationItem
+from parse.DataTransferObjects import TraceItem, InputItem, UFItem, InvocationItem, NondetReturnItem, ViolationItem
 from data.trace.Special import Special
 from data.trace.Branch import Branch
 
@@ -24,7 +24,9 @@ class ConstraintService:
     def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inputs: List[InputItem], ufs: List[UFItem],
                         symbolic_context_loss: bool, symbolic_precision_loss: bool,
                         reference_semantic_change: bool = False,
-                        missing_invocations: List[InvocationItem] = None):
+                        missing_invocations: List[InvocationItem] = None,
+                        nondet_returns: List[NondetReturnItem] = None,
+                        violation: Optional[ViolationItem] = None):
         """
         Adds constraints to the database.
 
@@ -42,6 +44,8 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp
         symbolic_precision_loss (bool): A flag indicating whether the symbolic precision was lost (UFs introduced).
         reference_semantic_change (bool): A flag indicating whether reference equality semantics changed.
         missing_invocations (list): Methods that could not be modelled symbolically during this trace.
+        nondet_returns (list): The values returned by Verifier.nondet*() calls with their call locations.
+        violation (ViolationItem): The throwable that escaped the entry method, if any.
 
         Returns:
         None: The result is the side effect of adding data to the database.
@@ -55,6 +59,12 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp
         # Flatten the missing-invocation DTOs into plain dicts so the Database/Tree stay decoupled
         # from the pydantic request models.
         missing_invocations_data = [item.model_dump() for item in (missing_invocations or [])]
+        # The witness data of this execution (plain dicts as well); the Database keeps the latest.
+        witness_data = {
+            'trace_id': trace_id,
+            'nondet_returns': [item.model_dump() for item in (nondet_returns or [])],
+            'violation': violation.model_dump() if violation is not None else None,
+        }
         # Adding the trace and inputs to the database for the specified endpoint.
-        Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change, missing_invocations_data)
+        Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change, missing_invocations_data, witness_data)
         logger.info(f'[CONSTRAINT SERVICE] Added trace {trace_id} to endpoint {endpoint_id}')
diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py
index 489190bc..9b7b8af9 100755
--- a/symbolic-explorer/data/Database.py
+++ b/symbolic-explorer/data/Database.py
@@ -42,6 +42,8 @@ def __init__(self):
         self.instr_coverage = {'total_executed': {}, 'total_instr_count': 0, 'endpoints': {}}
         self.branch_coverage = {'total_executed': {}, 'total_branch_instr_count': 0}
         self.violations = {}
+        # Witness data (nondet returns, uncaught throwable) of the latest trace per endpoint
+        self.witness_data = {}
         self.optimize_solutions = False  # Whether to use Z3 Optimize() to minimize values
         self.log_smt_formulas = False  # Whether to log SMT formulas and models to disk for debugging
 
@@ -61,6 +63,7 @@ def reset(self):
         self.instr_coverage = {'total_executed': {}, 'total_instr_count': 0, 'endpoints': {}}
         self.branch_coverage = {'total_executed': {}, 'total_branch_instr_count': 0}
         self.violations = {}
+        self.witness_data = {}
 
         lock.release()
 
@@ -114,13 +117,16 @@ def get_endpoints(self):
 
     def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF],
                   symbolic_context_loss: bool, symbolic_precision_loss: bool,
-                  reference_semantic_change: bool = False, missing_invocations: list = None):
+                  reference_semantic_change: bool = False, missing_invocations: list = None,
+                  witness_data: dict = None):
         endpoint_id = str(endpoint_id)
 
         lock.acquire()
 
         self._add_endpoint(endpoint_id)
         self.traces.append(trace)
+        if witness_data is not None:
+            self.witness_data[endpoint_id] = witness_data
         self.tree[endpoint_id].add(trace, inputs, ufs)
         self.tree[endpoint_id].record_inputs(inputs)
         self.tree[endpoint_id].record_ufs(ufs)
@@ -150,6 +156,21 @@ def get_tree(self, endpoint_id: Union[str, int]) -> Tree:
         lock.release()
         return ret
     
+    def get_witness_data(self, endpoint_id: Union[str, int]) -> dict | None:
+        """The witness data of the latest trace of the endpoint (None if no trace arrived since the last clear)."""
+        endpoint_id = str(endpoint_id)
+        lock.acquire()
+        ret = copy.deepcopy(self.witness_data.get(endpoint_id))
+        lock.release()
+        return ret
+
+    def clear_witness_data(self, endpoint_id: Union[str, int]):
+        """Forgets the witness data of the endpoint, so that only a trace of the next execution can provide it."""
+        endpoint_id = str(endpoint_id)
+        lock.acquire()
+        self.witness_data.pop(endpoint_id, None)
+        lock.release()
+
     def record_uncaught_exception(self, endpoint_id: Union[str, int]):
         endpoint_id = str(endpoint_id)
         lock.acquire()
diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py
index d3d75756..eae64fd7 100644
--- a/symbolic-explorer/driver/SVCompDriver.py
+++ b/symbolic-explorer/driver/SVCompDriver.py
@@ -18,6 +18,7 @@
 from enum import Enum
 from svcomp.SymbolicStorage import SymbolicStorage
 from svcomp.TestcaseStats import write_testcase_stats
+from svcomp.WitnessWriter import write_violation_witness
 from timing.TimingManager import TimingManager
 
 
@@ -197,6 +198,9 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port,
             logger.info(f'[SVCOMP] {"="*30} ROUND ({round_idx:03}) {"="*30}')
             logger.info(f'[SVCOMP] {"="*73}')
 
+            # Only a trace of this round may provide the witness data of the violating execution
+            Database.instance().clear_witness_data(ENDPOINT_ID)
+
             # Build the java command to run DSE
             command: List[str] = self.build_command(javaagent=agentpath, config=configpath, Z3_DIR=z3path, port=port, cp=cp, java_path=java_path)
 
@@ -327,6 +331,10 @@ def run(self):
             verdict = Verdict.SAFE
         verdict_logger.info(f'[VERDICT {self.verification_category.value}] {verdict.value}')
 
+        # The witness is written after the verdict and never affects it
+        if verdict == Verdict.VIOLATION:
+            self.write_witness()
+
         # Stop total timing (don't print summary here - execution.py will print complete summary with witness timing)
         TimingManager.instance().stop_total_timer()
 
@@ -343,6 +351,21 @@ def run(self):
         self.kill_current_process()
         
         
+    def write_witness(self):
+        """Writes witness.yml/witness.graphml for the VIOLATION verdict from the trace of the violating round."""
+        input_files = getattr(self.args, 'witness_input', None) or []
+        property_file = getattr(self.args, 'witness_property', None)
+        if not input_files or not property_file:
+            logger.warning('[WITNESS] No task input files/property file given (--witness-input/--witness-property), no witness is written')
+            return
+        write_violation_witness(
+            Database.instance().get_witness_data(ENDPOINT_ID),
+            input_files=input_files,
+            property_file=property_file,
+            out_dir=getattr(self.args, 'witness_dir', None) or 'witness',
+            producer_version=getattr(self.args, 'producer_version', None) or 'unknown',
+            base_dir=getattr(self.args, 'witness_base_dir', None) or None)
+
     def kill_current_process(self):
         pid = os.getpid()  
         os.kill(pid, signal.SIGTERM)  # Send termination signal
diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py
index 4d46be72..03b6c94f 100644
--- a/symbolic-explorer/parse/DataTransferObjects.py
+++ b/symbolic-explorer/parse/DataTransferObjects.py
@@ -37,11 +37,48 @@ class InvocationItem(BaseModel):
     count: int
 
 
+class NondetReturnItem(BaseModel):
+    """A value returned by a ``Verifier.nondet*()`` call and the location of the call.
+
+    ``value`` is the witness string form (integers decimal, char as code point, float/double as
+    Java's ``Float/Double.toString``, boolean ``true``/``false``, String raw); ``bits`` carries the
+    exact IEEE-754 bits of a float/double as ``0x``-prefixed hex. ``callIndex`` is the 0-based
+    index among the nondet calls on that source line of that class, in evaluation order;
+    ``method`` is the calling method (name + descriptor).
+    """
+    function: str
+    type: str
+    value: str
+    bits: Optional[str] = None
+    className: str
+    # The calling method as name + descriptor, e.g. main([Ljava/lang/String;)V
+    method: Optional[str] = None
+    sourceFile: str = ""
+    line: int
+    callIndex: int = 0
+
+
+class FrameItem(BaseModel):
+    """A stack frame of the throwable that escaped the entry method."""
+    className: str
+    sourceFile: str = ""
+    line: int
+
+
+class ViolationItem(BaseModel):
+    """The throwable that escaped the entry method, with its frames innermost first."""
+    throwable: str
+    frames: List[FrameItem] = []
+
+
 class ConstraintRequest(BaseModel):
     trace: List[TraceItem]
     inputs: List[InputItem]
     ufs: List[UFItem]
     missingInvocations: List[InvocationItem] = []
+    # Witness data: the nondet return values of the execution and the uncaught throwable (if any)
+    nondetReturns: List[NondetReturnItem] = []
+    violation: Optional[ViolationItem] = None
     symbolicContextLoss: bool
     symbolicPrecisionLoss: bool
     referenceSemanticChange: bool = False
diff --git a/symbolic-explorer/requirements.txt b/symbolic-explorer/requirements.txt
index fec927c0..0362c7cd 100644
--- a/symbolic-explorer/requirements.txt
+++ b/symbolic-explorer/requirements.txt
@@ -18,4 +18,5 @@ typing-inspection==0.4.2
 typing_extensions==4.15.0
 urllib3==2.6.3
 uvicorn==0.40.0
+witnesscreator @ git+https://github.com/SWAT-project/WitnessCreator@v1.0.0
 z3-solver==4.15.4.0
diff --git a/symbolic-explorer/svcomp/WitnessWriter.py b/symbolic-explorer/svcomp/WitnessWriter.py
new file mode 100644
index 00000000..dad58141
--- /dev/null
+++ b/symbolic-explorer/svcomp/WitnessWriter.py
@@ -0,0 +1,104 @@
+"""
+Writes the SV-COMP violation witness of a testcase from the trace of the violating execution.
+
+The executor ships the witness data in the trace (``nondetReturns``: every value returned by a
+``Verifier.nondet*()`` call with the location of the call; ``violation``: the throwable that escaped
+the entry method with its stack frames). The Database keeps the data of the latest trace; when the
+final verdict is VIOLATION the driver hands it to :func:`write_violation_witness`, which builds the
+witness files with the ``witnesscreator`` package (``witness.yml`` in format 2.3 and the legacy
+``witness.graphml``).
+
+Witness generation must never break or delay the verdict: everything here is caught and logged.
+"""
+
+import time
+from pathlib import Path
+from typing import Dict, List, Optional
+
+import log
+from timing.TimingManager import TimingManager
+
+logger = log.get_logger()
+
+# The witness formats written per violation; YAML (2.3) is what SV-COMP 2027 requires, GraphML is
+# kept for validators that still read it (e.g. wit4java).
+WITNESS_FORMATS = ("yaml", "graphml")
+PRODUCER_NAME = "SWAT"
+
+
+def write_violation_witness(witness_data: Optional[dict], input_files: List[str], property_file: str,
+                            out_dir: str, producer_version: str,
+                            base_dir: Optional[str] = None) -> Dict[str, Path]:
+    """
+    Write the violation witness files for the trace data of the violating execution.
+
+    Args:
+        witness_data: ``{'nondet_returns': [...], 'violation': {...} | None}`` as stored by the
+            Database for the latest trace, or None if no trace of the violating execution arrived.
+        input_files: The task's input files/directories exactly as given to the verifier.
+        property_file: Path to the property file of the task.
+        out_dir: Directory the witness files are written to (created if needed).
+        producer_version: The SWAT version recorded in the witness metadata.
+        base_dir: Directory relative input paths are resolved against (default: the working directory).
+
+    Returns:
+        The written files per format (``{'yaml': Path, 'graphml': Path}``), empty if nothing was written.
+        Never raises.
+    """
+    start = time.perf_counter()
+    try:
+        return _write(witness_data, input_files, property_file, out_dir, producer_version, base_dir)
+    except Exception:  # noqa: BLE001 - the verdict must not depend on the witness
+        logger.exception('[WITNESS] Writing the violation witness failed')
+        return {}
+    finally:
+        TimingManager.instance().record_witness_generation_time(time.perf_counter() - start)
+
+
+def _write(witness_data: Optional[dict], input_files: List[str], property_file: str, out_dir: str,
+           producer_version: str, base_dir: Optional[str]) -> Dict[str, Path]:
+    try:
+        from witnesscreator import Frame, Location, NondetReturn, Task, Violation, write_witnesses
+    except ImportError as e:
+        logger.error(f'[WITNESS] The witnesscreator package is not available, no witness is written: {e}')
+        return {}
+
+    if witness_data is None:
+        logger.warning('[WITNESS] No trace of the violating execution arrived; the witness has no waypoints')
+        witness_data = {}
+
+    values = []
+    for nr in witness_data.get('nondet_returns') or []:
+        values.append(NondetReturn(
+            function=nr['function'],
+            type=nr['type'],
+            value=nr['value'],
+            location=Location(class_name=nr['className'], source_file=nr.get('sourceFile') or None,
+                              line=nr['line'], call_index=nr.get('callIndex', 0),
+                              method=nr.get('method')),
+            bits=nr.get('bits'),
+        ))
+
+    violation = None
+    v = witness_data.get('violation')
+    if v is not None:
+        violation = Violation(
+            throwable=v['throwable'],
+            frames=[Frame(class_name=f['className'], source_file=f.get('sourceFile') or None, line=f['line'])
+                    for f in v.get('frames') or []],
+        )
+    else:
+        logger.warning('[WITNESS] No uncaught throwable recorded; the witness has no target waypoint')
+
+    task = Task(input_files=list(input_files), property_file=property_file,
+                producer_name=PRODUCER_NAME, producer_version=producer_version, base_dir=base_dir)
+
+    logger.info(f'[WITNESS] Writing witness ({len(values)} nondet values, '
+                f'target: {violation.throwable if violation else "none"}) to {out_dir}')
+    paths = write_witnesses(task, values, violation, out_dir=out_dir, formats=WITNESS_FORMATS)
+    for fmt, path in paths.items():
+        logger.info(f'[WITNESS] Written {fmt}: {path}')
+    missing = [fmt for fmt in WITNESS_FORMATS if fmt not in paths]
+    if missing:
+        logger.error(f'[WITNESS] Not written: {missing}')
+    return dict(paths)
diff --git a/targets/sv-comp/scripts/README.md b/targets/sv-comp/scripts/README.md
index 22ce37c6..d8aeb5dd 100644
--- a/targets/sv-comp/scripts/README.md
+++ b/targets/sv-comp/scripts/README.md
@@ -61,6 +61,15 @@ scripts/
 ./svcomp setup all
 ```
 
+Witnesses of violation results are written by the Symbolic Explorer itself (from the trace of
+the violating execution, via the `witnesscreator` package from `symbolic-explorer/requirements.txt`)
+to the testcase's log directory as `witness/witness.yml` (YAML format 2.3) and
+`witness/witness.graphml` (legacy). The harness only validates them: the YAML witness must have
+exactly one `target` waypoint and, if `SWAT_WITNESSLINT` names a WitnessLint command
+(e.g. `SWAT_WITNESSLINT="/path/venv/bin/python /path/witnesslint/witnesslinter.py"`), it is linted
+with `--expectViolationWitness --expectedWitnessVersion 2`; the GraphML witness is validated with
+wit4java (reported as `Validated:`). A proper validator setup is tracked in #47.
+
 ### Test Commands
 
 ```bash
diff --git a/targets/sv-comp/scripts/lib/__init__.py b/targets/sv-comp/scripts/lib/__init__.py
index 818811d0..b9a25c3c 100644
--- a/targets/sv-comp/scripts/lib/__init__.py
+++ b/targets/sv-comp/scripts/lib/__init__.py
@@ -17,7 +17,7 @@
     check_port_availability,
     ExecutionStatus,
 )
-from .witness import generate_and_validate_witness
+from .witness import validate_witness
 from .analysis.context_loss import main as analyze_context_loss
 from .comparison import compare_results
 from .utils import ci_print
@@ -50,7 +50,7 @@
     "check_port_availability",
     "ExecutionStatus",
     # Witness
-    "generate_and_validate_witness",
+    "validate_witness",
     # Analysis
     "analyze_context_loss",
     # Comparison
diff --git a/targets/sv-comp/scripts/lib/command_gen.py b/targets/sv-comp/scripts/lib/command_gen.py
index 9bf39f79..1f3a697f 100644
--- a/targets/sv-comp/scripts/lib/command_gen.py
+++ b/targets/sv-comp/scripts/lib/command_gen.py
@@ -49,14 +49,23 @@ def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=80
                     "-z3", str(library_path),
                     "--logdir", str(logging_dir),
                     "--mode", "sv-comp",
-                    '--port', str(port),
-                    "--classpath"]
+                    '--port', str(port)]
 
     cp: list[str] = []
+    inputs: list[str] = []
     for input_file in ver_task['input_files']:
-        cp.append(str((test_case_dir / input_file).resolve()))
+        inputs.append(str((test_case_dir / input_file).resolve()))
+        cp.append(inputs[-1])
         cp.append(str(BASE_PATH / 'libs' / 'java-library-path' / 'com.microsoft.z3.jar'))
-    return base_command + cp 
+
+    # The explorer writes the violation witness (witness.yml/witness.graphml) to <logging_dir>/witness
+    # from the trace of the violating execution; it needs the task's input files and property file.
+    property_path = test_case_dir.parent / 'properties' / ver_task['category'].value
+    witness_args: list[str] = ["--witness-dir", "witness",
+                               "--witness-property", str(property_path.resolve()),
+                               "--producer-version", "local",
+                               "--witness-input"] + inputs
+    return base_command + witness_args + ["--classpath"] + cp
 
 
 
diff --git a/targets/sv-comp/scripts/lib/execution.py b/targets/sv-comp/scripts/lib/execution.py
index db5c354e..d4f0d1f5 100644
--- a/targets/sv-comp/scripts/lib/execution.py
+++ b/targets/sv-comp/scripts/lib/execution.py
@@ -9,7 +9,7 @@
 from .dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command
 from .utils import ci_print
 from .command_gen import extract_testcases, generate_commands, new_run_timestamp, run_dir as make_run_dir
-from .witness import generate_and_validate_witness
+from .witness import validate_witness
 from collections import Counter
 from pathlib import Path
 
@@ -194,9 +194,10 @@ def target_execution(ver_task: VerificationTask, create_witness: bool = True) ->
             'case': case
         }
 
-        # Generate and validate witness (with timing)
+        # Validate the witness the explorer wrote for the violation verdict (with timing); the
+        # generation time is taken from the explorer's timing data below.
         if 'violation' in case and create_witness:
-            validated, witness_generation_time, witness_validation_time = generate_and_validate_witness(ver_task, output)
+            validated, witness_validation_time = validate_witness(ver_task)
 
     elapsed_time = time.perf_counter() - start_time
 
@@ -208,7 +209,8 @@ def target_execution(ver_task: VerificationTask, create_witness: bool = True) ->
             with open(timing_file, 'r') as f:
                 timing_data = json.load(f)
                 timing_breakdown = timing_data.get('aggregates', {})
-                # Update witness timing from our measurements
+                # Add the witness validation time measured here (generation is timed by the explorer)
+                witness_generation_time = timing_breakdown.get('witness_generation', witness_generation_time)
                 timing_breakdown['witness_generation'] = witness_generation_time
                 timing_breakdown['witness_validation'] = witness_validation_time
 
diff --git a/targets/sv-comp/scripts/lib/witness.py b/targets/sv-comp/scripts/lib/witness.py
index 16fd26c4..e1b538de 100644
--- a/targets/sv-comp/scripts/lib/witness.py
+++ b/targets/sv-comp/scripts/lib/witness.py
@@ -1,19 +1,33 @@
-import base64
+"""Validation of the witness files the Symbolic Explorer writes for violation verdicts.
+
+The explorer writes `witness.yml` (format 2.3) and `witness.graphml` to `<log_dir>/witness/` via the
+`witnesscreator` package. This module only checks them:
+
+- YAML: WitnessLint, if `SWAT_WITNESSLINT` names a linter command (e.g.
+  `"/path/venv/bin/python /path/witnesslint/witnesslinter.py"`); WitnessLint does not check for a
+  target segment, so the number of `target` waypoints is checked here (exactly one is expected).
+- GraphML: wit4java (the result is what `target_execution` reports as `validated`).
+
+A proper validator setup is tracked in #47.
+"""
 from contextlib import contextmanager
 import os
 import enum
 import logging
-import shutil
+import re
+import shlex
 import subprocess
 import time
 from typing import List, Optional, Tuple
 from pathlib import Path
-from .dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command
+from .dtypes import VerificationTask
 
 logger = logging.getLogger(__name__)
 SCRIPT_DIR = Path(__file__).resolve().parent.parent  # Now in lib/, so go up one more level
-WITNESS_CREATION_PATH = (SCRIPT_DIR.parent / 'WitnessCreator' / 'build' / 'libs' / 'WitnessCreator.jar')
 WITNESS_VALIDATION_PATH = (SCRIPT_DIR.parent / 'wit4java' / 'bin' / 'wit4java')
+WITNESSLINT_ENV = 'SWAT_WITNESSLINT'
+WITNESS_DIR_NAME = 'witness'
+TARGET_WAYPOINT = re.compile(r'^\s*type:\s*["\']?target["\']?\s*$')
 
 class ExecutionStatus(enum.Enum):
     SUCCESS = "success"
@@ -21,49 +35,63 @@ class ExecutionStatus(enum.Enum):
     TIMEOUT = "timeout"
 
 
+def witness_dir(ver_task: VerificationTask) -> Path:
+    """The directory the explorer writes the witness files of the task to."""
+    command_dict = ver_task.get('command') or {}
+    return Path(str(command_dict.get('log_dir', SCRIPT_DIR))) / WITNESS_DIR_NAME
 
-def generate_and_validate_witness(ver_task: VerificationTask, output: List[str]) -> Tuple[Optional[bool], float, float]:
-    """Extract witnesses from `output`, create witness files and validate them.
 
-    Returns tuple of (validation_result, generation_time, validation_time):
-        - validation_result: True/False on validation result or None if no witness was found
-        - generation_time: Time spent generating witness (seconds)
-        - validation_time: Time spent validating witness (seconds)
+def validate_witness(ver_task: VerificationTask) -> Tuple[Optional[bool], float]:
+    """Check the witness files the explorer wrote for a violation verdict.
+
+    Returns (validation_result, validation_time):
+        - validation_result: wit4java's verdict on witness.graphml (True/False), or None if no
+          witness was written
+        - validation_time: time spent validating (seconds)
     """
-    # Build an `info` dict compatible with the legacy implementation
     command_dict = ver_task.get('command', {})
     info = {
         'command': command_dict.get('command', []),
         'log_dir': str(command_dict.get('log_dir', SCRIPT_DIR))
     }
-
-    out = extract_last_round(output)
-    witnesses = extract_markers(out, "[WITNESS]")
-    if not witnesses:
-        logger.debug("No witnesses found in output")
-        return None, 0.0, 0.0
-
-    witness_dir = assemble_files(info)
-
-    logger.info("Generating witness files")
-    generation_start = time.perf_counter()
-    generate_witness(witness_dir, "\n".join(witnesses))
-    generation_time = time.perf_counter() - generation_start
+    directory = witness_dir(ver_task)
+    yaml_file = directory / 'witness.yml'
+    graphml_file = directory / 'witness.graphml'
+    if not yaml_file.exists() and not graphml_file.exists():
+        logger.warning(f"No witness files found in {directory}")
+        return None, 0.0
 
     logger.info("Validating witness")
     validation_start = time.perf_counter()
-    validation_result = validate_witness(info)
+    check_yaml_witness(yaml_file, input_dirs(info))
+    validation_result = validate_graphml_witness(info, graphml_file) if graphml_file.exists() else None
     validation_time = time.perf_counter() - validation_start
 
-    return validation_result, generation_time, validation_time
+    return validation_result, validation_time
+
+
+def input_dirs(info: dict) -> List[str]:
+    """The task's source directories (classpath entries that are directories)."""
+    try:
+        classpath_index = info['command'].index('--classpath')
+        classpath_entries = info['command'][classpath_index + 1:]
+    except ValueError:
+        classpath_entries = []
+    return [folder for folder in classpath_entries if Path(folder).is_dir()]
+
+
+def property_file(ver_task: VerificationTask) -> Path:
+    """The property file of the task, e.g. sv-benchmarks/java/properties/valid-assert.prp."""
+    return ver_task['file_path'].parent.parent / 'properties' / ver_task['category'].value
 
 
 def log_output(output: List[str]):
     for line in output:
         logger.info(line.strip())
-        
-def validate_witness(info: dict) -> bool:
-    """Run the external witness validator and return True if witness is correct."""
+
+
+def validate_graphml_witness(info: dict, witness_file: Path) -> bool:
+    """Run wit4java on the GraphML witness and return True if it reports the witness as correct."""
     cmd: List[str] = [str(WITNESS_VALIDATION_PATH), '--packages']
     main_folder = ''
 
@@ -84,7 +112,7 @@ def validate_witness(info: dict) -> bool:
             # ignore non-folders or missing paths
             continue
 
-    cmd.extend(['--witness', str(Path(info['log_dir']) / 'witness' / 'witness.graphml')])
+    cmd.extend(['--witness', str(witness_file)])
     if main_folder:
         cmd.append(main_folder)
 
@@ -95,8 +123,8 @@ def validate_witness(info: dict) -> bool:
         if "wit4java: Witness Correct" in line:
             return True
     return False
-        
-    
+
+
 @contextmanager
 def pushd(dirname):
     """Context manager to temporarily change the working directory."""
@@ -109,35 +137,41 @@ def pushd(dirname):
         os.chdir(original_dir)
 
 
-
-def extract_last_round(out: List[str], marker: str = "============================== ROUND") -> str:
-    return "\n".join(out).split(marker)[-1]
-
+def count_target_waypoints(witness_file: Path) -> int:
+    """The number of `target` waypoints in a YAML witness (a violation witness needs exactly one)."""
+    with open(witness_file, encoding='utf-8') as f:
+        return sum(1 for line in f if TARGET_WAYPOINT.match(line))
 
 
-def extract_markers(out: str, marker: str) -> List[str]:
-    res: List[str] = []
-    for line in out.split("\n"):
-        logger.debug(line)
-        if marker in line:
-            res.append(line)
-    return res
+def check_yaml_witness(witness_file: Path, inputs: List[str]) -> Optional[bool]:
+    """Check the YAML witness: exactly one target waypoint, and WitnessLint if configured.
 
-def generate_witness(witness_dir: str, witness: str) -> None:
-    with pushd(str(SCRIPT_DIR.parent / 'WitnessCreator')):
-        # base64 encode the string
-        enc = base64.b64encode(witness.encode()).decode()
-        cmd = [
-            'java',
-            '-jar',
-            str(WITNESS_CREATION_PATH),
-            enc,
-            str(witness_dir)
-        ]
-        logger.info(f"Running witness creator: {cmd}")
-        _, output = run_command_with_timeout(cmd)
-        logger.info("Witness created")
-        log_output(output)
+    Returns True iff all performed checks passed, False if one failed, None if there is no file.
+    """
+    if not witness_file.exists():
+        logger.warning(f"No YAML witness at {witness_file}")
+        return None
+    targets = count_target_waypoints(witness_file)
+    ok = targets == 1
+    logger.info(f"YAML witness target waypoints: {targets} ({'ok' if ok else 'expected exactly one'}) ({witness_file})")
+    lint = lint_witness(witness_file, inputs)
+    if lint is False:
+        ok = False
+    return ok
+
+
+def lint_witness(witness_file: Path, inputs: List[str]) -> Optional[bool]:
+    """Run WitnessLint on the YAML witness if SWAT_WITNESSLINT is set; True iff the witness is well-formed."""
+    linter = os.environ.get(WITNESSLINT_ENV)
+    if not linter or not witness_file.exists():
+        return None
+    cmd = shlex.split(linter) + ['--expectViolationWitness', '--expectedWitnessVersion', '2',
+                                 '--witness', str(witness_file)] + inputs
+    status, output = run_command_with_timeout(cmd)
+    log_output(output)
+    ok = status == ExecutionStatus.SUCCESS and any('finished with exit code 0' in line for line in output)
+    logger.info(f"WitnessLint: {'well-formed' if ok else 'FAULTY'} ({witness_file})")
+    return ok
 
 def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[ExecutionStatus, list[str]]:
     """Executes the given command and returns output from both STDOUT and STDERR."""
@@ -155,16 +189,16 @@ def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[Execut
             # Read output and wait for process to finish, with a timeout
             stdout, _ = proc.communicate(timeout=timeout)
             output = stdout.splitlines()
-        
+
             return ExecutionStatus.SUCCESS, output
-               
-            
+
+
         except subprocess.TimeoutExpired:
             proc.kill()
             stdout, _ = proc.communicate()
             output = stdout.splitlines()
             return ExecutionStatus.TIMEOUT, output
-            
+
         except Exception as e:
             logger.critical(f'[SVCOMP] Exception: {e}')
             proc.kill()
@@ -172,28 +206,3 @@ def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[Execut
             return ExecutionStatus.ERROR, output + [str(e)]
 
 
-def assemble_files(info: dict) -> str:
-    witness_dir = Path(info['log_dir']) / 'witness'
-    witness_dir.mkdir(parents=True, exist_ok=True)
-
-    try:
-        classpath_index = info['command'].index('--classpath')
-        classpath_entries = info['command'][classpath_index + 1:]
-    except ValueError:
-        classpath_entries = []
-
-    for folder in classpath_entries:
-        folder_path = Path(folder)
-        if not folder_path.exists():
-            continue
-        for src in folder_path.rglob('*.java'):
-            # Preserve relative path structure (package directories) for WitnessCreator
-            rel_path = src.relative_to(folder_path)
-            dst = witness_dir / rel_path
-            dst.parent.mkdir(parents=True, exist_ok=True)
-            logger.info(f"Copying {src} to {dst}")
-            shutil.copy(str(src), str(dst))
-
-    return str(witness_dir)
-    
-    
\ No newline at end of file