diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 138dd91..994aed3 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -3,6 +3,11 @@ name: Java CI with Gradle
 on:
   push:
   pull_request:
+  workflow_dispatch:
+
+env:
+  SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content
+  SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6
 
 jobs:
   build:
@@ -18,8 +23,142 @@ jobs:
         distribution: 'temurin'
     - name: Setup Gradle
       uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
+    - name: Prepare Solver Dependencies
+      run: ./gradlew copyNativeLibs
     - name: Build
-      run: ./gradlew build -x test
+      run: ./gradlew --no-daemon build -x test
+    - name: Build WitnessCreator JAR
+      run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar
+    - name: Upload JARs
+      if: github.event_name != 'pull_request'
+      uses: actions/upload-artifact@v4
+      with:
+        name: release-jars-${{ github.sha }}
+        path: |
+          symbolic-executor/lib/symbolic-executor.jar
+          targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar
+        if-no-files-found: error
+        retention-days: 1
+
+  package:
+    needs: build
+    if: >-
+      github.event_name == 'workflow_dispatch' ||
+      (github.event_name == 'push' && (
+        github.ref == 'refs/heads/main' ||
+        github.ref == 'refs/heads/dev' ||
+        startsWith(github.ref, 'refs/tags/')
+      ))
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+    - uses: actions/checkout@v5
+    - name: Download JARs
+      uses: actions/download-artifact@v4
+      with:
+        name: release-jars-${{ github.sha }}
+        path: ${{ runner.temp }}/release-jars
+    - name: Determine release channel
+      id: meta
+      run: |
+        ref_type="${GITHUB_REF_TYPE}"
+        ref_name="${GITHUB_REF_NAME}"
+        sha_short="${GITHUB_SHA::7}"
+
+        channel=""          # release/tag name; empty -> build artifact only, no release
+        release="false"
+        rolling="false"     # rolling channels move their tag to the current commit
+        prerelease="false"
+
+        if [[ "$ref_type" == "tag" ]]; then
+          channel="$ref_name"
+          release="true"
+        elif [[ "$ref_name" == "main" ]]; then
+          channel="latest"
+          release="true"
+          rolling="true"
+        elif [[ "$ref_name" == "dev" ]]; then
+          channel="latest-dev"
+          release="true"
+          rolling="true"
+          prerelease="true"
+        fi
+
+        # Channel-stable asset name gives the nightly cron a fixed download URL;
+        # the exact commit is recorded in the release notes and BUILD_INFO.txt.
+        if [[ -n "$channel" ]]; then
+          version="$channel"
+        else
+          version="$sha_short"
+        fi
+        zip_name="swat-svcomp-${version}.zip"
+
+        {
+          echo "channel=${channel}"
+          echo "version=${version}"
+          echo "zip-name=${zip_name}"
+          echo "release=${release}"
+          echo "rolling=${rolling}"
+          echo "prerelease=${prerelease}"
+        } >> "${GITHUB_OUTPUT}"
+    - name: Download SV-COMP reference runtime
+      run: |
+        curl --fail --location --retry 3 --output "${RUNNER_TEMP}/swat-verify.zip" "${SVCOMP_REFERENCE_URL}"
+        echo "${SVCOMP_REFERENCE_MD5}  ${RUNNER_TEMP}/swat-verify.zip" | md5sum --check -
+        unzip -q "${RUNNER_TEMP}/swat-verify.zip" -d "${RUNNER_TEMP}/swat-reference"
+    - name: Pack SV-COMP ZIP
+      env:
+        SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }}
+        SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars
+        SWAT_SVCOMP_REFERENCE_DIR: ${{ runner.temp }}/swat-reference/swat-verify
+        SWAT_SVCOMP_COMMIT: ${{ github.sha }}
+        SWAT_SVCOMP_REF: ${{ github.ref_name }}
+        SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }}
+      run: scripts/package-svcomp.sh
+    - name: Upload SV-COMP ZIP artifact
+      uses: actions/upload-artifact@v4
+      with:
+        name: swat-svcomp-${{ steps.meta.outputs.version }}
+        path: build/distributions/${{ steps.meta.outputs.zip-name }}
+        if-no-files-found: error
+    - name: Publish release
+      if: steps.meta.outputs.release == 'true'
+      env:
+        GH_TOKEN: ${{ github.token }}
+        CHANNEL: ${{ steps.meta.outputs.channel }}
+        ZIP_NAME: ${{ steps.meta.outputs.zip-name }}
+        ROLLING: ${{ steps.meta.outputs.rolling }}
+        PRERELEASE: ${{ steps.meta.outputs.prerelease }}
+      run: |
+        zip_path="build/distributions/${ZIP_NAME}"
+        notes="$(printf 'Automated SWAT SV-COMP package.\n\nRef: %s\nCommit: %s\nRun: %s/%s/actions/runs/%s\n' \
+          "$GITHUB_REF_NAME" "$GITHUB_SHA" "$GITHUB_SERVER_URL" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID")"
+
+        prerelease_flag=()
+        [[ "$PRERELEASE" == "true" ]] && prerelease_flag=(--prerelease)
+
+        if [[ "$ROLLING" == "true" ]]; then
+          # Refresh the rolling channel: drop the old release + tag, then recreate
+          # it at the current commit so the tag always tracks the channel head.
+          # Uses the default GITHUB_TOKEN, so the new tag does not retrigger CI.
+          gh release delete "$CHANNEL" --yes --cleanup-tag 2>/dev/null || true
+          gh release create "$CHANNEL" "$zip_path" \
+            --target "$GITHUB_SHA" \
+            --title "SWAT ${CHANNEL} (${GITHUB_SHA::7})" \
+            --notes "$notes" \
+            "${prerelease_flag[@]}"
+        else
+          # Permanent, version-tagged release (the tag already points at this commit).
+          if gh release view "$CHANNEL" >/dev/null 2>&1; then
+            gh release upload "$CHANNEL" "$zip_path" --clobber
+          else
+            gh release create "$CHANNEL" "$zip_path" \
+              --title "SWAT ${CHANNEL}" \
+              --notes "$notes" \
+              "${prerelease_flag[@]}"
+          fi
+        fi
 
   test:
     needs: build
@@ -82,4 +221,4 @@ jobs:
         java-version: '17'
         distribution: 'temurin'
     - name: Generate and submit dependency graph
-      uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
+      uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index 761ca1c..57b3d54 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,8 @@ targets/applications/openolat/libs/z3/
 **/logs/
 **/logs-debug/
 **/results/
+**/runs/
+**/runs-debug/
 **/*.class
 /build/
 **/build/
diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh
new file mode 100755
index 0000000..ee8ad2a
--- /dev/null
+++ b/scripts/package-svcomp.sh
@@ -0,0 +1,180 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# This script packages artifacts that were already produced by CI. It must not
+# invoke Gradle, create virtual environments, or download dependencies.
+#
+# Generated files are expected in the repository checkout after the CI build.
+# Set SWAT_SVCOMP_ARTIFACT_DIR only if those generated files live somewhere
+# else. The artifact root must contain:
+#
+# - symbolic-executor/lib/symbolic-executor.jar
+# - targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar
+#
+# Set SWAT_SVCOMP_REFERENCE_DIR to the extracted Zenodo reference package root
+# from https://zenodo.org/records/17748741. The reference root is used for the
+# pinned SV-COMP Python environment and JavaSMT compatibility JAR:
+#
+# - .venv_ubuntu_24_04_1__x86_64/
+#
+# Z3 is taken from the vendored Linux distribution ZIP in this repository.
+#
+ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+cd "$ROOT_DIR"
+
+VERSION="${SWAT_SVCOMP_VERSION:-$(git rev-parse --short HEAD)}"
+COMMIT="${SWAT_SVCOMP_COMMIT:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}"
+REF="${SWAT_SVCOMP_REF:-$(git rev-parse --abbrev-ref HEAD 2>/dev/null || echo unknown)}"
+CHANNEL="${SWAT_SVCOMP_CHANNEL:-}"
+PACKAGE_NAME="swat-svcomp-${VERSION}"
+WORK_DIR="$(mktemp -d "${TMPDIR:-/tmp}/swat-svcomp-package.XXXXXX")"
+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)"
+REFERENCE_DIR="${SWAT_SVCOMP_REFERENCE_DIR:-}"
+VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}"
+LINUX_Z3_DIST="z3-4.15.4-x64-glibc-2.39"
+LINUX_Z3_ZIP="${ROOT_DIR}/libs/${LINUX_Z3_DIST}.zip"
+
+if [[ -n "$REFERENCE_DIR" ]]; then
+  REFERENCE_DIR="$(cd "$REFERENCE_DIR" && pwd)"
+fi
+
+fail() {
+  echo "error: $*" >&2
+  exit 1
+}
+
+artifact_file() {
+  local rel="$1"
+  local path="${ARTIFACT_DIR}/${rel}"
+  [[ -f "$path" ]] || fail "missing built artifact file: ${path}"
+  printf '%s\n' "$path"
+}
+
+reference_file() {
+  local rel="$1"
+  [[ -n "$REFERENCE_DIR" ]] || fail "SWAT_SVCOMP_REFERENCE_DIR is required for ${rel}"
+
+  local path="${REFERENCE_DIR}/${rel}"
+  [[ -f "$path" ]] || fail "missing Zenodo reference file: ${path}"
+  printf '%s\n' "$path"
+}
+
+first_artifact_file() {
+  local path
+  for rel in "$@"; do
+    path="${ARTIFACT_DIR}/${rel}"
+    if [[ -f "$path" ]]; then
+      printf '%s\n' "$path"
+      return 0
+    fi
+  done
+  fail "missing built artifact file; checked: $*"
+}
+
+copy_tree_files() {
+  local src="$1"
+  local dest="$2"
+  mkdir -p "$dest"
+  find "$src" -type f \
+    ! -path '*/__pycache__/*' \
+    ! -path '*/.venv/*' \
+    ! -name '*.pyc' \
+    ! -name '*.pyo' \
+    ! -name '*.iml' \
+    -print0 | while IFS= read -r -d '' file; do
+      local rel="${file#"$src"/}"
+      mkdir -p "$dest/$(dirname "$rel")"
+      cp "$file" "$dest/$rel"
+    done
+}
+
+copy_artifact_file() {
+  local src="$1"
+  local dest="$2"
+  local mode="${3:-0644}"
+  mkdir -p "$(dirname "$dest")"
+  install -m "$mode" "$src" "$dest"
+}
+
+copy_artifact_tree() {
+  local src="$1"
+  local dest="$2"
+  [[ -d "$src" ]] || fail "missing artifact directory: ${src}"
+  mkdir -p "$(dirname "$dest")"
+  cp -a "$src" "$dest"
+}
+
+install_z3_runtime_file() {
+  local name="$1"
+  local mode="${2:-0644}"
+  local dest="${PACKAGE_DIR}/libs/java-library-path/${name}"
+
+  [[ -f "$LINUX_Z3_ZIP" ]] || fail "missing vendored Linux Z3 distribution: ${LINUX_Z3_ZIP}"
+  mkdir -p "$(dirname "$dest")"
+  unzip -p "$LINUX_Z3_ZIP" "${LINUX_Z3_DIST}/bin/${name}" > "$dest"
+  chmod "$mode" "$dest"
+}
+
+echo "Packaging repository files from: ${ROOT_DIR}"
+echo "Packaging built artifacts from: ${ARTIFACT_DIR}"
+
+echo "Creating package staging directory: ${PACKAGE_DIR}"
+mkdir -p "$PACKAGE_DIR"
+{
+  echo "version=${VERSION}"
+  echo "channel=${CHANNEL}"
+  echo "ref=${REF}"
+  echo "commit=${COMMIT}"
+} > "$PACKAGE_DIR/BUILD_INFO.txt"
+
+install -m 0644 LICENSE "$PACKAGE_DIR/LICENSE"
+install -m 0644 Third-Party-Licenses.html "$PACKAGE_DIR/Third-Party-Licenses.html"
+install -m 0644 "$SUPPORT_DIR/README.md" "$PACKAGE_DIR/README.md"
+install -m 0755 "$SUPPORT_DIR/run-swat.sh" "$PACKAGE_DIR/run-swat.sh"
+install -m 0755 "$SUPPORT_DIR/compile-target.sh" "$PACKAGE_DIR/compile-target.sh"
+install -m 0755 "$SUPPORT_DIR/smoketest.sh" "$PACKAGE_DIR/smoketest.sh"
+install -m 0755 "$SUPPORT_DIR/run_swat.py" "$PACKAGE_DIR/run_swat.py"
+install -m 0644 targets/sv-comp/sv-comp.cfg "$PACKAGE_DIR/sv-comp.cfg"
+
+EXECUTOR_JAR="$(first_artifact_file \
+  symbolic-executor/lib/symbolic-executor.jar \
+  symbolic-executor/build/libs/symbolic-executor-all.jar)"
+copy_artifact_file "$EXECUTOR_JAR" "$PACKAGE_DIR/symbolic-executor/lib/symbolic-executor.jar"
+
+copy_tree_files symbolic-explorer "$PACKAGE_DIR/symbolic-explorer"
+
+WITNESS_CREATOR_JAR="$(artifact_file targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar)"
+copy_artifact_file "$WITNESS_CREATOR_JAR" "$PACKAGE_DIR/WitnessCreator/build/libs/WitnessCreator.jar"
+mkdir -p "$PACKAGE_DIR/WitnessCreator/witnesses"
+install -m 0644 targets/sv-comp/WitnessCreator/witnesses/default_violation.st "$PACKAGE_DIR/WitnessCreator/witnesses/default_violation.st"
+install -m 0644 targets/sv-comp/WitnessCreator/witnesses/witness.st "$PACKAGE_DIR/WitnessCreator/witnesses/witness.st"
+
+install_z3_runtime_file z3 0755
+install_z3_runtime_file libz3.so
+install_z3_runtime_file libz3java.so
+install_z3_runtime_file com.microsoft.z3.jar
+install_z3_runtime_file libz3.a
+JAVA_SMT_JAR="$(reference_file libs/java-library-path/java-smt-latest.jar)"
+copy_artifact_file "$JAVA_SMT_JAR" "$PACKAGE_DIR/libs/java-library-path/java-smt-latest.jar"
+
+copy_tree_files "$SUPPORT_DIR/smoketest" "$PACKAGE_DIR/smoketest"
+
+[[ -n "$REFERENCE_DIR" ]] || fail "SWAT_SVCOMP_REFERENCE_DIR must point to the extracted Zenodo package root for ${VENV_DIR_NAME}"
+copy_artifact_tree "${REFERENCE_DIR}/${VENV_DIR_NAME}" "${PACKAGE_DIR}/${VENV_DIR_NAME}"
+
+mkdir -p "$DIST_DIR"
+ZIP_PATH="${DIST_DIR}/${PACKAGE_NAME}.zip"
+ZIP_TMP="${WORK_DIR}/${PACKAGE_NAME}.zip"
+
+echo "Creating ZIP: ${ZIP_PATH}"
+(
+  cd "$WORK_DIR"
+  zip -qr "$ZIP_TMP" "$PACKAGE_NAME"
+)
+cp "$ZIP_TMP" "$ZIP_PATH"
+
+echo "Package created at: ${ZIP_PATH}"
+echo "Staging directory left at: ${PACKAGE_DIR}"
diff --git a/scripts/svcomp-package/README.md b/scripts/svcomp-package/README.md
new file mode 100644
index 0000000..46852fd
--- /dev/null
+++ b/scripts/svcomp-package/README.md
@@ -0,0 +1,19 @@
+# SWAT SV-COMP Package
+
+This archive contains a runnable SWAT package for SV-COMP style Java verification tasks.
+
+Important entry points:
+
+- `run-swat.sh`: verifier entry point used by BenchExec.
+- `compile-target.sh`: helper used by `run_swat.py` to compile Java benchmark sources.
+- `smoketest.sh`: runs SWAT on two bundled smoke-test targets.
+- `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.
+
+Example:
+
+```sh
+./run-swat.sh ../../sv-benchmarks/java/properties/valid-assert.prp smoketest/common smoketest
+```
diff --git a/scripts/svcomp-package/compile-target.sh b/scripts/svcomp-package/compile-target.sh
new file mode 100755
index 0000000..5d2e5ff
--- /dev/null
+++ b/scripts/svcomp-package/compile-target.sh
@@ -0,0 +1,35 @@
+#!/bin/bash
+
+# Check if at least two arguments are provided
+if [ "$#" -lt 2 ]; then
+    echo "Usage: $0 <classpath1> ... <target_file>"
+    exit 1
+fi
+
+# Check if the fourth argument ends with 'rbtree' and swap if true
+if [[ "${4}" == *rbtree ]]; then
+    temp=$3
+    set -- "${@:1:2}" "$4" "$temp" "${@:5}"
+fi
+
+# print all params
+shift # Remove the first argument (property file)
+
+# Extract the target file (last argument)
+target_directory="${!#}"  # Get the last argument
+
+# Construct the classpath using all remaining arguments except the last one
+classpath=$(IFS=:; echo "${*:1:$#-1}/")
+
+build_directory="$target_directory/build"
+
+#echo $target_directory $classpath $build_directory
+# Create the build directory if it doesn't exist
+mkdir -p "$build_directory"
+
+# Use find to get all .java files recursively from the target directory
+java_files=$(find "$target_directory" -name "*.java")
+
+echo "javac  -source 1.8 -target 1.8 -cp \"$classpath\" -d \"$build_directory\" $java_files"
+# Compile all the found .java files
+javac  -source 1.8 -target 1.8 -cp "$classpath" -d "$build_directory" $java_files
\ No newline at end of file
diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh
new file mode 100755
index 0000000..fc21ac2
--- /dev/null
+++ b/scripts/svcomp-package/run-swat.sh
@@ -0,0 +1,66 @@
+#!/bin/bash
+
+
+# Check if the '-v' argument is among the arguments, indicating that the user wants to see the version
+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
+  fi
+done
+
+# get last argument
+last_path="${@: -1}"
+
+# get second last argument
+second_last_path="${*: -2:1}"
+
+# check if there is a Main.java in last_path
+if [ -f "$second_last_path/Main.java" ]; then
+    # switch the last two arguments
+    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)"
+source "$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/activate"
+echo "Running SWAT with arguments: $@"
+python3 -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1
+cat out.log
\ No newline at end of file
diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py
new file mode 100755
index 0000000..6b88333
--- /dev/null
+++ b/scripts/svcomp-package/run_swat.py
@@ -0,0 +1,239 @@
+from contextlib import contextmanager
+import logging, os, enum, subprocess, sys, base64, uuid
+
+import concurrent.futures, json, datetime
+from typing import List, Optional
+
+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')
+
+
+class ExecutionStatus(enum.Enum):
+    SUCCESS = "success"
+    ERROR = "error"
+    TIMEOUT = "timeout"
+
+class Verdict(enum.Enum):
+    VIOLATION = "== ERROR"
+    SAFE = "== OK"
+    UNKNOWN = "== DONT-KNOW"
+    NO_SYMBOLIC_VARS = "== NON-SYMBOLIC"
+
+@contextmanager
+def pushd(dirname):
+    """Context manager to temporarily change the working directory."""
+    original_dir = os.getcwd()
+    logger.info(f"Changing directory to: {dirname}")
+    os.chdir(dirname)
+    try:
+        yield
+    finally:
+        os.chdir(original_dir)
+
+def determine_result(output: List[str], property_file: str) -> Verdict:
+    """Parse the verdict for a specific property from the output."""
+    verdict = None
+    for line in output:
+        if f"[VERDICT {property_file}]" in line:
+            if "== OK" in line:
+                verdict = Verdict.SAFE
+                break
+            elif "== ERROR" in line:
+                verdict = Verdict.VIOLATION
+                break
+            elif "== DONT-KNOW" in line:
+                verdict = Verdict.UNKNOWN
+                break
+    return verdict
+
+
+
+
+
+
+def run_command_with_timeout(cmd: list[str], timeout: int | None = None) -> tuple[ExecutionStatus, list[str]]:
+    """Executes the given command and returns output from both STDOUT and STDERR.
+
+    timeout=None (the default) imposes no internal cutoff so SWAT can use the full
+    SV-COMP time budget; benchexec enforces the wall/CPU limit externally.
+    """
+
+    logger.info(f'[TARGET EXECUTION]: Running command: {cmd}')
+    output = []
+    with subprocess.Popen(
+            cmd,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.STDOUT,
+            universal_newlines=True,
+            bufsize=1
+    ) as proc:
+        try:
+            # 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()
+            output = [str(e)]
+            return ExecutionStatus.ERROR, output + [str(e)]
+
+
+
+
+
+def generate_command(args, property_file: str):
+    config_file = 'sv-comp.cfg'
+
+    agent_path = os.path.join(SCRIPT_DIR, 'symbolic-executor', 'lib', 'symbolic-executor.jar')
+    config_path = os.path.join(SCRIPT_DIR, config_file)
+    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'),
+                     "-prp", property_file,
+                     "--agent", agent_path,
+                     "--config", config_path,
+                     "-z3", library_path,
+                     "--logdir", logging_dir,
+                     "--mode", "sv-comp",
+                     '--port', "8000",
+                     "--classpath"]
+    print("CP args: " + str(args))
+    for arg in args[1:]:
+        print("CP arg: " + arg)
+        print("CP arg path: " + os.path.join(SCRIPT_DIR, arg))
+        base_command.append(os.path.join(SCRIPT_DIR, arg))
+    return base_command
+
+
+def copy_target(target_dir):
+    # generate random target tmp name
+    local_target_dir = f"target_{uuid.uuid4()}"
+
+    os.system(f'rm -rf {local_target_dir} && cp -r {target_dir} {local_target_dir}')
+    print(f"Target copied from {target_dir} to: {local_target_dir}")
+    return local_target_dir
+
+def compile_target(args, local_target_dir):
+    cmd = [
+        'bash',
+        f'compile-target.sh',
+    ]
+    args[-1] = local_target_dir # overwrite target dir
+    cmd = cmd + args
+    print(cmd)
+    _, output = run_command_with_timeout(cmd)
+    log_output(output)
+
+
+def extract_last_round(out, marker="============================== ROUND"):
+
+    return "\n ".join(out).split(marker)[-1]
+
+
+def extract_markers(out, marker):
+    res = []
+    for line in out.split("\n"):
+        print(line)
+        if marker in line:
+            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 log_output(output: List[str]):
+    for line in output:
+        logger.info(line.strip())
+
+if __name__ == "__main__":
+    logger.info("Running SWAT Wrapper...")
+
+    # Look for property file in arguments
+    # SV-COMP framework passes the .prp file directly as first argument
+    property_file = None
+    for arg in sys.argv[1:]:
+        if arg.endswith('.prp'):
+            property_file = os.path.basename(arg)
+            logger.info(f"Found property file in arguments: {property_file}")
+            break
+
+    if property_file is None:
+        logger.error(f"ERROR: No .prp file found in arguments.")
+        logger.error(f"Arguments: {sys.argv}")
+        exit(1)
+
+    logger.info(f"Using property file: {property_file}")
+
+    target_dir = sys.argv[-1]
+    cmd = generate_command(sys.argv[1:], property_file)
+    local_target_dir = copy_target(target_dir)
+    compile_target(sys.argv[1:], local_target_dir)
+
+    path = local_target_dir
+    log_dir = f'{path}/logs'
+
+    cmd[-1] = os.path.join(SCRIPT_DIR, local_target_dir, 'build') #f"{local_target_dir}/build"
+    #delete the dir if it exists
+    if os.path.exists(log_dir):
+        os.system(f'rm -rf {log_dir}')
+    os.makedirs(log_dir)
+    with pushd(path):
+        execution_status, output = run_command_with_timeout(cmd)
+        log_output(output)
+        print(f"Execution status: {execution_status}")
+        if execution_status == ExecutionStatus.TIMEOUT or execution_status == ExecutionStatus.ERROR:
+            print(f'Error: {output}')
+            exit(1)
+
+
+        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}")
+        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
new file mode 100755
index 0000000..95fb8c0
--- /dev/null
+++ b/scripts/svcomp-package/smoketest.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+cd "$(dirname "$0")"
+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!"
+    exit 1
+fi
+
diff --git a/scripts/svcomp-package/smoketest/Main.java b/scripts/svcomp-package/smoketest/Main.java
new file mode 100644
index 0000000..7362ba8
--- /dev/null
+++ b/scripts/svcomp-package/smoketest/Main.java
@@ -0,0 +1,10 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+public class Main {
+  public static void main(String[] args) {
+    // Fetch inputs using Verifier.nondet* methods
+    int i = Verifier.nondetInt();
+
+    assert i != 42;
+  }
+}
diff --git a/scripts/svcomp-package/smoketest/common/Verifier.java b/scripts/svcomp-package/smoketest/common/Verifier.java
new file mode 100644
index 0000000..7fd2399
--- /dev/null
+++ b/scripts/svcomp-package/smoketest/common/Verifier.java
@@ -0,0 +1,60 @@
+// This file is part of the SV-Benchmarks collection of verification tasks:
+// https://github.com/sosy-lab/sv-benchmarks
+//
+// SPDX-FileCopyrightText: Contributed by Peter Schrammel
+// SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.sv_benchmarks;
+
+import java.util.Random;
+
+public final class Verifier {
+  public static void assume(boolean condition) {
+    if (!condition) {
+      Runtime.getRuntime().halt(1);
+    }
+  }
+
+  public static boolean nondetBoolean() {
+    return new Random().nextBoolean();
+  }
+
+  public static byte nondetByte() {
+    return (byte) (new Random().nextInt());
+  }
+
+  public static char nondetChar() {
+    return (char) (new Random().nextInt());
+  }
+
+  public static short nondetShort() {
+    return (short) (new Random().nextInt());
+  }
+
+  public static int nondetInt() {
+    return new Random().nextInt();
+  }
+
+  public static long nondetLong() {
+    return new Random().nextLong();
+  }
+
+  public static float nondetFloat() {
+    return new Random().nextFloat();
+  }
+
+  public static double nondetDouble() {
+    return new Random().nextDouble();
+  }
+
+  public static String nondetString() {
+    Random random = new Random();
+    int size = random.nextInt();
+    assume(size >= 0);
+    byte[] bytes = new byte[size];
+    random.nextBytes(bytes);
+    return new String(bytes);
+  }
+}
diff --git a/settings.gradle b/settings.gradle
index defcd23..b7434f5 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -68,7 +68,7 @@ dependencyResolutionManagement {
             library('asm-tree', 'org.ow2.asm','asm-tree').versionRef('asm')
             library('jackson-databind', 'com.fasterxml.jackson.core:jackson-databind:2.14.1')
             library('java-smt', 'org.sosy-lab:java-smt:6.0.0')
-            library('spock-core', 'org.spockframework:spock-core:2.2-M1-groovy-4.0')
+            library('spock-core', 'org.spockframework:spock-core:2.2-groovy-4.0')
             library('mockito-core', 'org.mockito:mockito-core:3.12.4')
             library('logback-classic', 'ch.qos.logback:logback-classic:1.5.3')
             library('logback-core', 'ch.qos.logback:logback-core:1.5.3')
diff --git a/symbolic-executor/build.gradle b/symbolic-executor/build.gradle
index 0b7932b..9484147 100644
--- a/symbolic-executor/build.gradle
+++ b/symbolic-executor/build.gradle
@@ -50,12 +50,31 @@ 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
+    }
 
     testLogging {
         // Show events for passed, skipped, and failed tests
         events "passed", "failed", "skipped"
         // Enable standard output/error to be shown
-        showStandardStreams = true
+        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
+    systemProperty "exitOnError", "false"
+    
+    useJUnitPlatform()
+
+    testLogging {
+        // Show events for passed, skipped, and failed tests
+        events "passed", "failed", "skipped"
+        // Enable standard output/error to be shown
+        showStandardStreams = false
     }
 }
 
@@ -105,10 +124,6 @@ tasks.register('copyJar', Copy) {
 }
 
 
-test {
-    useJUnitPlatform()
-}
-
 // Set duplicate strategy to remove a warning
 // distTar.setDuplicatesStrategy(DuplicatesStrategy.INCLUDE)
 // distZip.setDuplicatesStrategy(DuplicatesStrategy.INCLUDE)
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java
index 7f89493..18a888a 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/ErrorHandler.java
@@ -5,12 +5,9 @@
 import ch.qos.logback.core.FileAppender;
 import de.uzl.its.swat.common.exceptions.SWATException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.config.Config;
 import de.uzl.its.swat.thread.ThreadHandler;
 
-import java.util.Arrays;
-
 import static java.lang.Thread.currentThread;
 /**
  * ErrorHandler is responsible for handling exceptions throughout the application. It decides
@@ -73,14 +70,6 @@ public void handleException(String msg, Throwable t) {
             throw new RuntimeException(msg, t);
         }
         logger.error("Preparing to halt execution due to error...");
-        try {
-            if (ThreadHandler.hasThreadContext(currentThread().getId())) {
-                ThreadHandler.logStats(currentThread().getId());
-            }
-            ThreadHandler.logStats(-1);
-        } catch (Exception e) {
-            logger.error("Error while logging stats");
-        }
         logger.error("Halting...");
         if (!config.isLogShadowStateToConsole()) {
             logger.info("Flushing loggers...");
@@ -100,28 +89,6 @@ public void handleException(String msg, Throwable t) {
 
     public void logException(String msg, Throwable t){
         logger.error(msg, t);
-        long threadId = currentThread().getId();
-        String executionStage;
-        if(ThreadHandler.hasThreadContext(threadId)){
-            try {
-                executionStage = ThreadHandler.getCurrentInstruction(threadId).toString();
-            } catch (Exception e) {
-                logger.error("Error while getting current instruction", e);
-                executionStage = "Unknown";
-            }
-        }  else {
-            executionStage = "Main Thread";
-            threadId = -1;
-        }
-
-        // Record the error
-        ErrorRecord errorRecord = new ErrorRecord(msg, t.getClass().getSimpleName(),
-                Arrays.toString(t.getStackTrace()), t.getMessage(), executionStage);
-        try{
-            ThreadHandler.recordException(threadId, errorRecord);
-        } catch (Exception e) {
-            logger.error("Error while recording exception", e);
-        }
     }
 
 }
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java
index ee4c341..e8859b9 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/exceptions/SWATAssert.java
@@ -3,7 +3,6 @@
 import ch.qos.logback.classic.Logger;
 import de.uzl.its.swat.common.ErrorHandler;
 import de.uzl.its.swat.common.logging.GlobalLogger;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.config.Config;
 import de.uzl.its.swat.symbolic.instruction.Instruction;
 import de.uzl.its.swat.thread.ThreadContext;
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java
index 6c6cfd3..cbf961c 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/StatsStorage.java
@@ -1,55 +1,32 @@
 package de.uzl.its.swat.common.logging;
 
-import com.fasterxml.jackson.core.JsonProcessingException;
-import com.fasterxml.jackson.databind.ObjectMapper;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.common.logging.records.InvocationEntry;
 import lombok.Getter;
 
-import java.util.ArrayList;
 import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-
+import java.util.HashSet;
+import java.util.Set;
+
+/**
+ * In-memory accumulator for per-execution statistics: the methods that could not be modelled
+ * symbolically ({@link #invocations}) and the subset of those that caused symbolic context loss
+ * ({@link #contextLossInvocations}). This data is attached to the trace and sent to the Symbolic
+ * Explorer (see {@code DTOBuilder}); the explorer owns the consolidated per-testcase output. The
+ * executor itself no longer writes any stats file.
+ */
 @Getter
 public class StatsStorage {
-    private String entrypoint;
     private final HashMap<InvocationEntry, Integer> invocations;
-    private final ArrayList<ErrorRecord> errors;
+    // Subset of invocations that received symbolic arguments and therefore caused context loss.
+    private final Set<InvocationEntry> contextLossInvocations;
 
     public StatsStorage() {
         this.invocations = new HashMap<>();
-        this.errors = new ArrayList<>();
+        this.contextLossInvocations = new HashSet<>();
     }
 
-    public String convertToJson() throws JsonProcessingException {
-        ObjectMapper mapper = new ObjectMapper();
-        List<Map<String, Object>> serializedList = new ArrayList<>();
-
-        invocations.forEach((entry, count) -> {
-            Map<String, Object> entryMap = new HashMap<>();
-            entryMap.put("owner", entry.owner());
-            entryMap.put("name", entry.name());
-            entryMap.put("desc", entry.desc());
-            entryMap.put("isInstance", entry.isInstance());
-            entryMap.put("invokeId", entry.invokeId());
-            entryMap.put("isSymbolic", entry.isSymbolic());
-            entryMap.put("count", count);  // Store the count as well
-
-            serializedList.add(entryMap);
-        });
-        errors.forEach(error -> {
-            Map<String, Object> errorMap = new HashMap<>();
-            errorMap.put("message", error.message());
-            errorMap.put("type", error.type());
-            errorMap.put("stackTrace", error.stackTrace());
-            errorMap.put("exceptionMessage", error.exceptionMessage());
-            errorMap.put("executionStage", error.executionStage());
-
-            serializedList.add(errorMap);
-        });
-
-        return mapper.writeValueAsString(serializedList);  // Convert the list of maps to JSON
+    /** Marks an already-recorded missing invocation as a context-loss culprit. */
+    public void recordContextLossInvocation(InvocationEntry entry) {
+        contextLossInvocations.add(entry);
     }
 }
-
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/records/ErrorRecord.java b/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/records/ErrorRecord.java
deleted file mode 100644
index 0322708..0000000
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/common/logging/records/ErrorRecord.java
+++ /dev/null
@@ -1,4 +0,0 @@
-package de.uzl.its.swat.common.logging.records;
-
-public record ErrorRecord(String message, String type, String stackTrace, String exceptionMessage, String executionStage) {
-}
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 0561ae1..48061c8 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
@@ -108,8 +108,6 @@ public static void terminate() {
         try {
             Transformer.logMissedClasses();
             ThreadHandler.disableThreadContext(currentThread().getId());
-            ThreadHandler.logStats(currentThread().getId());
-            ThreadHandler.logStats(-1);
             logger.info(
                     new PrintBox(
                             60,
@@ -140,7 +138,7 @@ public static void terminate() {
                     break;
                 case PRINT:
                     if (!ThreadHandler.isThreadContextAborted(currentThread().getId())) {
-                        System.out.println(ThreadHandler.getSymbolicVisitor(currentThread().getId()).getSymbolicTraceHandler().getTraceDTO());
+                        System.out.println(ThreadHandler.getSymbolicVisitor(currentThread().getId()).getSymbolicTraceHandler().getTraceDTO(ThreadHandler.getStatsStorage(currentThread().getId())));
                     }
                     break;
                 case NONE:
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java
index d1c465b..2150713 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java
@@ -96,13 +96,15 @@ public class InvocationHandler {
             }
 
 
-            ThreadHandler.recordMissingInvocation(Thread.currentThread().getId(),  new InvocationEntry(
+            long threadId = Thread.currentThread().getId();
+            InvocationEntry entry = new InvocationEntry(
                     owner,
                     name,
                     desc,
                     isInstance,
                     invokeId,
-                    containsSymbolicArgument));
+                    containsSymbolicArgument);
+            ThreadHandler.recordMissingInvocation(threadId, entry);
 
             if(
                     (retValue.equals(PlaceHolder.instance) // To detect a missing implementation
@@ -114,6 +116,9 @@ public class InvocationHandler {
                         owner,
                         desc);
                 symbolicTraceHandler.recordSymbolicContextLoss();
+                // Record the culprit so the explorer can compute the context-loss subset of the
+                // missing invocations without scraping logs.
+                ThreadHandler.recordContextLossInvocation(threadId, entry);
             }
 
         }
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java
index 8cf11a6..a716713 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java
@@ -21,15 +21,20 @@ public class Frame {
     /** Number of words that are returned on invoke method end */
     public final int nReturnWords;
     /** The symbolic version of Javas locals */
-    @Getter private final ArrayList<Value<?, ?>> locals = new ArrayList<>(8);
+    @Getter
+    private final ArrayList<Value<?, ?>> locals = new ArrayList<>(8);
     /** The symbolic version of Javas operand stack */
-    @Getter private final ArrayList<Value<?, ?>> operandStack = new ArrayList<>(8);
+    @Getter
+    private final ArrayList<Value<?, ?>> operandStack = new ArrayList<>(8);
     /** The return value of the symbolic stack frame */
-    @Getter private Value<?, ?> ret;
+    @Getter
+    private Value<?, ?> ret;
     /** The class name of the method that is invoked */
-    @Getter private final String className;
+    @Getter
+    private final String className;
     /** The method name of the method that is invoked */
-    @Getter private final String methodName;
+    @Getter
+    private final String methodName;
 
     /**
      * Constructor for Frame
@@ -249,14 +254,19 @@ public void printStack() throws NoThreadContextException {
         // purposes.
         Logger stateLogger = ThreadHandler.getShadowStateLogger(id);
 
-        int cnt = 3;
+        int cnt = 4;
         for (int i = operandStack.size() - 1; i >= 0; i--) {
             stateLogger.info("[{}]: {}", operandStack.size() - i, operandStack.get(i));
-            if(--cnt == 0) break;
+            if (--cnt == 0)
+                break;
         }
         int remaining = operandStack.size() - 4;
-        if (remaining >= 0) stateLogger.info("... ({} more)", remaining);
+        if (remaining > 0)
+            stateLogger.info("... ({} more)", remaining);
+
+        // stateLogger.info("LOCALS: {}", locals);
     }
+
     /**
      * Override of the default toString method for printing the Current symbolic stack frame and
      * locals
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 8fa442e..e1156b9 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
@@ -11,12 +11,15 @@
 import de.uzl.its.swat.common.exceptions.NoThreadContextException;
 import de.uzl.its.swat.common.exceptions.NotImplementedException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.common.logging.StatsStorage;
+import de.uzl.its.swat.common.logging.records.InvocationEntry;
 import de.uzl.its.swat.coverage.InstrCoverage;
 import de.uzl.its.swat.symbolic.trace.dto.*;
 import de.uzl.its.swat.thread.ThreadHandler;
 import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Map;
 
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
@@ -34,8 +37,33 @@ class DTOBuilder {
      * @param symbolicTrace The symbolic trace to be encoded.
      * @return The symbolic trace encoded as a JSON string.
      */
-    protected static String encodeTrace(SymbolicTrace symbolicTrace) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
-        return buildRequestBody(buildTraceDTO(symbolicTrace));
+    protected static String encodeTrace(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
+        return buildRequestBody(buildTraceDTO(symbolicTrace, statsStorage));
+    }
+
+    /**
+     * Builds the list of missing-invocation DTOs from the per-execution statistics. The full set of
+     * missing invocations is the superset; entries present in the context-loss set are flagged so
+     * the explorer can compute the context-loss subset without log scraping.
+     *
+     * @param statsStorage The per-execution statistics accumulator.
+     * @return The missing invocations encoded as DTOs.
+     */
+    private static ArrayList<InvocationDTO> buildMissingInvocations(StatsStorage statsStorage) {
+        ArrayList<InvocationDTO> missingInvocations = new ArrayList<>();
+        for (Map.Entry<InvocationEntry, Integer> e : statsStorage.getInvocations().entrySet()) {
+            InvocationEntry entry = e.getKey();
+            missingInvocations.add(
+                    new InvocationDTO(
+                            entry.owner(),
+                            entry.name(),
+                            entry.desc(),
+                            entry.isInstance(),
+                            entry.isSymbolic(),
+                            statsStorage.getContextLossInvocations().contains(entry),
+                            e.getValue()));
+        }
+        return missingInvocations;
     }
 
     /**
@@ -46,7 +74,7 @@ protected static String encodeTrace(SymbolicTrace symbolicTrace) throws NoThread
      * @return A {@link TraceDTO ConstraintDTO} that contains relevant all relevant information
      *     to transfer symbolic traces
      */
-    private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace) throws NoThreadContextException, NotImplementedException {
+    private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, NotImplementedException {
         ArrayList<InputDTO> inputs = new ArrayList<>();
         ArrayList<UFDTO> ufs = new ArrayList<>();
         ArrayList<BranchDTO> trace = new ArrayList<>();
@@ -106,7 +134,7 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace) throws NoThre
                 trace.add(new BranchDTO(se.getIid(), se.getInst()));
             }
         }
-        return new TraceDTO(inputs, trace, ufs, symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange());
+        return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), 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 6d99da5..0211915 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
@@ -6,6 +6,7 @@
 import de.uzl.its.swat.common.exceptions.NoThreadContextException;
 import de.uzl.its.swat.common.exceptions.NotImplementedException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
+import de.uzl.its.swat.common.logging.StatsStorage;
 import de.uzl.its.swat.symbolic.value.Value;
 import de.uzl.its.swat.thread.ThreadHandler;
 import java.util.ArrayList;
@@ -108,8 +109,8 @@ public List<BooleanFormula> getConstraints() {
      *
      * @return The symbolic trace encoded as a JSON string.
      */
-    public String getTraceDTO() throws NoThreadContextException, JsonProcessingException, NotImplementedException {
-        return DTOBuilder.encodeTrace(symbolicTrace);
+    public String getTraceDTO(StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
+        return DTOBuilder.encodeTrace(symbolicTrace, statsStorage);
     }
 
     /**
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/InvocationDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/InvocationDTO.java
new file mode 100644
index 0000000..1ecef89
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/InvocationDTO.java
@@ -0,0 +1,55 @@
+package de.uzl.its.swat.symbolic.trace.dto;
+
+/**
+ * Describes a single method invocation that could not be modelled symbolically during execution
+ * (i.e. it returned a {@link de.uzl.its.swat.symbolic.value.PlaceHolder}). These are collected per
+ * execution and shipped to the Symbolic Explorer as part of the trace so that the explorer owns the
+ * consolidated per-testcase statistics instead of relying on log/stats-file scraping.
+ *
+ * <p>{@code contextLoss} marks the dangerous subset: invocations that received symbolic arguments
+ * and therefore caused symbolic context loss (see {@code InvocationHandler}). Missing invocations
+ * are the superset; context-loss invocations are the subset.
+ */
+public class InvocationDTO {
+    @SuppressWarnings("unused")
+    private String owner;
+
+    @SuppressWarnings("unused")
+    private String name;
+
+    @SuppressWarnings("unused")
+    private String desc;
+
+    @SuppressWarnings("unused")
+    private boolean isInstance;
+
+    @SuppressWarnings("unused")
+    private boolean isSymbolic;
+
+    @SuppressWarnings("unused")
+    private boolean contextLoss;
+
+    @SuppressWarnings("unused")
+    private int count;
+
+    public InvocationDTO(
+            String owner,
+            String name,
+            String desc,
+            boolean isInstance,
+            boolean isSymbolic,
+            boolean contextLoss,
+            int count) {
+        this.owner = owner;
+        this.name = name;
+        this.desc = desc;
+        this.isInstance = isInstance;
+        this.isSymbolic = isSymbolic;
+        this.contextLoss = contextLoss;
+        this.count = count;
+    }
+
+    /** Private default constructor for serialization */
+    @SuppressWarnings("unused")
+    private InvocationDTO() {}
+}
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 2f8b394..75eaf69 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
@@ -12,6 +12,11 @@ public class TraceDTO {
     @SuppressWarnings("unused")
     private ArrayList<UFDTO> ufs;
 
+    // The methods encountered during execution that could not be modelled symbolically. The
+    // superset of all missing invocations; entries with contextLoss=true are the dangerous subset.
+    @SuppressWarnings("unused")
+    private ArrayList<InvocationDTO> missingInvocations;
+
     @SuppressWarnings("unused")
     private boolean symbolicContextLoss = false;
     @SuppressWarnings("unused")
@@ -19,10 +24,11 @@ public class TraceDTO {
     @SuppressWarnings("unused")
     private boolean referenceSemanticChange = false;
 
-    public TraceDTO(ArrayList<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) {
+    public TraceDTO(ArrayList<InputDTO> inputs, ArrayList<BranchDTO> trace, ArrayList<UFDTO> ufs, ArrayList<InvocationDTO> missingInvocations, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) {
         this.trace = trace;
         this.inputs = inputs;
         this.ufs = ufs;
+        this.missingInvocations = missingInvocations;
         this.symbolicContextLoss = symbolicContextLoss;
         this.symbolicPrecisionLoss = symbolicPrecisionLoss;
         this.referenceSemanticChange = referenceSemanticChange;
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java
index ebba905..24f8d59 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java
@@ -69,6 +69,7 @@ public BooleanFormula IF_ACMPNE(ObjectValue o2) {
             return super.IF_ACMPNE(o2);
         }
     }
+
     /**
      * Compares if two references are identical
      *
@@ -91,10 +92,10 @@ public Object getConcrete() {
     }
 
     public String MAKE_SYMBOLIC(String prefixOrIdx) {
-        if (prefixOrIdx.matches("-?\\d+")){
+        if (prefixOrIdx.matches("-?\\d+")) {
             // We assume a constructed idx was passed as it is a number
             initSymbolic(symbolicPrefix, prefixOrIdx);
-        } else if (prefixOrIdx.matches(".*-?\\d+")){
+        } else if (prefixOrIdx.matches(".*-?\\d+")) {
             // Its a list which already has prefix and idx
             initSymbolicWithoutIdx(prefixOrIdx);
         } else {
@@ -110,6 +111,7 @@ public String MAKE_SYMBOLIC() {
         formula = smgr.makeVariable(name);
         return name;
     }
+
     /**
      * Turns this IntValue into a symbolic variable
      *
@@ -146,7 +148,8 @@ public BooleanFormula getBounds(boolean upper) {
      *     implemented or void should be returned
      */
     @Override
-    public Value<?, ?> invokeMethod(String name, Type[] desc, Value<?, ?>[] args) throws NotImplementedException, ValueConversionException {
+    public Value<?, ?> invokeMethod(String name, Type[] desc, Value<?, ?>[] args)
+            throws NotImplementedException, ValueConversionException {
         return switch (name) {
             case "<init>" -> invokeInit(args, desc);
             case "charAt" -> invokeCharAt(args, desc);
@@ -215,7 +218,7 @@ public BooleanFormula getBounds(boolean upper) {
      * @return The resulting Value or PlaceHolder::instance
      */
     private Value<?, ?> invokeInit(Value<?, ?>[] args, Type[] desc) {
-        if(args.length == 1 && args[0] instanceof StringValue s) {
+        if (args.length == 1 && args[0] instanceof StringValue s) {
             this.concrete = s.concrete;
             this.formula = s.formula;
         }
@@ -236,7 +239,8 @@ public BooleanFormula getBounds(boolean upper) {
      *     the Value in args is of the same type.
      * @return The resulting Value or PlaceHolder::instance
      */
-    private Value<?, ?> invokeCharAt(Value<?, ?>[] args, Type[] desc) throws NotImplementedException, ValueConversionException {
+    private Value<?, ?> invokeCharAt(Value<?, ?>[] args, Type[] desc)
+            throws NotImplementedException, ValueConversionException {
         if (args.length == 1) {
             IntValue index = args[0].asIntValue();
             char result = concrete.charAt(index.concrete);
@@ -502,8 +506,7 @@ public BooleanFormula getBounds(boolean upper) {
             BooleanFormula constraints = uf.createEqualsIgnoreCaseConstraints(
                     this.formula, rhs.formula,
                     this.concrete, rhs.concrete,
-                    this.isSymbolic(), rhs.isSymbolic()
-            );
+                    this.isSymbolic(), rhs.isSymbolic());
             ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).addConstraint(constraints);
 
             // also carry the concrete result for concolic steering
@@ -516,7 +519,6 @@ public BooleanFormula getBounds(boolean upper) {
         }
     }
 
-
     /**
      * Invocation handling for the String instance method <a
      * href="https://docs.oracle.com/en/java/javase/16/docs/api/java.base/java/lang/String.html#Formatted">Formatted</a>().
@@ -566,8 +568,8 @@ public BooleanFormula getBounds(boolean upper) {
                 CharArrayValue dst = args[2].asObjectValue().asArrayValue().asCharArrayValue();
                 IntValue dstBegin = args[3].asIntValue();
                 for (int idx = srcBegin.concrete; idx < srcEnd.concrete; idx++) {
-                    Value<?, ?>[] charAtArgs = new Value[] {new IntValue(context, idx)};
-                    Type[] charAtDesc = new Type[] {Type.INT_TYPE};
+                    Value<?, ?>[] charAtArgs = new Value[] { new IntValue(context, idx) };
+                    Type[] charAtDesc = new Type[] { Type.INT_TYPE };
                     dst.storeElement(
                             new IntValue(context, dstBegin.concrete + idx),
                             (CharValue) invokeCharAt(charAtArgs, charAtDesc));
@@ -624,7 +626,8 @@ public BooleanFormula getBounds(boolean upper) {
      *     the Value in args is of the same type.
      * @return The resulting Value or PlaceHolder::instance
      */
-    private Value<?, ?> invokeIndexOf(Value<?, ?>[] args, Type[] desc) throws NotImplementedException, ValueConversionException {
+    private Value<?, ?> invokeIndexOf(Value<?, ?>[] args, Type[] desc)
+            throws NotImplementedException, ValueConversionException {
         if (args.length == 1) {
             return switch (desc[0].getDescriptor()) {
                 case "I" -> invokeIndexOf(args[0].asIntValue());
@@ -823,7 +826,8 @@ public BooleanFormula getBounds(boolean upper) {
      *     the Value in args is of the same type.
      * @return The resulting Value or PlaceHolder::instance
      */
-    private Value<?, ?> invokeReplace(Value<?, ?>[] args, Type[] desc) throws NotImplementedException, ValueConversionException {
+    private Value<?, ?> invokeReplace(Value<?, ?>[] args, Type[] desc)
+            throws NotImplementedException, ValueConversionException {
         if (args.length == 2) {
             return switch (desc[0].getDescriptor()) {
                 case "C" -> invokeReplace(args[0].asCharValue(), args[1].asCharValue());
@@ -836,17 +840,20 @@ public BooleanFormula getBounds(boolean upper) {
     }
 
     private Value<?, ?> invokeReplace(ObjectValue<?, ?> target, ObjectValue<?, ?> replacement) {
-        if (target instanceof StringValue s1 && replacement instanceof StringValue s2) {
+        if (target instanceof StringValue oldString && replacement instanceof StringValue newString) {
             // ToDo  (Nils): This is the correct implementation. However replaceAll is currently not
             // supported by Z3
             /*
-            this.formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula);
+            formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula);
              */
-            this.concrete = this.concrete.replace(s1.concrete, s2.concrete);
+
+            var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete);
+            var newFormula = this.formula;
             for (int i = 0; i < REPLACE_COUNT; i++) {
-                this.formula = smgr.replace(this.formula, s1.formula, s2.formula);
+                newFormula = smgr.replace(newFormula, oldString.formula, newString.formula);
             }
-            return this;
+
+            return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN);
         } else {
             return PlaceHolder.instance;
         }
@@ -858,16 +865,17 @@ public BooleanFormula getBounds(boolean upper) {
         // ToDo  (Nils): This is the correct implementation. However replaceAll is currently not
         // supported by Z3
         // See: https://git.its.uni-luebeck.de/research-projects/pet-hmr/knife-fuzzer/-/issues/54
-
         /*
-        this.formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula);
+        formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula);
          */
-        this.concrete = this.concrete.replace(oldString.concrete, newString.concrete);
+
+        var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete);
+        var newFormula = this.formula;
         for (int i = 0; i < REPLACE_COUNT; i++) {
-            this.formula = smgr.replace(this.formula, oldString.formula, newString.formula);
+            newFormula = smgr.replace(newFormula, oldString.formula, newString.formula);
         }
-        // ToDo: A new string is created as we need a new address, should the entire object be recreated above?
-        return new StringValue(context, this.concrete, this.formula, ObjectValue.ADDRESS_UNKNOWN);
+
+        return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN);
     }
 
     /**
@@ -941,7 +949,8 @@ public BooleanFormula getBounds(boolean upper) {
      *     the Value in args is of the same type.
      * @return The resulting Value or PlaceHolder::instance
      */
-    private Value<?, ?> invokeStartsWith(Value<?, ?>[] args, Type[] desc) throws NotImplementedException, ValueConversionException {
+    private Value<?, ?> invokeStartsWith(Value<?, ?>[] args, Type[] desc)
+            throws NotImplementedException, ValueConversionException {
         if (args.length == 1) {
             return invokeStartsWith(args[0].asStringValue());
         } else if (args.length == 2) {
@@ -1053,7 +1062,8 @@ public BooleanFormula getBounds(boolean upper) {
      *     the Value in args is of the same type.
      * @return The resulting Value or PlaceHolder::instance
      */
-    private Value<?, ?> invokeSubstring(Value<?, ?>[] args, Type[] desc) throws NotImplementedException, ValueConversionException {
+    private Value<?, ?> invokeSubstring(Value<?, ?>[] args, Type[] desc)
+            throws NotImplementedException, ValueConversionException {
         if (args.length == 1) {
             return invokeSubstring(args[0].asIntValue());
         } else if (args.length == 2) {
@@ -1091,14 +1101,14 @@ public BooleanFormula getBounds(boolean upper) {
      *     the Value in args is of the same type.
      * @return The resulting Value or PlaceHolder::instance
      */
-    private Value<?, ?> invokeToCharArray(Value<?, ?>[] args, Type[] desc) throws NotImplementedException, ValueConversionException {
+    private Value<?, ?> invokeToCharArray(Value<?, ?>[] args, Type[] desc)
+            throws NotImplementedException, ValueConversionException {
 
         if (!concrete.isEmpty()) {
-            CharArrayValue dst =
-                    new CharArrayValue(context, new IntValue(context, concrete.length()), -1);
+            CharArrayValue dst = new CharArrayValue(context, new IntValue(context, concrete.length()), -1);
             for (int idx = 0; idx < concrete.length(); idx++) {
-                Value<?, ?>[] charAtArgs = new Value[] {new IntValue(context, idx)};
-                Type[] charAtDesc = new Type[] {Type.INT_TYPE};
+                Value<?, ?>[] charAtArgs = new Value[] { new IntValue(context, idx) };
+                Type[] charAtDesc = new Type[] { Type.INT_TYPE };
                 dst.storeElement(
                         new IntValue(context, idx),
                         (CharValue) invokeCharAt(charAtArgs, charAtDesc));
@@ -1232,7 +1242,7 @@ public ImmutableSet<String> getSymbolicVariables() {
     }
 
     @Override
-    public String getSymPrefix(){
+    public String getSymPrefix() {
         return symbolicPrefix;
     }
 
@@ -1242,11 +1252,10 @@ public String toString() {
         String concreteString = null != concrete ? concrete : "";
 
         if (formulaString.length() > Config.instance().getLoggingFormulaLength()) {
-            formulaString =
-                    formulaString.substring(0, Config.instance().getLoggingFormulaLength()) + "...";
+            formulaString = formulaString.substring(0, Config.instance().getLoggingFormulaLength()) + "...";
         }
 
-        return "StringValue[" + this.internalID +"]; @"
+        return "StringValue[" + this.internalID + "]; @"
                 + Integer.toHexString(address)
                 + " ("
                 + concreteString
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java
index 25fb19f..38c571d 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java
@@ -8,7 +8,6 @@
 import de.uzl.its.swat.common.exceptions.ThreadAlreadyDisabledException;
 import de.uzl.its.swat.common.exceptions.ThreadAlreadyEnabledException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.common.logging.records.InvocationEntry;
 import de.uzl.its.swat.common.logging.LoggerUtils;
 import de.uzl.its.swat.common.logging.StatsStorage;
@@ -23,9 +22,6 @@
 import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
 import de.uzl.its.swat.symbolic.value.PlaceHolder;
 import de.uzl.its.swat.symbolic.value.Value;
-import java.io.FileNotFoundException;
-import java.io.FileOutputStream;
-import java.io.PrintStream;
 import java.util.HashMap;
 import java.util.concurrent.TimeUnit;
 
@@ -53,7 +49,6 @@ public class ThreadContext {
     @Getter @Setter private Instruction current;
     @Getter @Setter private Long instCnt = 0L;
     @Getter private Instruction next;
-    @Getter private PrintStream statsStream;
     @Getter private boolean disabled;
     @Getter private boolean aborted;
     Config config = Config.instance();
@@ -136,17 +131,6 @@ public ThreadContext(long id, String endpointName, int endpointID) throws Invali
 
 
         this.coverageTraceHandler = new CoverageTraceHandler();
-
-        try {
-
-            this.statsStream =
-                    new PrintStream(
-                            new FileOutputStream(
-                                    config.getLoggingDirectory() + "/stats_" + id + ".json",
-                                    true));
-        } catch (FileNotFoundException e) {
-            this.statsStream = System.out;
-        }
     }
 
     void checkAbortTimerExpiration() {
@@ -236,6 +220,10 @@ public void recordMissingInvocation(InvocationEntry entry) {
         statsStorage.getInvocations().merge(entry, 1, Integer::sum);
     }
 
+    public void recordContextLossInvocation(InvocationEntry entry) {
+        statsStorage.recordContextLossInvocation(entry);
+    }
+
 
     public long getNextSubUid(String symbolicVar) {
         long next = SubUid.getOrDefault(symbolicVar, 0L);
@@ -244,13 +232,4 @@ public long getNextSubUid(String symbolicVar) {
         return next;
     }
 
-    /**
-     * Records an exception that occurred during the execution of the symbolic execution. This includes swallowed
-     * assertions.
-     *
-     * @param record The error record
-     */
-    public void recordException(ErrorRecord record) {
-        statsStorage.getErrors().add(record);
-    }
 }
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 1aab04e..2ecdbac 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
@@ -4,7 +4,6 @@
 import com.fasterxml.jackson.core.JsonProcessingException;
 import de.uzl.its.swat.common.exceptions.*;
 import de.uzl.its.swat.common.logging.GlobalLogger;
-import de.uzl.its.swat.common.logging.records.ErrorRecord;
 import de.uzl.its.swat.common.logging.records.InvocationEntry;
 import de.uzl.its.swat.config.Config;
 import de.uzl.its.swat.coverage.CoverageRequest;
@@ -18,7 +17,6 @@
 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.io.PrintStream;
 import java.util.HashMap;
 import java.util.concurrent.ThreadLocalRandom;
 import java.util.logging.LogRecord;
@@ -139,6 +137,15 @@ public static UFHandler getUFHandler(long id) throws NoThreadContextException {
         }
     }
 
+    public static de.uzl.its.swat.common.logging.StatsStorage getStatsStorage(long id) throws NoThreadContextException {
+        ThreadContext context = threadContextHashMap.get(id);
+        if (context != null) {
+            return context.getStatsStorage();
+        } else {
+            throw new NoThreadContextException(id);
+        }
+    }
+
     public static void sendData(long id) throws NoThreadContextException, JsonProcessingException, NotImplementedException {
         ThreadContext context = threadContextHashMap.get(id);
         if (context != null) {
@@ -156,7 +163,7 @@ public static void sendData(long id) throws NoThreadContextException, JsonProces
             }
             if(!config.isCoverageOnly()) {
                 ConstraintRequest.sendConstraints(
-                        symbolicStateHandler.getTraceDTO(), endpointID, traceID);
+                        symbolicStateHandler.getTraceDTO(context.getStatsStorage()), endpointID, traceID);
             }
 
         } else {
@@ -273,25 +280,12 @@ public static void recordMissingInvocation(
         }
     }
 
-    public static void recordException(long id, ErrorRecord er) throws NoThreadContextException  {
-        ThreadContext context = threadContextHashMap.get(id);
-        if (context != null) {
-            context.recordException(er);
-        } else {
-            throw new NoThreadContextException(id);
-        }
-    }
-
-    public static void logStats(long id) throws NoThreadContextException  {
+    public static void recordContextLossInvocation(
+            long id, InvocationEntry entry) throws NoThreadContextException  {
         if (!config.isLoggingStats()) return;
         ThreadContext context = threadContextHashMap.get(id);
         if (context != null) {
-            PrintStream ps = context.getStatsStream();
-            try {
-                ps.println(context.getStatsStorage().convertToJson());
-            } catch (JsonProcessingException e) {
-                logger.warn("Error logging missing invocation context.");
-            }
+            context.recordContextLossInvocation(entry);
         } else {
             throw new NoThreadContextException(id);
         }
diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy
index d170c2f..b31c470 100644
--- a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy
+++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/lang/StringValueTest.groovy
@@ -8,7 +8,7 @@ import org.objectweb.asm.Type
 import org.sosy_lab.java_smt.api.*
 import spock.lang.Specification
 import spock.lang.Unroll
-
+import spock.lang.Tag
 
 import static java.lang.Thread.currentThread
 
@@ -157,6 +157,7 @@ class StringValueTest extends Specification {
         "Case"   | "case"   | true
     }
 
+    @Tag("slow")
     @Unroll
     def "equalsIgnoreCase(String anotherString) - Two symbolic strings" (String s1, String s2, boolean expected) {
         setup:
diff --git a/symbolic-explorer/constraint/ConstraintController.py b/symbolic-explorer/constraint/ConstraintController.py
index afe20f7..7b205a0 100755
--- a/symbolic-explorer/constraint/ConstraintController.py
+++ b/symbolic-explorer/constraint/ConstraintController.py
@@ -38,6 +38,7 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str
         trace = request.trace
         inputs = request.inputs
         ufs = request.ufs
+        missingInvocations = request.missingInvocations
         symbolicContextLoss = request.symbolicContextLoss
         symbolicPrecisionLoss = request.symbolicPrecisionLoss
         referenceSemanticChange = request.referenceSemanticChange
@@ -49,6 +50,7 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str
             'trace': trace,
             'inputs': inputs,
             'ufs': ufs,
+            'missing_invocations': missingInvocations,
             'symbolic_context_loss': symbolicContextLoss,
             'symbolic_precision_loss': symbolicPrecisionLoss,
             'reference_semantic_change': referenceSemanticChange})
diff --git a/symbolic-explorer/constraint/ConstraintService.py b/symbolic-explorer/constraint/ConstraintService.py
index 89831e6..14cee24 100755
--- a/symbolic-explorer/constraint/ConstraintService.py
+++ b/symbolic-explorer/constraint/ConstraintService.py
@@ -4,7 +4,7 @@
 from data.trace.Input import Input
 from data.trace.UF import UF
 
-from parse.DataTransferObjects import TraceItem, InputItem, UFItem
+from parse.DataTransferObjects import TraceItem, InputItem, UFItem, InvocationItem
 from data.trace.Special import Special
 from data.trace.Branch import Branch
 
@@ -23,7 +23,8 @@ class ConstraintService:
     @staticmethod
     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):
+                        reference_semantic_change: bool = False,
+                        missing_invocations: List[InvocationItem] = None):
         """
         Adds constraints to the database.
 
@@ -40,6 +41,7 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp
         symbolic_context_loss (bool): A flag indicating whether the symbolic context was lost.
         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.
 
         Returns:
         None: The result is the side effect of adding data to the database.
@@ -50,6 +52,9 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp
         # logger.info(f'[CONSTRAINT SERVICE] Parsed trace: {[t.__str__() for t in trace_parsed]}')
         inputs_parsed: List[Input] = Parser.parse_inputs(inputs)
         ufs_parsed: List[UF] = Parser.parse_ufs(ufs)
+        # 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 [])]
         # 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)
+        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)
         logger.info(f'[CONSTRAINT SERVICE] Added trace {trace_id} to endpoint {endpoint_id}')
diff --git a/symbolic-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py
index 6636395..7544bc0 100755
--- a/symbolic-explorer/data/BinaryExecutionTree/Tree.py
+++ b/symbolic-explorer/data/BinaryExecutionTree/Tree.py
@@ -8,7 +8,7 @@
 
 import log
 logger = log.get_logger()
-#import pygraphviz as pgv
+# import pygraphviz as pgv
 
 class Tree:
     """
@@ -37,6 +37,13 @@ def __init__(self, endpoint_id: Union[str, int]):
         self.uncaught_exceptions: int = 0
         self.symbolic_vars: Set = set()
         self.ufs: Set = set()
+        # Missing invocations accumulated across all traces of this testcase, keyed by
+        # (owner, name, desc, isInstance, isSymbolic). Each value aggregates count and context_loss.
+        self.missing_invocations: dict = {}
+        # Execution errors detected in the executor's stdout (internal SWAT assertions or
+        # [SWAT Exception]s) that make the verdict untrustworthy. These cannot ride the trace
+        # because they halt the executor JVM before it sends one, so they are surfaced here.
+        self.execution_errors: list = []
 
 
     def record_inputs(self, inputs: List[Input]):
@@ -60,6 +67,52 @@ def record_ufs(self, ufs: List[UF]):
             self.ufs.add(uf.definition)
                                    
 
+    def record_missing_invocations(self, invocations: Optional[List[dict]]):
+        """
+        Accumulates missing invocations across all traces of this testcase.
+
+        Args:
+            invocations (list): Dicts with keys owner, name, desc, isInstance, isSymbolic,
+                contextLoss, count. Entries are deduped by
+                (owner, name, desc, isInstance, isSymbolic); counts are summed and contextLoss
+                is OR-ed across traces. The full set is the superset of missing invocations;
+                entries with context_loss=True form the context-loss subset.
+        """
+        if not invocations:
+            return
+        for inv in invocations:
+            key = (inv['owner'], inv['name'], inv['desc'], inv['isInstance'], inv['isSymbolic'])
+            count = int(inv.get('count', 1))
+            context_loss = bool(inv.get('contextLoss', False))
+            existing = self.missing_invocations.get(key)
+            if existing is None:
+                self.missing_invocations[key] = {
+                    'owner': inv['owner'],
+                    'name': inv['name'],
+                    'desc': inv['desc'],
+                    'isInstance': inv['isInstance'],
+                    'isSymbolic': inv['isSymbolic'],
+                    'context_loss': context_loss,
+                    'count': count,
+                }
+            else:
+                existing['count'] += count
+                existing['context_loss'] = existing['context_loss'] or context_loss
+
+    def record_execution_error(self, kind: str, message: str):
+        """
+        Records an execution error surfaced from the executor's stdout.
+
+        Deduplicated by (kind, message) so repeated exploration rounds don't inflate the list.
+
+        Args:
+            kind (str): A short category, e.g. "swat_assertion" or "swat_exception".
+            message (str): The offending output line.
+        """
+        entry = {'kind': kind, 'message': message}
+        if entry not in self.execution_errors:
+            self.execution_errors.append(entry)
+
     def record_context_loss(self):
         logger.warning("Context loss recorded!")
         self.symbolic_context_loss = True
@@ -130,8 +183,10 @@ def add_recursive(self, parent: Optional[Node], node: Optional[Union[Node, Leaf]
                 return Node(parent, trace, inputs, ufs) if len(trace) > 0 else Leaf(parent, inputs, ufs)
 
         return node
+    
+
+# VISUALIZATIONS
     def get_constraint_label(self, parent: Node, node: Union[Node, Leaf]):
-        return None
         """Get the constraint label for an edge."""
         if isinstance(node, Leaf):
             return ""
@@ -140,7 +195,6 @@ def get_constraint_label(self, parent: Node, node: Union[Node, Leaf]):
         return ""
 
     def add_to_dot(self, node: Optional[Union[Node, Leaf]], graph, parent: Optional[Node] = None):
-        return None
         """Recursively add nodes and edges to the DOT graph."""
         if node is not None:
             graph.add_node(node.gid, label=str(node.gid) + ':' + str(node.id))
@@ -153,11 +207,10 @@ def add_to_dot(self, node: Optional[Union[Node, Leaf]], graph, parent: Optional[
                 self.add_to_dot(node.branched, graph, node)
                 self.add_to_dot(node.skipped, graph, node)
 
-#    def plot_tree(self, idx):
-#        return None
-#        """Plot the tree using Graphviz and save to a file."""
-#        #log.info(self.to_string())
-#        G = pgv.AGraph(directed=True, strict=True, rankdir='TB')
-#        self.add_to_dot(self.root, G)
-#        G.layout(prog="dot")
-#        G.draw(f"tree_{idx}.png")
+    def plot_tree(self, idx):
+       """Plot the tree using Graphviz and save to a file."""
+       #log.info(self.to_string())
+       G = pgv.AGraph(directed=True, strict=True, rankdir='TB')
+       self.add_to_dot(self.root, G)
+       G.layout(prog="dot")
+       G.draw(f"tree_{idx}.png")
diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py
index e4866a8..489190b 100755
--- a/symbolic-explorer/data/Database.py
+++ b/symbolic-explorer/data/Database.py
@@ -114,7 +114,7 @@ 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):
+                  reference_semantic_change: bool = False, missing_invocations: list = None):
         endpoint_id = str(endpoint_id)
 
         lock.acquire()
@@ -124,6 +124,7 @@ def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Bra
         self.tree[endpoint_id].add(trace, inputs, ufs)
         self.tree[endpoint_id].record_inputs(inputs)
         self.tree[endpoint_id].record_ufs(ufs)
+        self.tree[endpoint_id].record_missing_invocations(missing_invocations)
         self.tree[endpoint_id].record_context_loss() if symbolic_context_loss else None
         self.tree[endpoint_id].record_precision_loss() if symbolic_precision_loss else None
         self.tree[endpoint_id].record_reference_semantic_change() if reference_semantic_change else None
@@ -155,6 +156,12 @@ def record_uncaught_exception(self, endpoint_id: Union[str, int]):
         self.tree[endpoint_id].uncaught_exceptions += 1
         lock.release()
 
+    def record_execution_error(self, endpoint_id: Union[str, int], kind: str, message: str):
+        endpoint_id = str(endpoint_id)
+        lock.acquire()
+        self.tree[endpoint_id].record_execution_error(kind, message)
+        lock.release()
+
     def add_solution(self, branch_id: int, sol: Any, inputs: List[Input], endpoint_id: Union[str, int]):
         lock.acquire()
         self.solutions[branch_id] = Solution(sol=sol, inputs=inputs, endpoint_id=endpoint_id)
diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py
index a0081e8..d3d7575 100644
--- a/symbolic-explorer/driver/SVCompDriver.py
+++ b/symbolic-explorer/driver/SVCompDriver.py
@@ -17,6 +17,7 @@
 
 from enum import Enum
 from svcomp.SymbolicStorage import SymbolicStorage
+from svcomp.TestcaseStats import write_testcase_stats
 from timing.TimingManager import TimingManager
 
 
@@ -139,8 +140,9 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac
             
             for l in output:
                 if "java.lang.AssertionError: [SWAT]" in l:
-                    # Internal assertion error in the DSE 
+                    # Internal assertion error in the DSE
                     logger.critical(f'[SVCOMP] SWAT Assertion failed: {l}')
+                    Database.instance().record_execution_error(ENDPOINT_ID, 'swat_assertion', l.strip())
                     self.state.verdict = Verdict.UNKNOWN
                     return Action.REPORTVERDICT
                 if "java.lang.AssertionError" in l and self.verification_category == VerificationCategory.VALID_ASSERT_PRP:
@@ -156,6 +158,7 @@ def determine_next_step(self, status: ExecutionStatus, output: List[str] ) -> Ac
                     Database.instance().record_uncaught_exception(ENDPOINT_ID)
                 if "[SWAT Exception]:" in l:
                     logger.info(f'[SVCOMP] SWAT Exception: {l}')
+                    Database.instance().record_execution_error(ENDPOINT_ID, 'swat_exception', l.strip())
                     self.state.verdict = Verdict.UNKNOWN
                     return Action.REPORTVERDICT
 
@@ -222,6 +225,9 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port,
             logger.info(f'[STATUS] {status}')
             next_step: Action = self.determine_next_step(status, output)
 
+            # Visualize DB tree
+            # print("Plotting DB Tree...", flush=True)
+            # Database.instance().get_tree(0).plot_tree(round_idx)
             round_idx += 1
 
             if next_step == Action.REPORTVERDICT:
@@ -258,7 +264,7 @@ def retrieve_solution(self):
                 continue
             branch_found = True
             #logger.info(f'[SYMBOLIC EXPLORATION] Solving for branch {branch.id}')
-            sat, sol = StrategyService.solve_branch(branch)
+            sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None)
              
             if sat == SATResult.SAT:
                 logger.info(f'[SYMBOLIC EXPLORATION] Found solution for branch {branch.id} {"skipped" if branch.skipped is None else "branched"}')
@@ -329,6 +335,11 @@ def run(self):
         timing_file = os.path.join(log_dir, 'timing_data.json')
         TimingManager.instance().save_to_file(Path(timing_file))
 
+        # Write the consolidated per-testcase statistics (verdict, soundness flags, missing
+        # invocations and the context-loss subset) so the analysis can rely on structured data.
+        stats_file = os.path.join(log_dir, 'stats.json')
+        write_testcase_stats(Path(stats_file), verdict, self.verification_category, Database.instance().get_tree(ENDPOINT_ID))
+
         self.kill_current_process()
         
         
diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py
index be30d85..4d46be7 100644
--- a/symbolic-explorer/parse/DataTransferObjects.py
+++ b/symbolic-explorer/parse/DataTransferObjects.py
@@ -22,10 +22,26 @@ class InputItem(BaseModel):
     upperBound: str
 
 
+class InvocationItem(BaseModel):
+    """A method invocation that could not be modelled symbolically during execution.
+
+    The full list is the superset of missing invocations; entries with ``contextLoss`` set are the
+    dangerous subset that received symbolic arguments and caused symbolic context loss.
+    """
+    owner: str
+    name: str
+    desc: str
+    isInstance: bool
+    isSymbolic: bool
+    contextLoss: bool
+    count: int
+
+
 class ConstraintRequest(BaseModel):
     trace: List[TraceItem]
     inputs: List[InputItem]
     ufs: List[UFItem]
+    missingInvocations: List[InvocationItem] = []
     symbolicContextLoss: bool
     symbolicPrecisionLoss: bool
     referenceSemanticChange: bool = False
diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py
index dd9a0ee..471f0f8 100755
--- a/symbolic-explorer/solver/SolverHandler.py
+++ b/symbolic-explorer/solver/SolverHandler.py
@@ -358,7 +358,7 @@ def write_optimizer_to_file(optimizer: Optimize, output_dir: str = "smt_files")
         return filepath
 
     @staticmethod
-    def solve(node: Any, path_constraints: list) -> Tuple[SATResult, Dict[str, Any]]:
+    def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000) -> Tuple[SATResult, Dict[str, Any]]:
         """
         Solve for the given node and path constraints using ConstraintCache (modern approach).
 
@@ -391,6 +391,8 @@ def solve(node: Any, path_constraints: list) -> Tuple[SATResult, Dict[str, Any]]
         for i, path_constraint_str in enumerate(path_constraints):
             path_cached = cache.get_smt_constraint(path_constraint_str, source=f"path_{i}")
             all_exprs.extend(path_cached['exprs'])
+        
+        # logger.debug(f"[SOLVER] all_exprs: {all_exprs}")
 
 
         # Create solver with shared context from cache
@@ -432,7 +434,8 @@ def solve(node: Any, path_constraints: list) -> Tuple[SATResult, Dict[str, Any]]
             except Exception as e:
                 logger.warning(f"[SOLVER] Failed to save SMT formula: {e}")
 
-        solver.set("timeout", 60 * 1000)
+        if timeout_ms is not None:
+            solver.set("timeout", timeout_ms)
         t_start = time.time()
         res = solver.check()
         t_check = time.time() - t_start
diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py
index 5d97d72..56f3924 100755
--- a/symbolic-explorer/strategy/StrategyService.py
+++ b/symbolic-explorer/strategy/StrategyService.py
@@ -82,7 +82,7 @@ def collect_uf_definitions(node: Node) -> list():
         return uf_definitions
 
     @staticmethod
-    def solve_branch(possible_branch: Node, endpoint_id=None):
+    def solve_branch(possible_branch: Node, endpoint_id=None, solver_timeout_ms: int | None = 60 * 1000):
         db = Database.instance()
 
         path_constraints = StrategyService.collect_path_constrains(possible_branch)
@@ -93,7 +93,7 @@ def solve_branch(possible_branch: Node, endpoint_id=None):
 
         inputs = possible_branch.inputs
 
-        sat, sol = Z3Handler.solve(possible_branch, path_constraints)
+        sat, sol = Z3Handler.solve(possible_branch, path_constraints, timeout_ms=solver_timeout_ms)
 
         if sat == SATResult.SAT:
             db.add_solution(branch_id=possible_branch.gid, sol=sol, inputs=inputs, endpoint_id=endpoint_id)
diff --git a/symbolic-explorer/svcomp/SVCompHandler.py b/symbolic-explorer/svcomp/SVCompHandler.py
index 7922fb1..a14c9ae 100755
--- a/symbolic-explorer/svcomp/SVCompHandler.py
+++ b/symbolic-explorer/svcomp/SVCompHandler.py
@@ -192,7 +192,7 @@ def retrieve_solution(self):
             if not StrategyService.is_symbolic_branch(branch):
                 continue
             branch_found = True
-            sat, sol = StrategyService.solve_branch(branch)
+            sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None)
              
             if sat == SATResult.SAT:
                 symbolic_vars = branch.inputs
diff --git a/symbolic-explorer/svcomp/TestcaseStats.py b/symbolic-explorer/svcomp/TestcaseStats.py
new file mode 100644
index 0000000..830f042
--- /dev/null
+++ b/symbolic-explorer/svcomp/TestcaseStats.py
@@ -0,0 +1,81 @@
+"""
+Consolidated per-testcase statistics for SV-COMP runs.
+
+The Symbolic Explorer owns the per-testcase output: after a testcase completes it writes a single
+``stats.json`` into the log directory containing the verdict, the soundness-relevant flags, and the
+methods that could not be modelled symbolically. This replaces the executor-written ``stats_*.json``
+files and lets the analysis rely on authoritative structured data instead of scraping logs.
+
+The missing-invocation list is the superset; entries with ``context_loss=True`` are the dangerous
+subset that received symbolic arguments and caused symbolic context loss. This makes the
+superset/subset relationship explicit (see issue #25), rather than inferring it from regexes.
+"""
+
+import json
+from pathlib import Path
+
+import log
+
+logger = log.get_logger()
+
+
+def _signature(inv: dict) -> str:
+    """Render a missing invocation as a stable ``owner/name:desc`` signature."""
+    return f"{inv['owner']}/{inv['name']}:{inv['desc']}"
+
+
+def build_testcase_stats(verdict, category, tree) -> dict:
+    """
+    Assemble the consolidated per-testcase statistics dictionary.
+
+    Args:
+        verdict: The final (post-downgrade) Verdict enum for the testcase.
+        category: The VerificationCategory enum for the property.
+        tree: The per-endpoint Tree holding accumulated metadata for the testcase.
+
+    Returns:
+        A JSON-serializable dict describing the testcase outcome.
+    """
+    # Order: context-loss culprits first, then by signature, for readable output.
+    missing = sorted(
+        tree.missing_invocations.values(),
+        key=lambda i: (not i['context_loss'], i['owner'], i['name'], i['desc']),
+    )
+    context_loss_methods = sorted({_signature(i) for i in missing if i['context_loss']})
+
+    return {
+        'property': category.value,
+        'verdict': verdict.name,
+        'verdict_raw': verdict.value,
+        'soundness': {
+            'symbolic_context_loss': tree.symbolic_context_loss,
+            'symbolic_precision_loss': tree.symbolic_precision_loss,
+            'reference_semantic_change': tree.reference_semantic_change,
+            'uncaught_exceptions': tree.uncaught_exceptions,
+        },
+        'symbolic_vars': sorted(tree.symbolic_vars),
+        'missing_invocations': missing,
+        'context_loss_methods': context_loss_methods,
+        'execution_errors': list(tree.execution_errors),
+        'counts': {
+            'missing_invocations': len(missing),
+            'context_loss_invocations': sum(1 for i in missing if i['context_loss']),
+            'execution_errors': len(tree.execution_errors),
+        },
+    }
+
+
+def write_testcase_stats(filepath: Path, verdict, category, tree):
+    """Write the consolidated per-testcase statistics to ``filepath`` as JSON."""
+    data = build_testcase_stats(verdict, category, tree)
+
+    filepath.parent.mkdir(parents=True, exist_ok=True)
+    with open(filepath, 'w') as f:
+        json.dump(data, f, indent=2)
+
+    logger.info(
+        f"[STATS] Saved testcase stats to {filepath} "
+        f"({data['counts']['missing_invocations']} missing invocations, "
+        f"{data['counts']['context_loss_invocations']} context-loss, "
+        f"{data['counts']['execution_errors']} execution errors)"
+    )
diff --git a/targets/sv-comp/scripts/README.md b/targets/sv-comp/scripts/README.md
index 5992b85..22ce37c 100644
--- a/targets/sv-comp/scripts/README.md
+++ b/targets/sv-comp/scripts/README.md
@@ -27,7 +27,7 @@ scripts/
 ├── svcomp.py           # Main CLI entry point
 ├── lib/                # Library modules (refactored from original scripts)
 │   ├── __init__.py
-│   ├── analysis.py     # (was analyse_ctx_loss.py)
+│   ├── analysis/       # context_loss.py (was analyse_ctx_loss.py) + timing/failures/performance
 │   ├── command_gen.py  # (was command_generation.py)
 │   ├── comparison.py   # (was compare_results.py)
 │   ├── dtypes.py       # (unchanged)
@@ -86,19 +86,35 @@ scripts/
 ### Analysis Commands
 
 ```bash
-# Analyze latest results for context losses
+# Analyze the latest run: scoring summary (Correct/Failed/Unk/Error/Timeout) plus
+# the missing-invocation superset and its context-loss subset, read from each
+# testcase's stats.json (no log scraping)
 ./svcomp analyze results
 
-# Analyze specific results file
-./svcomp analyze results path/to/results.json
+# Analyze a specific run directory
+./svcomp analyze results runs/run_20260101_120000
 
 # Compare two result files
-./svcomp analyze compare results/old.json results/new.json
+./svcomp analyze compare runs/run_A/results/results_valid-assert.prp_*.json \
+                         runs/run_B/results/results_valid-assert.prp_*.json
 
 # Show test case statistics
 ./svcomp analyze stats
 ```
 
+### Run output
+
+Each `./svcomp test run` writes everything for that run under one timestamped directory,
+so previous runs are preserved:
+
+```
+runs/run_<timestamp>/
+├── logs/<folder>/<testcase>_<property>/   # explorer.log, stats.json, timing_data.json, ...
+└── results/                               # results_<category>_<timestamp>.json, stage_timing.csv, histograms
+```
+
+Debug runs (a `*-debug.cfg`) are grouped per target instead: `runs-debug/<folder>/<testcase>/run_<timestamp>/logs/`.
+
 ### Utility Commands
 
 ```bash
@@ -127,17 +143,18 @@ scripts/
 
 ## Migration Notes
 
-### Old Scripts (Still Available)
+### Old Scripts (Removed)
 
-The original Python scripts are still in the `scripts/` directory and can be used directly if needed:
-- `target_selection.py`
-- `command_generation.py`
-- `target_execution.py`
-- `witness_validation.py`
-- `analyse_ctx_loss.py`
-- `compare_results.py`
+The original top-level scripts have been removed; their functionality lives in `lib/` and is driven through the `./svcomp` CLI:
+- `target_selection.py` → `lib/selection.py`
+- `command_generation.py` → `lib/command_gen.py`
+- `target_execution.py` → `lib/execution.py`
+- `witness_validation.py` → `lib/witness.py`
+- `analyse_ctx_loss.py` → `lib/analysis/context_loss.py`
+- `compare_results.py` → `lib/comparison.py`
+- `util.py` → `lib/utils.py`, `dtypes.py` → `lib/dtypes.py`
 
-However, **it's recommended to use the new CLI** for better user experience.
+`run_locally.sh` and `ci_run.sh` now invoke `./svcomp test run`.
 
 ### Key Changes
 
@@ -147,11 +164,9 @@ However, **it's recommended to use the new CLI** for better user experience.
 4. **Relative Imports**: Library modules use relative imports for better packaging
 5. **Wrapper Script**: `svcomp` wrapper automatically uses the venv Python
 
-### Backwards Compatibility
+### Programmatic Use
 
-- Old scripts still work as before
-- Library functions are exposed through `lib/__init__.py`
-- Can import and use functions programmatically:
+- Library functions are exposed through `lib/__init__.py`:
   ```python
   from lib import extract_testcases, generate_commands, run_parallel
   ```
@@ -171,10 +186,10 @@ However, **it's recommended to use the new CLI** for better user experience.
 - [ ] Improve error messages and validation
 - [ ] Add shell completion support
 
-**Phase 3: 🔜 Future**
-- [ ] Add deprecation warnings to old scripts
-- [ ] Update documentation
-- [ ] Consider removing old scripts
+**Phase 3: ✅ Complete**
+- ✅ Removed the legacy top-level scripts (consolidated into `lib/`)
+- ✅ `run_locally.sh` / `ci_run.sh` use the `./svcomp` CLI
+- ✅ `runs/run_<timestamp>/{logs,results}` output layout; analysis reads per-testcase `stats.json`
 
 ## Examples
 
@@ -190,11 +205,8 @@ However, **it's recommended to use the new CLI** for better user experience.
 # Run tests for specific category
 ./svcomp test run --categories valid-assert.prp --workers 30
 
-# Analyze results
+# Analyze the latest run
 ./svcomp analyze results
-
-# Compare with previous run
-./svcomp analyze compare results/old.json results/new.json
 ```
 
 ### Development Workflow
diff --git a/targets/sv-comp/scripts/analyse_ctx_loss.py b/targets/sv-comp/scripts/analyse_ctx_loss.py
deleted file mode 100644
index f8019d6..0000000
--- a/targets/sv-comp/scripts/analyse_ctx_loss.py
+++ /dev/null
@@ -1,399 +0,0 @@
-#!/usr/bin/env python3
-"""
-Analyze SV-Comp results to identify context loss methods that need implementation.
-Run this script in the directory containing the results JSON file.
-
-Usage: python3 analyse_ctx_loss.py results_valid-assert.prp_XXXXXX.json
-"""
-
-import json
-import sys
-import re
-from collections import defaultdict
-from pathlib import Path
-
-
-def extract_context_loss_methods(log_content: str) -> list[str]:
-    """Extract all method names causing context loss from log content."""
-    methods = set()  # Use set to dedupe
-    if not log_content:
-        return list(methods)
-
-    # Look for "Context loss:" pattern
-    for match in re.finditer(r'Context loss:\s*(.+?)(?:\n|$)', log_content):
-        methods.add(match.group(1).strip())
-
-    # Also look for "Uninstrumented invocation" pattern
-    for match in re.finditer(r'Uninstrumented invocation.*?:\s*(.+?)(?:\n|$)', log_content):
-        methods.add(match.group(1).strip())
-
-    # Look for "Context loss recorded" with method info on previous lines
-    for match in re.finditer(r'(\S+\.\S+)\s*\n.*Context loss recorded', log_content):
-        methods.add(match.group(1).strip())
-
-    return list(methods)
-
-
-def extract_missing_invocations(log_content: str) -> list[str]:
-    """Extract missing/unimplemented method invocations from log content."""
-    methods = set()  # Use set to dedupe
-    if not log_content:
-        return list(methods)
-
-    # Pattern: "Error visiting Instruction INVOKE* owner/class/method:desc"
-    # Example: "Error visiting Instruction INVOKEVIRTUAL java/lang/Double/byteValue:()B"
-    for match in re.finditer(
-        r'Error visiting Instruction (INVOKE\w+)\s+(\S+?)(?:\s*\(|$)',
-        log_content
-    ):
-        invoke_type = match.group(1)
-        method_sig = match.group(2)
-        # Clean up the method signature (remove id info if present)
-        method_sig = re.sub(r'\s*\(id:.*', '', method_sig)
-        methods.add(f"{invoke_type} {method_sig}")
-
-    # Pattern: "Not implemented: <method> in <class>"
-    for match in re.finditer(r'Not implemented:\s*(.+?)\s+in\s+(\S+)', log_content):
-        method = match.group(1).strip()
-        cls = match.group(2).strip()
-        methods.add(f"NOT_IMPLEMENTED {cls}/{method}")
-
-    return list(methods)
-
-
-def extract_symbolic_invocations_from_stats(stats_path: Path) -> list[str]:
-    """
-    Extract symbolic method invocations from stats JSON files.
-
-    Stats files contain entries like:
-    {"owner":"java/lang/Character","isSymbolic":true,"name":"isUnicodeIdentifierStart","desc":"(I)Z"}
-
-    Returns list of method signatures that have isSymbolic=true (missing implementations).
-    """
-    methods = set()
-
-    # Check both stats_1.json and stats_-1.json
-    for stats_file in ['stats_1.json', 'stats_-1.json']:
-        file_path = stats_path / stats_file
-        if not file_path.exists():
-            continue
-
-        try:
-            with open(file_path) as f:
-                data = json.load(f)
-
-            if isinstance(data, list):
-                for entry in data:
-                    if isinstance(entry, dict) and entry.get('isSymbolic', False):
-                        owner = entry.get('owner', '')
-                        name = entry.get('name', '')
-                        desc = entry.get('desc', '')
-                        is_instance = entry.get('isInstance', False)
-                        invoke_type = 'INVOKEVIRTUAL' if is_instance else 'INVOKESTATIC'
-                        if owner and name:
-                            methods.add(f"{invoke_type} {owner}/{name}:{desc}")
-        except (json.JSONDecodeError, IOError):
-            pass
-
-    return list(methods)
-
-
-def extract_errors(log_content: str) -> list[str]:
-    """Extract error messages from log content."""
-    errors = []
-    if not log_content:
-        return errors
-
-    # Look for SWAT Exception patterns
-    for match in re.finditer(r'\[SWAT Exception\]:\s*(.+?)(?:\n|$)', log_content):
-        errors.append(match.group(1).strip())
-
-    # Look for general exceptions
-    for match in re.finditer(r'Exception.*?:\s*(.+?)(?:\n|$)', log_content):
-        msg = match.group(1).strip()
-        if msg and len(msg) < 200:
-            errors.append(msg)
-
-    return errors
-
-
-def get_log_dir(logs_dir: Path, task_name: str, property_name: str) -> Path:
-    """
-    Construct the path to the log directory for a given task.
-
-    Task name format: folder/testname (e.g., "objects/objects03")
-    Log dir format: logs/<folder>/<testname>_<property>/
-    """
-    parts = task_name.split('/')
-    if len(parts) >= 2:
-        folder = parts[0]
-        testname = parts[1]
-    else:
-        folder = ""
-        testname = parts[0]
-
-    # Property name like "valid-assert.prp" -> "valid-assert"
-    prop_short = property_name.replace('.prp', '')
-
-    return logs_dir / folder / f"{testname}_{prop_short}"
-
-
-def get_log_path(logs_dir: Path, task_name: str, property_name: str) -> Path:
-    """
-    Construct the path to the explorer.log for a given task.
-    """
-    return get_log_dir(logs_dir, task_name, property_name) / "explorer.log"
-
-
-def get_stats_dir(logs_dir: Path, task_name: str, property_name: str) -> Path:
-    """
-    Construct the path to the stats directory (logs/ subdirectory) for a given task.
-    """
-    return get_log_dir(logs_dir, task_name, property_name) / "logs"
-
-
-def read_log_file(log_path: Path) -> str:
-    """Read log file content, return empty string if not found."""
-    try:
-        if log_path.exists():
-            return log_path.read_text(errors='replace')
-    except Exception:
-        pass
-    return ""
-
-
-def main():
-    if len(sys.argv) < 2:
-        # Find the latest results file
-        results_dir = Path('.')
-        json_files = list(results_dir.glob('results_*.json'))
-        if not json_files:
-            json_files = list(Path('results').glob('results_*.json'))
-        if not json_files:
-            print("Usage: python3 analyse_ctx_loss.py <results_file.json>")
-            print("No results files found in current directory")
-            sys.exit(1)
-        results_file = max(json_files, key=lambda p: p.stat().st_mtime)
-        print(f"Using latest results file: {results_file}")
-    else:
-        results_file = Path(sys.argv[1])
-
-    # Determine logs directory (sibling to results file or parent's logs/)
-    if results_file.parent.name == 'results':
-        logs_dir = results_file.parent.parent / 'logs'
-    else:
-        logs_dir = results_file.parent / 'logs'
-
-    print(f"Looking for logs in: {logs_dir}")
-
-    with open(results_file) as f:
-        data = json.load(f)
-
-    results = data['results']
-    category = data.get('category', 'valid-assert.prp')
-
-    # Analyze all 0-point tasks
-    zero_points_by_folder = defaultdict(list)
-    context_loss_methods = defaultdict(list)
-    missing_invocations = defaultdict(list)
-    all_errors = defaultdict(list)
-
-    for name, task in results.items():
-        # task format: [status_change, points, execution_status, error_bool, validated, time]
-        points = task[1]
-        if points == 0:
-            folder = name.split('/')[0]
-            status = task[0]
-            exec_status = task[2]
-
-            # Read the actual log file from disk
-            log_path = get_log_path(logs_dir, name, category)
-            log_content = read_log_file(log_path)
-
-            # Get stats directory for symbolic invocations
-            stats_dir = get_stats_dir(logs_dir, name, category)
-
-            zero_points_by_folder[folder].append({
-                'name': name,
-                'status': status,
-                'exec_status': exec_status,
-                'log_path': str(log_path),
-                'log_content': log_content,
-                'log_exists': log_path.exists(),
-                'stats_dir': str(stats_dir)
-            })
-
-            # Extract context loss methods
-            methods = extract_context_loss_methods(log_content)
-            for method in methods:
-                context_loss_methods[method].append(name)
-
-            # Extract missing invocations from error logs
-            invocations = extract_missing_invocations(log_content)
-            for inv in invocations:
-                missing_invocations[inv].append(name)
-
-            # Extract symbolic invocations from stats JSON files
-            symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir)
-            for inv in symbolic_invocations:
-                missing_invocations[inv].append(name)
-
-            # Extract errors
-            errors = extract_errors(log_content)
-            for error in errors:
-                all_errors[error].append(name)
-
-    # Print summary by folder
-    print("\n" + "=" * 80)
-    print("TASKS WITH 0 POINTS BY FOLDER")
-    print("=" * 80)
-    total_zero = 0
-    logs_found = 0
-    for folder, tasks in sorted(zero_points_by_folder.items(), key=lambda x: -len(x[1])):
-        folder_logs_found = sum(1 for t in tasks if t['log_exists'])
-        print(f"{folder}: {len(tasks)} tasks ({folder_logs_found} logs found)")
-        total_zero += len(tasks)
-        logs_found += folder_logs_found
-    print(f"\nTotal: {total_zero} tasks with 0 points ({logs_found} logs found)")
-
-    # Print context loss methods sorted by frequency
-    print("\n" + "=" * 80)
-    print("CONTEXT LOSS METHODS (sorted by frequency)")
-    print("=" * 80)
-
-    if not context_loss_methods:
-        print("No context loss methods found in logs.")
-    else:
-        for method, tasks in sorted(context_loss_methods.items(), key=lambda x: -len(x[1])):
-            print(f"\n{len(tasks):3d} tasks - {method}")
-            print(f"    Examples: {', '.join(tasks[:3])}")
-
-    # Print missing invocations sorted by frequency
-    print("\n" + "=" * 80)
-    print("MISSING/UNIMPLEMENTED INVOCATIONS (sorted by frequency)")
-    print("=" * 80)
-
-    if not missing_invocations:
-        print("No missing invocations found in logs.")
-    else:
-        for inv, tasks in sorted(missing_invocations.items(), key=lambda x: -len(x[1])):
-            # Dedupe task list (same task may appear multiple times)
-            unique_tasks = list(dict.fromkeys(tasks))
-            print(f"\n{len(unique_tasks):3d} tasks - {inv}")
-            print(f"    Examples: {', '.join(unique_tasks[:3])}")
-
-    # Print errors sorted by frequency
-    print("\n" + "=" * 80)
-    print("ERRORS (sorted by frequency)")
-    print("=" * 80)
-
-    if not all_errors:
-        print("No specific errors found in logs.")
-    else:
-        for error, tasks in sorted(all_errors.items(), key=lambda x: -len(x[1]))[:20]:
-            print(f"\n{len(tasks):3d} tasks - {error[:100]}")
-            print(f"    Examples: {', '.join(tasks[:3])}")
-
-    # Detailed breakdown for each folder
-    print("\n" + "=" * 80)
-    print("DETAILED BREAKDOWN BY FOLDER")
-    print("=" * 80)
-
-    for folder in ['autostub', 'jbmc-regression', 'java-ranger-regression', 'algorithms', 'argv-tasks', 'float-nonlinear-calculation', 'securibench', 'objects']:
-        if folder not in zero_points_by_folder:
-            continue
-
-        print(f"\n--- {folder} ({len(zero_points_by_folder[folder])} tasks) ---")
-
-        folder_context_loss = defaultdict(list)
-        folder_missing_invocations = defaultdict(list)
-        folder_errors = defaultdict(list)
-        other_issues = defaultdict(list)
-        tasks_with_missing_invocations = set()
-
-        for task in zero_points_by_folder[folder]:
-            log_content = task['log_content']
-            stats_dir = Path(task['stats_dir'])
-            methods = extract_context_loss_methods(log_content)
-            invocations = extract_missing_invocations(log_content)
-            symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir)
-            errors = extract_errors(log_content)
-
-            if methods:
-                for method in methods:
-                    folder_context_loss[method].append(task['name'])
-
-            all_invocations = invocations + symbolic_invocations
-            if all_invocations:
-                tasks_with_missing_invocations.add(task['name'])
-                for inv in all_invocations:
-                    folder_missing_invocations[inv].append(task['name'])
-
-            # Always categorize by verdict/status (not just when no missing invocations)
-            if errors:
-                for error in errors:
-                    folder_errors[error[:80]].append(task['name'])
-
-            if 'timeout' in task['exec_status'].lower():
-                other_issues['timeout'].append(task['name'])
-            elif not task['log_exists']:
-                other_issues['log file not found'].append(task['name'])
-            elif not log_content.strip():
-                other_issues['log file empty'].append(task['name'])
-            elif 'DONT-KNOW' in log_content:
-                other_issues['verdict: DONT-KNOW'].append(task['name'])
-            elif 'NoThreadContextException' in log_content:
-                other_issues['NoThreadContextException'].append(task['name'])
-            elif not methods and not all_invocations:
-                other_issues['unknown (check log)'].append(task['name'])
-
-        if folder_context_loss:
-            print("  Context loss methods:")
-            for method, tasks in sorted(folder_context_loss.items(), key=lambda x: -len(x[1]))[:10]:
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {method[:80]}")
-
-        if folder_missing_invocations:
-            print(f"  Missing invocations ({len(tasks_with_missing_invocations)} unique tasks):")
-            for inv, tasks in sorted(folder_missing_invocations.items(), key=lambda x: -len(x[1]))[:10]:
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {inv[:80]}")
-
-        if folder_errors:
-            print("  Errors:")
-            for error, tasks in sorted(folder_errors.items(), key=lambda x: -len(x[1]))[:10]:
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {error[:80]}")
-
-        if other_issues:
-            print("  Other issues:")
-            for issue, tasks in sorted(other_issues.items(), key=lambda x: -len(x[1])):
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {issue[:80]}")
-
-    # Print sample logs for debugging
-    print("\n" + "=" * 80)
-    print("SAMPLE LOGS (first 5 tasks with 0 points)")
-    print("=" * 80)
-
-    count = 0
-    for name, task in results.items():
-        if task[1] == 0 and count < 5:
-            log_path = get_log_path(logs_dir, name, category)
-            log_content = read_log_file(log_path)
-
-            print(f"\n{name}:")
-            print(f"  Status: {task[0]}")
-            print(f"  Exec status: {task[2]}")
-            print(f"  Log path: {log_path}")
-            print(f"  Log exists: {log_path.exists()}")
-            if log_content:
-                # Show last 500 chars which usually has the verdict
-                print(f"  Log tail: ...{log_content[-500:]}")
-            else:
-                print(f"  Log: (empty or not found)")
-            count += 1
-
-
-if __name__ == '__main__':
-    main()
diff --git a/targets/sv-comp/scripts/analyze_by_correctness.py b/targets/sv-comp/scripts/analyze_by_correctness.py
deleted file mode 100644
index feaa4df..0000000
--- a/targets/sv-comp/scripts/analyze_by_correctness.py
+++ /dev/null
@@ -1,211 +0,0 @@
-#!/usr/bin/env python3
-"""
-Analyze timing data grouped by verdict correctness.
-"""
-import json
-from pathlib import Path
-import statistics
-
-# Find most recent results file
-results_dir = Path(__file__).resolve().parent.parent / 'results'
-results_files = sorted(results_dir.glob('*.json'), key=lambda p: p.stat().st_mtime, reverse=True)
-
-if not results_files:
-    print("No results files found!")
-    exit(1)
-
-results_file = results_files[0]
-print(f"Loading: {results_file.name}")
-print(f"Note: Filtering out testcases with solver_count == 0")
-
-# Extract property from results filename (e.g., "valid-assert" from "results_valid-assert.prp_...")
-results_filename = results_file.name
-property_suffix = None
-if results_filename.startswith("results_") and ".prp_" in results_filename:
-    property_part = results_filename[len("results_"):results_filename.index(".prp_")]
-    property_suffix = "_" + property_part
-    print(f"Detected property suffix: {property_suffix}")
-
-# Debug: count how many we skip
-skipped_count = 0
-processed_count = 0
-
-# Load results
-with open(results_file) as f:
-    results = json.load(f)
-
-# Load timing data
-log_dir = Path(__file__).resolve().parent.parent / 'logs'
-timing_files = {tf.parent.name: tf for tf in log_dir.rglob('timing_data.json')}
-
-# Group testcases by different categories
-correct = []           # All correct: expected == actual (TP + TN)
-true_correct = []      # True Positives: violation -> violation
-true_negative = []     # True Negatives: safe -> safe
-false_results = []     # False Positives + False Negatives: expected != actual (excluding unknown/crash)
-incorrect = []         # All incorrect: expected != actual (including unknown/crash)
-
-# Parse results structure: results[testcase_name] = [case_occurrence, points, status, dse_error, witness, elapsed, timing]
-for testcase_name, result_data in results.get('results', {}).items():
-    if not isinstance(result_data, list) or len(result_data) < 7:
-        continue
-
-    case_occurrence = result_data[0]  # e.g., "safe -> unknown" or "violation -> violation"
-    timing_breakdown = result_data[6]  # Dict with timing data
-
-    # Parse expected -> actual from case_occurrence
-    parts = case_occurrence.split(' -> ')
-    if len(parts) != 2:
-        continue
-    expected, actual = parts
-
-    # Get timing data
-    try:
-        # Convert testcase name to directory name
-        # e.g., 'objects/objects08' -> 'objects08_valid-assert'
-        if '/' in testcase_name:
-            # Remove category prefix (everything before and including '/')
-            testcase_short = testcase_name.split('/')[-1]
-        else:
-            testcase_short = testcase_name
-
-        # Add property suffix if detected
-        if property_suffix:
-            testcase_dir = testcase_short + property_suffix
-        else:
-            testcase_dir = testcase_short
-
-        # Check if timing file exists to get solver_count
-        timing_file = timing_files.get(testcase_dir)
-        if timing_file:
-            with open(timing_file) as f:
-                timing_data_full = json.load(f)
-                solver_count = timing_data_full.get('statistics', {}).get('solver_count', 0)
-                # Skip testcases with zero solver calls
-                if solver_count == 0:
-                    skipped_count += 1
-                    continue
-                else:
-                    processed_count += 1
-        else:
-            # No timing file found, skip this testcase
-            skipped_count += 1
-            continue
-
-        total_time = timing_breakdown.get('total_time', 0)
-        executor = timing_breakdown.get('symbolic_executor', 0)
-        solver = timing_breakdown.get('smt_solver', 0)
-        witness_gen = timing_breakdown.get('witness_generation', 0)
-        witness_val = timing_breakdown.get('witness_validation', 0)
-
-        # Compute corrected explorer time as residual
-        corrected_explorer = max(0.0, total_time - executor - solver - witness_gen - witness_val)
-
-        timing_entry = {
-            'name': testcase_name,
-            'total': total_time,
-            'executor': executor,
-            'solver': solver,
-            'explorer': corrected_explorer,
-            'witness_gen': witness_gen,
-            'witness_val': witness_val,
-            'expected': expected,
-            'actual': actual,
-            'case': case_occurrence
-        }
-
-        # Categorize into groups
-        is_correct = (expected == actual)
-
-        if is_correct:
-            correct.append(timing_entry)
-            if actual == 'violation':  # True Positive
-                true_correct.append(timing_entry)
-            elif actual == 'safe':  # True Negative
-                true_negative.append(timing_entry)
-
-        if not is_correct:
-            incorrect.append(timing_entry)
-            # False results = incorrect but not unknown/crash
-            if actual not in ['unknown', 'crash']:
-                false_results.append(timing_entry)
-
-    except Exception as e:
-        print(f"Error processing {testcase_name}: {e}")
-
-print(f"\n{'='*70}")
-print(f"FILTERING RESULTS")
-print(f"{'='*70}")
-print(f"Skipped (no timing file or solver_count=0): {skipped_count}")
-print(f"Processed (solver_count > 0):               {processed_count}")
-
-print(f"\n{'='*70}")
-print(f"RESULTS SUMMARY")
-print(f"{'='*70}")
-print(f"Correct (expected == actual):          {len(correct):>4} testcases")
-print(f"  - True Correct (violation->violation): {len(true_correct):>4} testcases")
-print(f"  - True Negative (safe->safe):          {len(correct)-len(true_correct):>4} testcases")
-print(f"Incorrect (expected != actual):        {len(incorrect):>4} testcases")
-print(f"  - False Results (not unknown/crash):   {len(false_results):>4} testcases")
-print(f"  - Unknown/Crash:                       {len(incorrect)-len(false_results):>4} testcases")
-print(f"Total:                                 {len(correct) + len(incorrect):>4} testcases")
-
-def compute_stats(group, group_name):
-    if not group:
-        print(f"\n{group_name}: No data")
-        return
-
-    print(f"\n{'='*70}")
-    print(f"{group_name} ({len(group)} testcases)")
-    print(f"{'='*70}")
-
-    # Compute mean
-    mean_stats = {
-        'executor': statistics.mean(t['executor'] for t in group),
-        'solver': statistics.mean(t['solver'] for t in group),
-        'explorer': statistics.mean(t['explorer'] for t in group),
-        'witness_gen': statistics.mean(t['witness_gen'] for t in group),
-        'witness_val': statistics.mean(t['witness_val'] for t in group),
-    }
-    mean_total = sum(mean_stats.values())
-
-    print("\nMEAN:")
-    for key, val in mean_stats.items():
-        pct = (val / mean_total * 100) if mean_total > 0 else 0
-        print(f"  {key:<20} {val:>8.2f}s ({pct:>5.1f}%)")
-    print(f"  {'Total':<20} {mean_total:>8.2f}s")
-
-    # Compute median
-    median_stats = {
-        'executor': statistics.median(t['executor'] for t in group),
-        'solver': statistics.median(t['solver'] for t in group),
-        'explorer': statistics.median(t['explorer'] for t in group),
-        'witness_gen': statistics.median(t['witness_gen'] for t in group),
-        'witness_val': statistics.median(t['witness_val'] for t in group),
-    }
-    median_total = sum(median_stats.values())
-
-    print("\nMEDIAN:")
-    for key, val in median_stats.items():
-        pct = (val / median_total * 100) if median_total > 0 else 0
-        print(f"  {key:<20} {val:>8.2f}s ({pct:>5.1f}%)")
-    print(f"  {'Total':<20} {median_total:>8.2f}s")
-
-    # Show distribution for solver (all should have solver_count > 0 due to filtering)
-    solver_times = [t['solver'] for t in group]
-    zero_time = sum(1 for s in solver_times if s == 0.0)
-    print(f"\nSolver time distribution (all have solver_count > 0):")
-    print(f"  Zero solver TIME:     {zero_time:>4} ({zero_time/len(group)*100:>5.1f}%)")
-    print(f"  Non-zero solver TIME: {len(group)-zero_time:>4} ({(len(group)-zero_time)/len(group)*100:>5.1f}%)")
-
-    # Show some examples
-    print(f"\nFirst 5 examples:")
-    for i, t in enumerate(group[:5], 1):
-        print(f"  {i}. {t['name']}: {t['expected']} -> {t['actual']}")
-        print(f"     Executor: {t['executor']:.2f}s, Solver: {t['solver']:.2f}s, Explorer: {t['explorer']:.2f}s")
-
-compute_stats(correct, "CORRECT (All expected == actual)")
-compute_stats(true_correct, "TRUE POSITIVE (violation -> violation)")
-compute_stats(true_negative, "TRUE NEGATIVE (safe -> safe)")
-compute_stats(false_results, "FALSE RESULTS (FP + FN, excluding unknown/crash)")
-compute_stats(incorrect, "INCORRECT (All expected != actual)")
diff --git a/targets/sv-comp/scripts/ci_run.sh b/targets/sv-comp/scripts/ci_run.sh
index 3cc3fd2..8b07f37 100755
--- a/targets/sv-comp/scripts/ci_run.sh
+++ b/targets/sv-comp/scripts/ci_run.sh
@@ -1,7 +1,8 @@
 #!/bin/bash
 
-# Name of the virtual environment directory
-VENV_DIR="venv"
+# Name of the virtual environment directory (the svcomp CLI spawns the explorer
+# via .venv/bin/python3, so this must be .venv).
+VENV_DIR=".venv"
 echo "::group::Prepare dependencies..."
 # Check if the virtual environment directory exists
 if [ ! -d "$VENV_DIR" ]; then
@@ -23,7 +24,7 @@ rm -rf ../sv-benchmarks/.github
 echo "::endgroup::"
 
 echo "Running Tests..."
-python3 target_execution.py
+python3 svcomp.py test run --mode parallel --categories valid-assert.prp
 
 # Deactivate the virtual environment (optional)
 deactivate
diff --git a/targets/sv-comp/scripts/command_generation.py b/targets/sv-comp/scripts/command_generation.py
deleted file mode 100644
index 37c2b5e..0000000
--- a/targets/sv-comp/scripts/command_generation.py
+++ /dev/null
@@ -1,115 +0,0 @@
-from target_selection import extract_testcases
-import logging
-import socket
-from pathlib import Path
-from pprint import pformat
-from dtypes import Command, VerificationTask
-
-logging.basicConfig(level=logging.INFO)
-logger = logging.getLogger(__name__)
-
-SCRIPT_DIR = Path(__file__).resolve().parent
-BASE_PATH = SCRIPT_DIR.parents[2]
-PYENV_PATH = SCRIPT_DIR / '.venv' / 'bin' / 'python3'
-
-
-def is_port_available(port: int) -> bool:
-    """
-    Check if a port is available for binding.
-
-    Args:
-        port: The port number to check
-
-    Returns:
-        True if the port is available, False if occupied
-    """
-    sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
-    try:
-        sock.bind(('127.0.0.1', port))
-        sock.close()
-        return True
-    except OSError:
-        return False
-
-
-def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=8087, config_file:str = 'swat.cfg') -> list[str]:
-
-
-    test_case_dir = ver_task['file_path'].parent
-    agent_path = BASE_PATH / 'symbolic-executor' / 'lib' / 'symbolic-executor.jar'
-    config_path = SCRIPT_DIR / '..' / config_file
-    library_path = BASE_PATH / 'libs' / 'java-library-path'
-
-    base_command: list[str] = [str(PYENV_PATH), "-u", str(BASE_PATH / 'symbolic-explorer' / 'SymbolicExplorer.py'),
-                    "-prp", ver_task['category'].value,
-                    "--agent", str(agent_path),
-                    "--config", str(config_path),
-                    "-z3", str(library_path),
-                    "--logdir", str(logging_dir),
-                    "--mode", "sv-comp",
-                    '--port', str(port),
-                    "--classpath"]
-
-    cp: list[str] = []
-    for input_file in ver_task['input_files']:
-        cp.append(str((test_case_dir / input_file).resolve()))
-        cp.append(str(BASE_PATH / 'libs' / 'java-library-path' / 'com.microsoft.z3.jar'))
-    return base_command + cp 
-
-
-
-
-def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg') -> list[VerificationTask]:
-
-    port = 9000
-    skipped_ports = []
-
-    for ver_task in ver_tasks:
-        # Find next available port
-        while not is_port_available(port):
-            skipped_ports.append(port)
-            port += 1
-
-            # Safety check: don't go beyond reasonable port range
-            if port > 65535:
-                raise RuntimeError("Ran out of available ports! Too many ports occupied.")
-
-        # Extract unique identifier for the target (based on its relative path and the name of the .yml file)
-        target_dir = ver_task['file_path'].parent
-
-        # Get relative path from sv-benchmarks/java/
-        sv_benchmarks_java = Path('sv-benchmarks') / 'java'
-        rel_target_path = target_dir.relative_to(target_dir.parents[len(target_dir.parts) - list(target_dir.parts).index('sv-benchmarks') - 1] / sv_benchmarks_java)
-
-        target_name = ver_task['file_path'].stem
-        target = rel_target_path / target_name
-
-        # Include category in log dir to avoid collisions when same file has multiple properties
-        category_suffix = ver_task['category'].value.replace('.prp', '')
-        logging_dir = SCRIPT_DIR / '..' / 'logs' / rel_target_path / f"{target_name}_{category_suffix}"
-        command: Command = {
-            'target_dir': target_dir,
-            'target': target,
-            'log_dir': logging_dir,
-            'command': generate_command(ver_task, logging_dir, port=port, config_file=config_file)
-        }
-        ver_task['command'] = command
-        port += 1
-
-    if skipped_ports:
-        logger.warning(f"Skipped {len(skipped_ports)} occupied ports during command generation: {skipped_ports[:10]}{'...' if len(skipped_ports) > 10 else ''}")
-
-    return ver_tasks
-    
-    
-if __name__ == "__main__":
-    logger.info("Generating commands...")
-    task_dir = SCRIPT_DIR.parent / 'sv-benchmarks'
-    logger.info(f"Base directory: {task_dir}")
-    ver_tasks: list[VerificationTask] = extract_testcases(task_dir)
-    logger.info(f"Extracted {len(ver_tasks)} test cases.")
-    commands = generate_commands(ver_tasks)
-    logger.info(f"Generated {len(commands)} commands.")
-    logger.info("\nFirst 3 commands:")
-    for i, command in enumerate(commands[:3], 1):
-        logger.info(f"\nCommand {i}:\n{pformat(dict(command), width=100)}")
\ No newline at end of file
diff --git a/targets/sv-comp/scripts/commands/analyze.py b/targets/sv-comp/scripts/commands/analyze.py
index d214a38..ce71578 100644
--- a/targets/sv-comp/scripts/commands/analyze.py
+++ b/targets/sv-comp/scripts/commands/analyze.py
@@ -3,7 +3,6 @@
 import click
 import logging
 from pathlib import Path
-import sys
 
 logger = logging.getLogger(__name__)
 
@@ -15,57 +14,29 @@ def analyze():
 
 
 @analyze.command(name='results')
-@click.argument('results_file', type=click.Path(exists=True), required=False)
-@click.option('--logs-dir', type=click.Path(exists=True), help='Path to logs directory')
+@click.argument('run_dir', type=click.Path(exists=True), required=False)
 @click.pass_context
-def analyze_results(ctx, results_file, logs_dir):
-    """Analyze results to identify context losses and failures.
+def analyze_results(ctx, run_dir):
+    """Analyze a run from its consolidated stats.json files.
 
-    If RESULTS_FILE is not provided, will use the most recent results file.
+    Prints a scoring summary plus the missing-invocation superset and its
+    context-loss subset. If RUN_DIR is not provided, uses the most recent
+    runs/run_* directory.
     """
-    from lib.analysis.context_loss import main as run_analysis
+    from lib.analysis.context_loss import analyze_run, find_latest_run
 
     script_dir = ctx.obj['script_dir']
 
-    # Determine results file
-    if results_file:
-        results_path = Path(results_file)
+    if run_dir:
+        run_path = Path(run_dir)
     else:
-        # Look for latest results file
-        results_dir = script_dir.parent / 'results'
-        if results_dir.exists():
-            json_files = list(results_dir.glob('results_*.json'))
-            if json_files:
-                results_path = max(json_files, key=lambda p: p.stat().st_mtime)
-                click.echo(f"Using latest results file: {results_path}")
-            else:
-                click.echo("Error: No results files found in results/", err=True)
-                ctx.exit(1)
-        else:
-            click.echo("Error: results/ directory not found and no file specified", err=True)
+        run_path = find_latest_run(script_dir.parent / 'runs')
+        if run_path is None:
+            click.echo("Error: No runs found under runs/. Run 'svcomp test run' first.", err=True)
             ctx.exit(1)
+        click.echo(f"Using latest run: {run_path}")
 
-    # Determine logs directory
-    if logs_dir:
-        logs_path = Path(logs_dir)
-    else:
-        logs_path = script_dir.parent / 'logs'
-
-    if not logs_path.exists():
-        click.secho(f"Warning: Logs directory not found at {logs_path}", fg='yellow')
-
-    click.echo(f"Analyzing results from: {results_path}")
-    click.echo(f"Looking for logs in: {logs_path}\n")
-
-    # Run the analysis by temporarily modifying sys.argv
-    old_argv = sys.argv
-    try:
-        sys.argv = ['analyse_ctx_loss.py', str(results_path)]
-        run_analysis()
-    except SystemExit:
-        pass  # analysis script calls sys.exit
-    finally:
-        sys.argv = old_argv
+    analyze_run(run_path)
 
 
 @analyze.command(name='compare')
diff --git a/targets/sv-comp/scripts/commands/test.py b/targets/sv-comp/scripts/commands/test.py
index a40e526..f0398c0 100644
--- a/targets/sv-comp/scripts/commands/test.py
+++ b/targets/sv-comp/scripts/commands/test.py
@@ -72,6 +72,7 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file, categories, target
         check_port_availability,
         VerificationCategory,
     )
+    from lib.command_gen import new_run_timestamp, run_dir as make_run_dir
     script_dir = ctx.obj['script_dir']
 
     # Determine benchmark directory
@@ -107,13 +108,15 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file, categories, target
                 click.echo(f"Filtered to {len(ver_tasks)} test cases for categories: {[c.value for c in selected_categories]}")
 
         # Generate commands
-        if mode == 'single' and target is None:
+        if mode == 'single':
             # Use default target from original script
             config = 'swat-debug.cfg'
         else:
             config = config_file
 
-        ver_tasks_with_commands = generate_commands(ver_tasks, config)
+        # One timestamp ties this run's per-testcase logs to its results dir.
+        run_timestamp = new_run_timestamp()
+        ver_tasks_with_commands = generate_commands(ver_tasks, config, run_timestamp=run_timestamp)
         click.echo(f"Generated {len(ver_tasks_with_commands)} commands")
 
         # Check port availability
@@ -143,7 +146,9 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file, categories, target
                 # Run default single target
                 run_single_target(ver_tasks_with_commands, create_witness=not no_witness)
         else:
-            run_parallel(ver_tasks_with_commands, max_workers=workers, create_witness=not no_witness)
+            run = make_run_dir(run_timestamp)
+            click.echo(f"Run directory: {run}")
+            run_parallel(ver_tasks_with_commands, max_workers=workers, create_witness=not no_witness, run_dir=run)
 
         click.secho("✓ Test execution complete", fg='green')
 
diff --git a/targets/sv-comp/scripts/commands/util.py b/targets/sv-comp/scripts/commands/util.py
index f4ffbf6..c8da339 100644
--- a/targets/sv-comp/scripts/commands/util.py
+++ b/targets/sv-comp/scripts/commands/util.py
@@ -109,18 +109,16 @@ def show_config(ctx):
     click.echo(f"\nBenchmark directory: {benchmark_dir}")
     click.echo(f"  Exists: {benchmark_dir.exists()}")
 
-    # Show results directory
-    results_dir = script_dir.parent / 'results'
-    click.echo(f"\nResults directory: {results_dir}")
-    click.echo(f"  Exists: {results_dir.exists()}")
-    if results_dir.exists():
-        result_files = list(results_dir.glob('results_*.json'))
-        click.echo(f"  Result files: {len(result_files)}")
-
-    # Show logs directory
-    logs_dir = script_dir.parent / 'logs'
-    click.echo(f"\nLogs directory: {logs_dir}")
-    click.echo(f"  Exists: {logs_dir.exists()}")
+    # Show runs directory (each run has its own runs/run_<timestamp>/{logs,results})
+    runs_dir = script_dir.parent / 'runs'
+    click.echo(f"\nRuns directory: {runs_dir}")
+    click.echo(f"  Exists: {runs_dir.exists()}")
+    if runs_dir.exists():
+        run_dirs = sorted((p for p in runs_dir.glob('run_*') if p.is_dir()),
+                          key=lambda p: p.stat().st_mtime)
+        click.echo(f"  Runs: {len(run_dirs)}")
+        if run_dirs:
+            click.echo(f"  Latest run: {run_dirs[-1].name}")
 
 
 @util.command(name='check-deps')
diff --git a/targets/sv-comp/scripts/compare_results.py b/targets/sv-comp/scripts/compare_results.py
deleted file mode 100644
index d25a49d..0000000
--- a/targets/sv-comp/scripts/compare_results.py
+++ /dev/null
@@ -1,56 +0,0 @@
-import json
-import os
-
-def compare_results(current_file, reference_file):
-    # Load current and reference data
-    with open(current_file, 'r') as f:
-        current_data = json.load(f)
-
-    with open(reference_file, 'r') as f:
-        reference_data = json.load(f)
-
-    # Extract results from both files
-    current_results = current_data.get("results", {})
-    reference_results = reference_data.get("results", {})
-
-    # Compare cases
-    changes = []
-    for case, current_value in current_results.items():
-        current_status = current_value[0]  # Extract the status from the current results
-
-        # Check if the case exists in reference
-        if case in reference_results:
-            reference_status = reference_results[case][0]  # Extract the status from the reference results
-            if current_status != reference_status:
-                changes.append({
-                    "case": case,
-                    "from": reference_status,
-                    "to": current_status
-                })
-        else:
-            # New case added in current results
-            changes.append({
-                "case": case,
-                "from": "Not present",
-                "to": current_status
-            })
-
-    # Identify cases removed in the current results
-    for case in reference_results:
-        if case not in current_results:
-            changes.append({
-                "case": case,
-                "from": reference_results[case][0],
-                "to": "Removed"
-            })
-
-    # Print the changes
-    for change in changes:
-        print(f"Case: {change['case']} changed from {change['from']} to {change['to']}")
-
-# Replace these with paths to your JSON files
-SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__))
-current_file = os.path.join(SCRIPT_DIR, '..', 'results', "results_20241122_103412.json")
-reference_file = os.path.join(SCRIPT_DIR, '..', 'results', "results_20241122_100419.json")
-
-compare_results(current_file, reference_file)
diff --git a/targets/sv-comp/scripts/dtypes.py b/targets/sv-comp/scripts/dtypes.py
deleted file mode 100644
index 9d2f1c6..0000000
--- a/targets/sv-comp/scripts/dtypes.py
+++ /dev/null
@@ -1,38 +0,0 @@
-from pathlib import Path
-from typing import Optional, TypedDict
-import enum
-
-class ExpectedVerdict(enum.Enum):
-    VIOLATION = False
-    SAFE = True
-
-class Verdict(enum.Enum):
-    VIOLATION = "== ERROR"
-    SAFE = "== OK"
-    UNKNOWN = "== DONT-KNOW"
-    NO_SYMBOLIC_VARS = "== NON-SYMBOLIC"
-    
-class VerificationCategory(enum.Enum):
-    VALID_ASSERT_PRP = "valid-assert.prp"
-    NO_RUNTIME_EXCEPTION_PRP = "no-runtime-exception.prp"
-    NO_DEADLOCK_PRP = "no-deadlock.prp"
-
-class Command(TypedDict):
-    target_dir: Path
-    target: Path
-    log_dir: Path
-    command: list[str]
-    
-class VerificationResult(TypedDict):
-    points: int
-    case: str
-    
-class VerificationTask(TypedDict):
-    category: VerificationCategory
-    verdict: ExpectedVerdict
-    file_path: Path
-    input_files: list[Path]
-    command: Optional[Command]
-    result: Optional[VerificationResult]
-    
-    
\ No newline at end of file
diff --git a/targets/sv-comp/scripts/lib/analysis/context_loss.py b/targets/sv-comp/scripts/lib/analysis/context_loss.py
index f8019d6..26ce238 100644
--- a/targets/sv-comp/scripts/lib/analysis/context_loss.py
+++ b/targets/sv-comp/scripts/lib/analysis/context_loss.py
@@ -1,398 +1,226 @@
 #!/usr/bin/env python3
 """
-Analyze SV-Comp results to identify context loss methods that need implementation.
-Run this script in the directory containing the results JSON file.
+Analyze a SV-COMP run from its consolidated per-testcase ``stats.json`` files.
 
-Usage: python3 analyse_ctx_loss.py results_valid-assert.prp_XXXXXX.json
+A run lives under ``runs/run_<timestamp>/`` with:
+  - ``results/results_<category>_<ts>.json`` : per-target verdict / points / timing
+  - ``logs/<rel>/<name>_<cat>/stats.json``   : per-testcase missing invocations,
+                                               context-loss subset, execution errors
+
+This reads that structured data directly — no log scraping — and prints a scoring
+summary (Correct / Failed / Unk / Error / Timeout) plus the missing-invocation
+superset and its authoritative context-loss subset (issue #25).
 """
 
 import json
 import sys
-import re
 from collections import defaultdict
 from pathlib import Path
+from typing import Optional
 
+# lib/analysis/context_loss.py -> scripts/
+SCRIPT_DIR = Path(__file__).resolve().parents[2]
 
-def extract_context_loss_methods(log_content: str) -> list[str]:
-    """Extract all method names causing context loss from log content."""
-    methods = set()  # Use set to dedupe
-    if not log_content:
-        return list(methods)
-
-    # Look for "Context loss:" pattern
-    for match in re.finditer(r'Context loss:\s*(.+?)(?:\n|$)', log_content):
-        methods.add(match.group(1).strip())
-
-    # Also look for "Uninstrumented invocation" pattern
-    for match in re.finditer(r'Uninstrumented invocation.*?:\s*(.+?)(?:\n|$)', log_content):
-        methods.add(match.group(1).strip())
-
-    # Look for "Context loss recorded" with method info on previous lines
-    for match in re.finditer(r'(\S+\.\S+)\s*\n.*Context loss recorded', log_content):
-        methods.add(match.group(1).strip())
-
-    return list(methods)
-
+SCORE_BUCKETS = ['Correct', 'Failed', 'Unk', 'Error', 'Timeout']
 
-def extract_missing_invocations(log_content: str) -> list[str]:
-    """Extract missing/unimplemented method invocations from log content."""
-    methods = set()  # Use set to dedupe
-    if not log_content:
-        return list(methods)
 
-    # Pattern: "Error visiting Instruction INVOKE* owner/class/method:desc"
-    # Example: "Error visiting Instruction INVOKEVIRTUAL java/lang/Double/byteValue:()B"
-    for match in re.finditer(
-        r'Error visiting Instruction (INVOKE\w+)\s+(\S+?)(?:\s*\(|$)',
-        log_content
-    ):
-        invoke_type = match.group(1)
-        method_sig = match.group(2)
-        # Clean up the method signature (remove id info if present)
-        method_sig = re.sub(r'\s*\(id:.*', '', method_sig)
-        methods.add(f"{invoke_type} {method_sig}")
+def find_latest_run(runs_root: Path) -> Optional[Path]:
+    """Return the most recently modified runs/run_* directory, or None."""
+    if not runs_root.exists():
+        return None
+    run_dirs = [p for p in runs_root.glob('run_*') if p.is_dir()]
+    if not run_dirs:
+        return None
+    return max(run_dirs, key=lambda p: p.stat().st_mtime)
 
-    # Pattern: "Not implemented: <method> in <class>"
-    for match in re.finditer(r'Not implemented:\s*(.+?)\s+in\s+(\S+)', log_content):
-        method = match.group(1).strip()
-        cls = match.group(2).strip()
-        methods.add(f"NOT_IMPLEMENTED {cls}/{method}")
 
-    return list(methods)
+def classify(case: str, points, exec_status, error) -> str:
+    """Bucket a single result into Correct / Failed / Unk / Error / Timeout.
 
-
-def extract_symbolic_invocations_from_stats(stats_path: Path) -> list[str]:
+    Precedence: a timeout or a crash/error is reported as such regardless of points;
+    otherwise positive points are Correct, negative points are Failed (wrong verdict),
+    and zero points are Unknown (unknown / non-symbolic).
     """
-    Extract symbolic method invocations from stats JSON files.
-
-    Stats files contain entries like:
-    {"owner":"java/lang/Character","isSymbolic":true,"name":"isUnicodeIdentifierStart","desc":"(I)Z"}
-
-    Returns list of method signatures that have isSymbolic=true (missing implementations).
-    """
-    methods = set()
-
-    # Check both stats_1.json and stats_-1.json
-    for stats_file in ['stats_1.json', 'stats_-1.json']:
-        file_path = stats_path / stats_file
-        if not file_path.exists():
-            continue
-
-        try:
-            with open(file_path) as f:
-                data = json.load(f)
-
-            if isinstance(data, list):
-                for entry in data:
-                    if isinstance(entry, dict) and entry.get('isSymbolic', False):
-                        owner = entry.get('owner', '')
-                        name = entry.get('name', '')
-                        desc = entry.get('desc', '')
-                        is_instance = entry.get('isInstance', False)
-                        invoke_type = 'INVOKEVIRTUAL' if is_instance else 'INVOKESTATIC'
-                        if owner and name:
-                            methods.add(f"{invoke_type} {owner}/{name}:{desc}")
-        except (json.JSONDecodeError, IOError):
-            pass
-
-    return list(methods)
-
-
-def extract_errors(log_content: str) -> list[str]:
-    """Extract error messages from log content."""
-    errors = []
-    if not log_content:
-        return errors
-
-    # Look for SWAT Exception patterns
-    for match in re.finditer(r'\[SWAT Exception\]:\s*(.+?)(?:\n|$)', log_content):
-        errors.append(match.group(1).strip())
-
-    # Look for general exceptions
-    for match in re.finditer(r'Exception.*?:\s*(.+?)(?:\n|$)', log_content):
-        msg = match.group(1).strip()
-        if msg and len(msg) < 200:
-            errors.append(msg)
+    s = str(exec_status).lower()
+    if 'timeout' in s:
+        return 'Timeout'
+    if 'error' in s or error or 'crash' in str(case).lower():
+        return 'Error'
+    if points and points > 0:
+        return 'Correct'
+    if points and points < 0:
+        return 'Failed'
+    return 'Unk'
+
+
+def load_json(path: Path):
+    """Load a JSON file, returning None if it is missing or unreadable."""
+    try:
+        with open(path) as f:
+            return json.load(f)
+    except (OSError, json.JSONDecodeError):
+        return None
 
-    return errors
 
+def stats_path_for(logs_dir: Path, target: str, category: str) -> Path:
+    """Path to a testcase's stats.json, derived from its target and property."""
+    cat_short = category.replace('.prp', '')
+    return logs_dir / f"{target}_{cat_short}" / 'stats.json'
 
-def get_log_dir(logs_dir: Path, task_name: str, property_name: str) -> Path:
-    """
-    Construct the path to the log directory for a given task.
 
-    Task name format: folder/testname (e.g., "objects/objects03")
-    Log dir format: logs/<folder>/<testname>_<property>/
-    """
-    parts = task_name.split('/')
-    if len(parts) >= 2:
-        folder = parts[0]
-        testname = parts[1]
-    else:
-        folder = ""
-        testname = parts[0]
+def signature(inv: dict) -> str:
+    """Render a missing invocation as a stable owner/name:desc signature."""
+    return f"{inv['owner']}/{inv['name']}:{inv['desc']}"
 
-    # Property name like "valid-assert.prp" -> "valid-assert"
-    prop_short = property_name.replace('.prp', '')
 
-    return logs_dir / folder / f"{testname}_{prop_short}"
+def analyze_run(run_dir: Path):
+    """Aggregate and print the analysis for a single run directory."""
+    run_dir = Path(run_dir)
+    results_dir = run_dir / 'results'
+    logs_dir = run_dir / 'logs'
 
+    results_files = sorted(results_dir.glob('results_*.json'))
+    if not results_files:
+        print(f"No results files found in {results_dir}")
+        return
 
-def get_log_path(logs_dir: Path, task_name: str, property_name: str) -> Path:
-    """
-    Construct the path to the explorer.log for a given task.
-    """
-    return get_log_dir(logs_dir, task_name, property_name) / "explorer.log"
+    print(f"Analyzing run: {run_dir.name}")
+    print(f"  results: {results_dir}")
+    print(f"  logs:    {logs_dir}\n")
 
+    # Scoring buckets per category, and total points per category.
+    score: dict = {}
+    points_by_cat: dict = {}
 
-def get_stats_dir(logs_dir: Path, task_name: str, property_name: str) -> Path:
-    """
-    Construct the path to the stats directory (logs/ subdirectory) for a given task.
-    """
-    return get_log_dir(logs_dir, task_name, property_name) / "logs"
+    # Missing-invocation aggregation across all testcases of the run.
+    # signature -> {tasks: set, count: int, context_loss: bool, isSymbolic: bool}
+    missing: dict = {}
+    exec_errors: dict = defaultdict(list)  # message -> [tasks]
 
+    total_tasks = 0
+    stats_missing = 0  # testcases with no stats.json on disk
 
-def read_log_file(log_path: Path) -> str:
-    """Read log file content, return empty string if not found."""
-    try:
-        if log_path.exists():
-            return log_path.read_text(errors='replace')
-    except Exception:
-        pass
-    return ""
+    for rf in results_files:
+        data = load_json(rf)
+        if not data:
+            continue
+        category = data.get('category', rf.stem)
+        cat_buckets: dict = defaultdict(int)
+
+        for target, tup in data.get('results', {}).items():
+            total_tasks += 1
+            case = tup[0] if len(tup) > 0 else ''
+            points = tup[1] if len(tup) > 1 else 0
+            exec_status = tup[2] if len(tup) > 2 else ''
+            error = tup[3] if len(tup) > 3 else False
+            cat_buckets[classify(case, points, exec_status, error)] += 1
+
+            stats = load_json(stats_path_for(logs_dir, target, category))
+            if stats is None:
+                stats_missing += 1
+                continue
+            for inv in stats.get('missing_invocations', []):
+                sig = signature(inv)
+                m = missing.setdefault(
+                    sig, {'tasks': set(), 'count': 0, 'context_loss': False, 'isSymbolic': False})
+                m['tasks'].add(target)
+                m['count'] += inv.get('count', 1)
+                m['context_loss'] = m['context_loss'] or inv.get('context_loss', False)
+                m['isSymbolic'] = m['isSymbolic'] or inv.get('isSymbolic', False)
+            for e in stats.get('execution_errors', []):
+                exec_errors[e.get('message', '')].append(target)
+
+        score[category] = dict(cat_buckets)
+        points_by_cat[category] = data.get('points')
+
+    _print_scoring_summary(score, points_by_cat, total_tasks)
+    _print_missing_invocations(missing)
+    _print_execution_errors(exec_errors)
+
+    if stats_missing:
+        print(f"\nNote: {stats_missing} testcase(s) had no stats.json "
+              f"(crash before the explorer wrote one, or an older run).")
+
+
+def _print_scoring_summary(score: dict, points_by_cat: dict, total_tasks: int):
+    print("=" * 78)
+    print("SCORING SUMMARY")
+    print("=" * 78)
+    header = f"{'Category':<26}" + "".join(f"{b:>9}" for b in SCORE_BUCKETS) + f"{'Total':>8}{'Points':>9}"
+    print(header)
+    print("-" * len(header))
+
+    totals = {b: 0 for b in SCORE_BUCKETS}
+    total_points = 0
+    for category in sorted(score):
+        buckets = score[category]
+        row_total = sum(buckets.get(b, 0) for b in SCORE_BUCKETS)
+        pts = points_by_cat.get(category) or 0
+        total_points += pts
+        for b in SCORE_BUCKETS:
+            totals[b] += buckets.get(b, 0)
+        if row_total == 0:
+            continue  # don't clutter the table with categories that had no testcases
+        cells = "".join(f"{buckets.get(b, 0):>9}" for b in SCORE_BUCKETS)
+        print(f"{category:<26}{cells}{row_total:>8}{pts:>9}")
+
+    print("-" * len(header))
+    grand_total = sum(totals.values())
+    cells = "".join(f"{totals[b]:>9}" for b in SCORE_BUCKETS)
+    print(f"{'TOTAL':<26}{cells}{grand_total:>8}{total_points:>9}")
+    print()
+
+
+def _print_missing_invocations(missing: dict):
+    print("=" * 78)
+    cl = {sig: m for sig, m in missing.items() if m['context_loss']}
+    print(f"MISSING INVOCATIONS  (superset: {len(missing)} signatures; "
+          f"context-loss subset: {len(cl)})")
+    print("=" * 78)
+    if not missing:
+        print("None.")
+        print()
+        return
+
+    # Most-impactful first: by number of testcases, then total count.
+    for sig, m in sorted(missing.items(), key=lambda kv: (-len(kv[1]['tasks']), -kv[1]['count'])):
+        marker = "CL " if m['context_loss'] else "   "
+        print(f"  {marker}{len(m['tasks']):>4} tasks  (count={m['count']:<5}) {sig}")
+    print()
+
+    if cl:
+        print("-" * 78)
+        print(f"CONTEXT-LOSS METHODS (subset that caused symbolic context loss):")
+        for sig in sorted(cl):
+            print(f"    {sig}")
+        print()
+
+
+def _print_execution_errors(exec_errors: dict):
+    if not exec_errors:
+        return
+    print("=" * 78)
+    print(f"EXECUTION ERRORS  ({len(exec_errors)} distinct)")
+    print("=" * 78)
+    for msg, tasks in sorted(exec_errors.items(), key=lambda kv: -len(kv[1])):
+        unique = list(dict.fromkeys(tasks))
+        print(f"  {len(unique):>4} tasks  {msg[:90]}")
+        print(f"           e.g. {', '.join(unique[:3])}")
+    print()
 
 
 def main():
-    if len(sys.argv) < 2:
-        # Find the latest results file
-        results_dir = Path('.')
-        json_files = list(results_dir.glob('results_*.json'))
-        if not json_files:
-            json_files = list(Path('results').glob('results_*.json'))
-        if not json_files:
-            print("Usage: python3 analyse_ctx_loss.py <results_file.json>")
-            print("No results files found in current directory")
-            sys.exit(1)
-        results_file = max(json_files, key=lambda p: p.stat().st_mtime)
-        print(f"Using latest results file: {results_file}")
-    else:
-        results_file = Path(sys.argv[1])
-
-    # Determine logs directory (sibling to results file or parent's logs/)
-    if results_file.parent.name == 'results':
-        logs_dir = results_file.parent.parent / 'logs'
+    """Standalone entry point: analyze a run dir argument or the latest run."""
+    if len(sys.argv) >= 2:
+        run_dir = Path(sys.argv[1])
     else:
-        logs_dir = results_file.parent / 'logs'
-
-    print(f"Looking for logs in: {logs_dir}")
-
-    with open(results_file) as f:
-        data = json.load(f)
-
-    results = data['results']
-    category = data.get('category', 'valid-assert.prp')
-
-    # Analyze all 0-point tasks
-    zero_points_by_folder = defaultdict(list)
-    context_loss_methods = defaultdict(list)
-    missing_invocations = defaultdict(list)
-    all_errors = defaultdict(list)
-
-    for name, task in results.items():
-        # task format: [status_change, points, execution_status, error_bool, validated, time]
-        points = task[1]
-        if points == 0:
-            folder = name.split('/')[0]
-            status = task[0]
-            exec_status = task[2]
-
-            # Read the actual log file from disk
-            log_path = get_log_path(logs_dir, name, category)
-            log_content = read_log_file(log_path)
-
-            # Get stats directory for symbolic invocations
-            stats_dir = get_stats_dir(logs_dir, name, category)
-
-            zero_points_by_folder[folder].append({
-                'name': name,
-                'status': status,
-                'exec_status': exec_status,
-                'log_path': str(log_path),
-                'log_content': log_content,
-                'log_exists': log_path.exists(),
-                'stats_dir': str(stats_dir)
-            })
-
-            # Extract context loss methods
-            methods = extract_context_loss_methods(log_content)
-            for method in methods:
-                context_loss_methods[method].append(name)
-
-            # Extract missing invocations from error logs
-            invocations = extract_missing_invocations(log_content)
-            for inv in invocations:
-                missing_invocations[inv].append(name)
-
-            # Extract symbolic invocations from stats JSON files
-            symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir)
-            for inv in symbolic_invocations:
-                missing_invocations[inv].append(name)
-
-            # Extract errors
-            errors = extract_errors(log_content)
-            for error in errors:
-                all_errors[error].append(name)
-
-    # Print summary by folder
-    print("\n" + "=" * 80)
-    print("TASKS WITH 0 POINTS BY FOLDER")
-    print("=" * 80)
-    total_zero = 0
-    logs_found = 0
-    for folder, tasks in sorted(zero_points_by_folder.items(), key=lambda x: -len(x[1])):
-        folder_logs_found = sum(1 for t in tasks if t['log_exists'])
-        print(f"{folder}: {len(tasks)} tasks ({folder_logs_found} logs found)")
-        total_zero += len(tasks)
-        logs_found += folder_logs_found
-    print(f"\nTotal: {total_zero} tasks with 0 points ({logs_found} logs found)")
-
-    # Print context loss methods sorted by frequency
-    print("\n" + "=" * 80)
-    print("CONTEXT LOSS METHODS (sorted by frequency)")
-    print("=" * 80)
-
-    if not context_loss_methods:
-        print("No context loss methods found in logs.")
-    else:
-        for method, tasks in sorted(context_loss_methods.items(), key=lambda x: -len(x[1])):
-            print(f"\n{len(tasks):3d} tasks - {method}")
-            print(f"    Examples: {', '.join(tasks[:3])}")
-
-    # Print missing invocations sorted by frequency
-    print("\n" + "=" * 80)
-    print("MISSING/UNIMPLEMENTED INVOCATIONS (sorted by frequency)")
-    print("=" * 80)
-
-    if not missing_invocations:
-        print("No missing invocations found in logs.")
-    else:
-        for inv, tasks in sorted(missing_invocations.items(), key=lambda x: -len(x[1])):
-            # Dedupe task list (same task may appear multiple times)
-            unique_tasks = list(dict.fromkeys(tasks))
-            print(f"\n{len(unique_tasks):3d} tasks - {inv}")
-            print(f"    Examples: {', '.join(unique_tasks[:3])}")
-
-    # Print errors sorted by frequency
-    print("\n" + "=" * 80)
-    print("ERRORS (sorted by frequency)")
-    print("=" * 80)
-
-    if not all_errors:
-        print("No specific errors found in logs.")
-    else:
-        for error, tasks in sorted(all_errors.items(), key=lambda x: -len(x[1]))[:20]:
-            print(f"\n{len(tasks):3d} tasks - {error[:100]}")
-            print(f"    Examples: {', '.join(tasks[:3])}")
-
-    # Detailed breakdown for each folder
-    print("\n" + "=" * 80)
-    print("DETAILED BREAKDOWN BY FOLDER")
-    print("=" * 80)
-
-    for folder in ['autostub', 'jbmc-regression', 'java-ranger-regression', 'algorithms', 'argv-tasks', 'float-nonlinear-calculation', 'securibench', 'objects']:
-        if folder not in zero_points_by_folder:
-            continue
-
-        print(f"\n--- {folder} ({len(zero_points_by_folder[folder])} tasks) ---")
-
-        folder_context_loss = defaultdict(list)
-        folder_missing_invocations = defaultdict(list)
-        folder_errors = defaultdict(list)
-        other_issues = defaultdict(list)
-        tasks_with_missing_invocations = set()
-
-        for task in zero_points_by_folder[folder]:
-            log_content = task['log_content']
-            stats_dir = Path(task['stats_dir'])
-            methods = extract_context_loss_methods(log_content)
-            invocations = extract_missing_invocations(log_content)
-            symbolic_invocations = extract_symbolic_invocations_from_stats(stats_dir)
-            errors = extract_errors(log_content)
-
-            if methods:
-                for method in methods:
-                    folder_context_loss[method].append(task['name'])
-
-            all_invocations = invocations + symbolic_invocations
-            if all_invocations:
-                tasks_with_missing_invocations.add(task['name'])
-                for inv in all_invocations:
-                    folder_missing_invocations[inv].append(task['name'])
-
-            # Always categorize by verdict/status (not just when no missing invocations)
-            if errors:
-                for error in errors:
-                    folder_errors[error[:80]].append(task['name'])
-
-            if 'timeout' in task['exec_status'].lower():
-                other_issues['timeout'].append(task['name'])
-            elif not task['log_exists']:
-                other_issues['log file not found'].append(task['name'])
-            elif not log_content.strip():
-                other_issues['log file empty'].append(task['name'])
-            elif 'DONT-KNOW' in log_content:
-                other_issues['verdict: DONT-KNOW'].append(task['name'])
-            elif 'NoThreadContextException' in log_content:
-                other_issues['NoThreadContextException'].append(task['name'])
-            elif not methods and not all_invocations:
-                other_issues['unknown (check log)'].append(task['name'])
-
-        if folder_context_loss:
-            print("  Context loss methods:")
-            for method, tasks in sorted(folder_context_loss.items(), key=lambda x: -len(x[1]))[:10]:
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {method[:80]}")
-
-        if folder_missing_invocations:
-            print(f"  Missing invocations ({len(tasks_with_missing_invocations)} unique tasks):")
-            for inv, tasks in sorted(folder_missing_invocations.items(), key=lambda x: -len(x[1]))[:10]:
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {inv[:80]}")
-
-        if folder_errors:
-            print("  Errors:")
-            for error, tasks in sorted(folder_errors.items(), key=lambda x: -len(x[1]))[:10]:
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {error[:80]}")
-
-        if other_issues:
-            print("  Other issues:")
-            for issue, tasks in sorted(other_issues.items(), key=lambda x: -len(x[1])):
-                unique_tasks = list(dict.fromkeys(tasks))
-                print(f"    {len(unique_tasks):3d} - {issue[:80]}")
-
-    # Print sample logs for debugging
-    print("\n" + "=" * 80)
-    print("SAMPLE LOGS (first 5 tasks with 0 points)")
-    print("=" * 80)
-
-    count = 0
-    for name, task in results.items():
-        if task[1] == 0 and count < 5:
-            log_path = get_log_path(logs_dir, name, category)
-            log_content = read_log_file(log_path)
-
-            print(f"\n{name}:")
-            print(f"  Status: {task[0]}")
-            print(f"  Exec status: {task[2]}")
-            print(f"  Log path: {log_path}")
-            print(f"  Log exists: {log_path.exists()}")
-            if log_content:
-                # Show last 500 chars which usually has the verdict
-                print(f"  Log tail: ...{log_content[-500:]}")
-            else:
-                print(f"  Log: (empty or not found)")
-            count += 1
+        run_dir = find_latest_run(SCRIPT_DIR / '..' / 'runs')
+        if run_dir is None:
+            print("Usage: python3 -m lib.analysis.context_loss <run_dir>")
+            print("No runs found under runs/")
+            sys.exit(1)
+        print(f"Using latest run: {run_dir}")
+    analyze_run(run_dir)
 
 
 if __name__ == '__main__':
diff --git a/targets/sv-comp/scripts/lib/command_gen.py b/targets/sv-comp/scripts/lib/command_gen.py
index ccfa7f6..9bf39f7 100644
--- a/targets/sv-comp/scripts/lib/command_gen.py
+++ b/targets/sv-comp/scripts/lib/command_gen.py
@@ -1,8 +1,10 @@
 from .selection import extract_testcases
+import datetime
 import logging
 import socket
 from pathlib import Path
 from pprint import pformat
+from typing import Optional
 from .dtypes import Command, VerificationTask
 
 logging.basicConfig(level=logging.INFO)
@@ -59,13 +61,27 @@ def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=80
 
 
 
-def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg') -> list[VerificationTask]:
+def new_run_timestamp() -> str:
+    """Returns a timestamp identifying a single run, shared across all its outputs."""
+    return datetime.datetime.now().strftime("%Y%m%d_%H%M%S")
+
+
+def run_dir(run_timestamp: str) -> Path:
+    """The directory holding a non-debug run's logs/ and results/."""
+    return SCRIPT_DIR / '..' / 'runs' / f"run_{run_timestamp}"
+
+
+def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swat.cfg', run_timestamp: Optional[str] = None) -> list[VerificationTask]:
 
     port = 9000
     skipped_ports = []
 
-    # Determine log directory base based on config file
-    log_dir_base = 'logs-debug' if 'debug' in config_file.lower() else 'logs'
+    # A single timestamp ties a run's per-testcase logs to its results.
+    if run_timestamp is None:
+        run_timestamp = new_run_timestamp()
+
+    # Debug runs keep a timestamped history per target; normal runs share one run dir.
+    is_debug = 'debug' in config_file.lower()
 
     for ver_task in ver_tasks:
         # Find next available port
@@ -89,7 +105,14 @@ def generate_commands(ver_tasks: list[VerificationTask], config_file: str = 'swa
 
         # Include category in log dir to avoid collisions when same file has multiple properties
         category_suffix = ver_task['category'].value.replace('.prp', '')
-        logging_dir = SCRIPT_DIR / '..' / log_dir_base / rel_target_path / f"{target_name}_{category_suffix}"
+        testcase = f"{target_name}_{category_suffix}"
+        if is_debug:
+            # runs-debug/<rel>/<testcase>/run_<ts>/logs — grouped per target so a debug
+            # session keeps the history of its runs together.
+            logging_dir = SCRIPT_DIR / '..' / 'runs-debug' / rel_target_path / testcase / f"run_{run_timestamp}" / 'logs'
+        else:
+            # runs/run_<ts>/logs/<rel>/<testcase> — all testcases of a run share one run dir.
+            logging_dir = run_dir(run_timestamp) / 'logs' / rel_target_path / testcase
         command: Command = {
             'target_dir': target_dir,
             'target': target,
diff --git a/targets/sv-comp/scripts/lib/execution.py b/targets/sv-comp/scripts/lib/execution.py
index fbf1f1d..db5c354 100644
--- a/targets/sv-comp/scripts/lib/execution.py
+++ b/targets/sv-comp/scripts/lib/execution.py
@@ -8,7 +8,7 @@
 from pprint import pformat
 from .dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command
 from .utils import ci_print
-from .command_gen import extract_testcases, generate_commands
+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 collections import Counter
 from pathlib import Path
@@ -283,7 +283,15 @@ def run_command_with_timeout(cmd: list[str], timeout: int = 900) -> tuple[Execut
 
  
 
-def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50, create_witness: bool = True):
+def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50, create_witness: bool = True, run_dir: Optional[Path] = None, run_timestamp: Optional[str] = None):
+    # Resolve the run context so all outputs (per-testcase logs + aggregated results) share one dir.
+    if run_timestamp is None:
+        run_timestamp = run_dir.name.replace('run_', '') if run_dir is not None else new_run_timestamp()
+    if run_dir is None:
+        run_dir = make_run_dir(run_timestamp)
+    run_dir = Path(run_dir)
+    results_dir = run_dir / 'results'
+
     max_workers = min(max_workers, len(ver_tasks))
 
     logger.info(f"Running parallel target execution with {max_workers} workers...")
@@ -315,13 +323,13 @@ def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50, create_
     total_elapsed_time = time.perf_counter() - total_start_time
     logger.info(f"Total parallel execution time: {total_elapsed_time:.2f}s")
 
-    evaluate_results(results)
+    evaluate_results(results, results_dir, run_timestamp)
 
     # Run aggregate analysis from timing files
     from .analysis.timing import TimingAnalysis
-    TimingAnalysis.print_timing_statistics()
+    TimingAnalysis.print_timing_statistics(run_dir / 'logs')
 
-def evaluate_results(results):
+def evaluate_results(results, results_dir: Path, run_timestamp: str):
     """Evaluate results with per-category statistics including timing."""
     total_points = 0
     category_stats = {}
@@ -473,13 +481,13 @@ def evaluate_results(results):
         all_elapsed = [t[2] for t in all_times]
         logger.info(f"Overall timing: min={min(all_elapsed):.2f}s, max={max(all_elapsed):.2f}s, mean={sum(all_elapsed)/len(all_elapsed):.2f}s")
 
-    save_results(category_stats, results)
+    save_results(category_stats, results, results_dir, run_timestamp)
 
     # Save aggregate stage timing to CSV
-    save_aggregate_stage_timing(category_stats)
+    save_aggregate_stage_timing(category_stats, results_dir, run_timestamp)
 
     # Generate timing histogram
-    generate_timing_histogram(category_stats, results)
+    generate_timing_histogram(category_stats, results, results_dir, run_timestamp)
 
     summary_path = os.getenv("GITHUB_STEP_SUMMARY")
     if summary_path is not None:
@@ -488,17 +496,17 @@ def evaluate_results(results):
     return total_points
 
 
-def generate_timing_histogram(category_stats, results, folder='results'):
+def generate_timing_histogram(category_stats, results, results_dir: Path, run_timestamp: str):
     """Generate histogram(s) of execution times using matplotlib."""
     if not MATPLOTLIB_AVAILABLE:
         logger.warning("matplotlib not available, skipping histogram generation. Install with: pip install matplotlib numpy")
         return
 
-    folder = os.path.join(SCRIPT_DIR, '..', folder)
+    folder = str(results_dir)
     if not os.path.exists(folder):
         os.makedirs(folder)
 
-    timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S")
+    timestamp = run_timestamp
 
     # Collect all times across categories
     all_times = []
@@ -610,14 +618,14 @@ def generate_timing_histogram(category_stats, results, folder='results'):
         logger.info(f"Timing boxplot saved to: {boxplot_path}")
 
 
-def save_results(category_stats, results, folder='results'):
+def save_results(category_stats, results, results_dir: Path, run_timestamp: str):
     """Save results with one JSON file per category, including timing data."""
-    folder = os.path.join(SCRIPT_DIR, '..', folder)
+    folder = str(results_dir)
 
     if not os.path.exists(folder):
         os.makedirs(folder)
 
-    timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S")
+    timestamp = run_timestamp
 
     # Save one file per category
     for category_name, stats in category_stats.items():
@@ -656,14 +664,14 @@ def save_results(category_stats, results, folder='results'):
         logger.info(f"[{category_name}] Results saved to {filepath}")
 
 
-def save_aggregate_stage_timing(category_stats, folder='results'):
+def save_aggregate_stage_timing(category_stats, results_dir: Path, run_timestamp: str):
     """Save aggregate stage timing data to CSV file for easy analysis."""
-    folder = os.path.join(SCRIPT_DIR, '..', folder)
+    folder = str(results_dir)
 
     if not os.path.exists(folder):
         os.makedirs(folder)
 
-    timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S")
+    timestamp = run_timestamp
     filename = f"stage_timing_{timestamp}.csv"
     filepath = os.path.join(folder, filename)
 
@@ -834,7 +842,8 @@ def run_single_target(ver_tasks: list[VerificationTask], create_witness: bool =
         config_file = "sv-comp.cfg"
     else:
         raise ValueError(f"Invalid mode: {mode}")
-    ver_tasks_with_commands = generate_commands(ver_tasks, config_file)#[:10]
+    run_timestamp = new_run_timestamp()
+    ver_tasks_with_commands = generate_commands(ver_tasks, config_file, run_timestamp=run_timestamp)#[:10]
     logger.info(f"Generated {len(ver_tasks_with_commands)} commands.")
 
     # Check port availability before starting tests (sanity check)
@@ -848,7 +857,7 @@ def run_single_target(ver_tasks: list[VerificationTask], create_witness: bool =
     if mode == Mode.SINGLE_TARGET: # type: ignore
         run_single_target(ver_tasks_with_commands)
     elif mode == Mode.PARALLEL:
-        run_parallel(ver_tasks_with_commands)
+        run_parallel(ver_tasks_with_commands, run_timestamp=run_timestamp)
     else:
         raise ValueError(f"Invalid mode: {mode}")
 
diff --git a/targets/sv-comp/scripts/run_locally.sh b/targets/sv-comp/scripts/run_locally.sh
index 209bdc2..0915c5e 100755
--- a/targets/sv-comp/scripts/run_locally.sh
+++ b/targets/sv-comp/scripts/run_locally.sh
@@ -24,7 +24,7 @@ echo "Clone target Repository"
 "$SCRIPT_DIR/checkout.sh"
 
 echo "Running Tests..."
-python3 "$SCRIPT_DIR/target_execution.py"
+python3 "$SCRIPT_DIR/svcomp.py" test run --mode parallel --categories valid-assert.prp
 
 # Deactivate the virtual environment (optional)
 deactivate
diff --git a/targets/sv-comp/scripts/target_execution.py b/targets/sv-comp/scripts/target_execution.py
deleted file mode 100644
index 0184aba..0000000
--- a/targets/sv-comp/scripts/target_execution.py
+++ /dev/null
@@ -1,703 +0,0 @@
-from contextlib import contextmanager
-import logging, os, enum, subprocess
-import socket
-import time
-
-import concurrent.futures, json, datetime
-from typing import List, Optional
-from pprint import pformat
-from dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command
-from util import ci_print
-from command_generation import extract_testcases, generate_commands
-from witness_validation import generate_and_validate_witness
-from collections import Counter
-from pathlib import Path
-
-try:
-    import matplotlib.pyplot as plt
-    import numpy as np
-    MATPLOTLIB_AVAILABLE = True
-except ImportError:
-    MATPLOTLIB_AVAILABLE = False
-
-
-logging.basicConfig(level=logging.INFO)
-logger = logging.getLogger(__name__)
-SCRIPT_DIR = Path(__file__).resolve().parent
-
-class ExecutionStatus(enum.Enum):
-    SUCCESS = "success"
-    ERROR = "error"
-    TIMEOUT = "timeout"
-
-
-
-class Mode(enum.Enum):
-    SINGLE_TARGET = "single"
-    PARALLEL = "parallel"
-
-
-def check_port_availability(ver_tasks: list[VerificationTask]) -> tuple[bool, list[int]]:
-    """
-    Check if all ports required by verification tasks are available.
-
-    Args:
-        ver_tasks: List of verification tasks with command configuration
-
-    Returns:
-        Tuple of (all_available: bool, occupied_ports: list[int])
-    """
-    occupied_ports = []
-    required_ports = set()
-
-    # Extract all required ports from commands
-    for ver_task in ver_tasks:
-        command = ver_task.get('command')
-        if command:
-            cmd_list = command.get('command', [])
-            # Find --port argument
-            try:
-                port_idx = cmd_list.index('--port')
-                if port_idx + 1 < len(cmd_list):
-                    port = int(cmd_list[port_idx + 1])
-                    required_ports.add(port)
-            except (ValueError, IndexError):
-                continue
-
-    if not required_ports:
-        logger.info("No ports found in commands")
-        return True, []
-
-    logger.info(f"Checking availability of {len(required_ports)} ports (range: {min(required_ports)}-{max(required_ports)})")
-
-    # Check each port
-    for port in sorted(required_ports):
-        sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
-        try:
-            # Try to bind to the port
-            sock.bind(('127.0.0.1', port))
-            sock.close()
-        except OSError:
-            # Port is already in use
-            occupied_ports.append(port)
-
-    if occupied_ports:
-        logger.error(f"The following {len(occupied_ports)} ports are already in use: {occupied_ports}")
-        logger.error("Please kill the processes using these ports before running tests.")
-        logger.error(f"You can find processes with: lsof -i :{occupied_ports[0]} (for example)")
-        return False, occupied_ports
-    else:
-        logger.info(f"All {len(required_ports)} ports are available")
-        return True, []
-
-
-@contextmanager
-def pushd(dirname):
-    """Context manager to temporarily change the working directory."""
-    original_dir = os.getcwd()
-    logger.info(f"Changing directory to: {dirname}")
-    os.chdir(dirname)
-    try:
-        yield
-    finally:
-        os.chdir(original_dir)
-
-def reset_log_dir(log_dir) -> None:
-    logger.info("Resetting log directory...")
-    if os.path.exists(log_dir):
-        os.system(f"rm -rf {log_dir}")
-    os.makedirs(log_dir)
-
-
-def parse_verdict_from_output(output: List[str], category: VerificationCategory) -> Optional[Verdict]:
-    """Parse the verdict for a specific category from the output."""
-
-    for line in output:
-        if f"[VERDICT {category.value}]" in line:
-            if "== OK" in line:
-                return Verdict.SAFE
-            elif "== ERROR" in line:
-                return Verdict.VIOLATION
-            elif "== DONT-KNOW" in line:
-                return Verdict.UNKNOWN
-            elif "== NON-SYMBOLIC" in line:
-                return Verdict.NO_SYMBOLIC_VARS
-
-    return None  # No verdict found for this category
-
-
-def determine_result(output: List[str], category: VerificationCategory, expected_verdict: ExpectedVerdict) -> tuple[int, str]:
-    """Determine points and case based on the actual vs expected verdict for a single category."""
-    actual_verdict = parse_verdict_from_output(output, category)
-
-    # If no verdict found in output, treat as crash
-    if actual_verdict is None:
-        if expected_verdict == ExpectedVerdict.SAFE:
-            return 0, 'safe -> crash'
-        else:
-            return 0, 'violation -> crash'
-
-    # Compare actual vs expected
-    if expected_verdict == ExpectedVerdict.SAFE:
-        if actual_verdict == Verdict.SAFE:
-            return 2, 'safe -> safe'
-        elif actual_verdict == Verdict.VIOLATION:
-            return -16, 'safe -> violation'
-        elif actual_verdict == Verdict.UNKNOWN:
-            return 0, 'safe -> unknown'
-        elif actual_verdict == Verdict.NO_SYMBOLIC_VARS:
-            return 0, 'safe -> non-symbolic'
-    else:  # expected_verdict == ExpectedVerdict.VIOLATION
-        if actual_verdict == Verdict.SAFE:
-            return -32, 'violation -> safe'
-        elif actual_verdict == Verdict.VIOLATION:
-            return 1, 'violation -> violation'
-        elif actual_verdict == Verdict.UNKNOWN:
-            return 0, 'violation -> unknown'
-        elif actual_verdict == Verdict.NO_SYMBOLIC_VARS:
-            return 0, 'violation -> non-symbolic'
-
-    # Shouldn't reach here, but handle gracefully
-    return 0, 'unknown'
-
-def target_execution(ver_task: VerificationTask) -> tuple[Path, str, int, ExecutionStatus, bool, Optional[bool], float]:
-    """
-    Execute a verification task and return results including execution time.
-
-    Returns:
-        Tuple of (target, case, points, execution_status, error, validated, elapsed_time_seconds)
-    """
-    command = ver_task['command']
-    if command is None:
-        raise ValueError(f"No command found for verification task: {ver_task['file_path']}")
-
-    target = command["target"]
-    ci_print(f'::group:: Executing target: {target} ({ver_task["category"].value}) ------')
-    log_dir = command["log_dir"]
-    reset_log_dir(log_dir)
-    cmd = command["command"]
-    validated = None
-
-    start_time = time.perf_counter()
-
-    with pushd(log_dir):
-        execution_status, output = run_command_with_timeout(cmd)
-        log_output(output)
-        error: bool = check_for_dse_error(output)
-        points, case = determine_result(output, ver_task['category'], ver_task['verdict'])
-
-        # Store result in the verification task
-        ver_task['result'] = {
-            'points': points,
-            'case': case
-        }
-
-        # ToDo: add witness validation
-        if 'violation' in case:
-            validated = generate_and_validate_witness(ver_task, output)
-
-    elapsed_time = time.perf_counter() - start_time
-
-    logger.info(f"{ver_task['category'].value} | Points: {points}, Case: {case}, Execution Status: {execution_status}, Error: {error}, Validated: {validated}, Time: {elapsed_time:.2f}s")
-
-    ci_print(f"::endgroup::")
-    return target, case, points, execution_status, error, validated, elapsed_time
-
-def check_for_dse_error(output: List[str]) -> bool:
-    for line in output:
-        if "SWAT Assertion failed" in line:
-            return True
-    return False
-
-
-
-def log_output(output: List[str]):
-    for line in output:
-        logger.info(line.strip())
-
-def run_command_with_timeout(cmd: list[str], timeout: int = 90) -> tuple[ExecutionStatus, list[str]]:
-    """Executes the given command and returns output from both STDOUT and STDERR."""
-
-    logger.info(f'[TARGET EXECUTION]: Running symbolic-explorer: {cmd}')
-    output = []
-    with subprocess.Popen(
-            cmd,
-            stdout=subprocess.PIPE,
-            stderr=subprocess.STDOUT,
-            universal_newlines=True,
-            bufsize=1
-    ) as proc:
-        try:
-            # 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()
-            output = [str(e)]
-            return ExecutionStatus.ERROR, output + [str(e)]
-
- 
-
-def run_parallel(ver_tasks: list[VerificationTask], max_workers: int=50):
-    max_workers = min(max_workers, len(ver_tasks))
-
-    logger.info(f"Running parallel target execution with {max_workers} workers...")
-
-    results = {}
-    for category in VerificationCategory:
-        results[category.value] = {}
-
-    total_start_time = time.perf_counter()
-
-    with concurrent.futures.ThreadPoolExecutor(max_workers=max_workers) as executor:
-        # Create a mapping from futures to their corresponding tasks
-        future_to_task = {}
-        for ver_task in ver_tasks:
-            future = executor.submit(target_execution, ver_task)
-            future_to_task[future] = ver_task
-
-        for future in concurrent.futures.as_completed(future_to_task): # type: ignore
-            try:
-                # Get the task associated with this future
-                ver_task = future_to_task[future]
-                target, case, points, execution_status, error, validated, elapsed_time = future.result()
-                logger.info(f"{ver_task['category'].value} | Points: {points}, Case: {case}, Execution Status: {execution_status}, Error: {error}, Validated: {validated}, Time: {elapsed_time:.2f}s")
-
-                results[ver_task['category'].value][target] = (case, points, execution_status.value, error, validated, elapsed_time)
-            except Exception as e:
-                logger.error(f'Exception occurred: {e}')
-
-    total_elapsed_time = time.perf_counter() - total_start_time
-    logger.info(f"Total parallel execution time: {total_elapsed_time:.2f}s")
-
-    evaluate_results(results)
-
-def evaluate_results(results):
-    """Evaluate results with per-category statistics including timing."""
-    total_points = 0
-    category_stats = {}
-    all_times = []  # Collect all execution times for histogram
-
-    # Initialize per-category stats
-    for category_name in results.keys():
-        category_stats[category_name] = {
-            'points': 0,
-            'case_occurrences': {},
-            'execution_statuses': {},
-            'dse_errors': 0,
-            'witness_stats': {},
-            'timing': {
-                'times': [],
-                'min': None,
-                'max': None,
-                'mean': None,
-                'median': None,
-                'total': 0
-            }
-        }
-
-    # Process each category's results
-    for category_name, category_results in results.items():
-        category_points = 0
-        category_times = []
-
-        for target, result_tuple in category_results.items():
-            # Handle both old format (5 elements) and new format (6 elements with timing)
-            if len(result_tuple) == 6:
-                case, points, execution_status, error, validated, elapsed_time = result_tuple
-            else:
-                case, points, execution_status, error, validated = result_tuple
-                elapsed_time = 0.0
-
-            # Update category stats
-            category_points += points
-            category_times.append(elapsed_time)
-            all_times.append((category_name, target, elapsed_time))
-
-            stats = category_stats[category_name]
-
-            if case in stats['case_occurrences']:
-                stats['case_occurrences'][case] += 1
-            else:
-                stats['case_occurrences'][case] = 1
-
-            if execution_status in stats['execution_statuses']:
-                stats['execution_statuses'][execution_status] += 1
-            else:
-                stats['execution_statuses'][execution_status] = 1
-
-            if error:
-                stats['dse_errors'] += 1
-
-            if validated in stats['witness_stats']:
-                stats['witness_stats'][validated] += 1
-            else:
-                stats['witness_stats'][validated] = 1
-
-            logger.info(f"[{category_name}] Target: {target}, Execution Status: {execution_status}, Case: {case}, Points: {points}, Error: {error}, Validated: {validated}, Time: {elapsed_time:.2f}s")
-
-        # Calculate timing statistics for this category
-        if category_times:
-            stats = category_stats[category_name]
-            stats['timing']['times'] = category_times
-            stats['timing']['min'] = min(category_times)
-            stats['timing']['max'] = max(category_times)
-            stats['timing']['mean'] = sum(category_times) / len(category_times)
-            stats['timing']['total'] = sum(category_times)
-            sorted_times = sorted(category_times)
-            mid = len(sorted_times) // 2
-            stats['timing']['median'] = sorted_times[mid] if len(sorted_times) % 2 else (sorted_times[mid-1] + sorted_times[mid]) / 2
-
-        category_stats[category_name]['points'] = category_points
-        total_points += category_points
-
-        logger.info(f"\n[{category_name}] Category Points: {category_points}")
-        logger.info(f"[{category_name}] Case occurrences: {category_stats[category_name]['case_occurrences']}")
-        logger.info(f"[{category_name}] Execution statuses: {category_stats[category_name]['execution_statuses']}")
-        logger.info(f"[{category_name}] DSE errors: {category_stats[category_name]['dse_errors']}")
-        logger.info(f"[{category_name}] Witness stats: {category_stats[category_name]['witness_stats']}")
-
-        # Log timing stats
-        timing = category_stats[category_name]['timing']
-        if timing['min'] is not None:
-            logger.info(f"[{category_name}] Timing: min={timing['min']:.2f}s, max={timing['max']:.2f}s, mean={timing['mean']:.2f}s, median={timing['median']:.2f}s, total={timing['total']:.2f}s")
-
-    logger.info(f"\n{'='*50}")
-    logger.info(f"TOTAL POINTS (ALL CATEGORIES): {total_points}")
-    logger.info(f"{'='*50}")
-
-    # Print overall timing summary
-    if all_times:
-        all_elapsed = [t[2] for t in all_times]
-        logger.info(f"Overall timing: min={min(all_elapsed):.2f}s, max={max(all_elapsed):.2f}s, mean={sum(all_elapsed)/len(all_elapsed):.2f}s")
-
-    save_results(category_stats, results)
-
-    # Generate timing histogram
-    generate_timing_histogram(category_stats, results)
-
-    summary_path = os.getenv("GITHUB_STEP_SUMMARY")
-    if summary_path is not None:
-        print_github_ci(total_points, category_stats, results)
-
-    return total_points
-
-
-def generate_timing_histogram(category_stats, results, folder='results'):
-    """Generate histogram(s) of execution times using matplotlib."""
-    if not MATPLOTLIB_AVAILABLE:
-        logger.warning("matplotlib not available, skipping histogram generation. Install with: pip install matplotlib numpy")
-        return
-
-    folder = os.path.join(SCRIPT_DIR, '..', folder)
-    if not os.path.exists(folder):
-        os.makedirs(folder)
-
-    timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S")
-
-    # Collect all times across categories
-    all_times = []
-    category_times_dict = {}
-
-    for category_name, stats in category_stats.items():
-        times = stats['timing'].get('times', [])
-        if times:
-            category_times_dict[category_name] = times
-            all_times.extend(times)
-
-    if not all_times:
-        logger.info("No timing data available for histogram generation")
-        return
-
-    # Create figure with subplots
-    num_categories = len(category_times_dict)
-    fig_height = 4 + (num_categories * 3)  # Dynamic height based on categories
-    fig, axes = plt.subplots(num_categories + 1, 1, figsize=(12, fig_height))
-
-    if num_categories == 0:
-        axes = [axes]
-    elif num_categories == 1:
-        axes = [axes[0], axes[1]]
-
-    # Overall histogram
-    ax_overall = axes[0]
-    all_times_array = np.array(all_times)
-
-    # Use log scale bins if there's wide variation
-    if max(all_times) > 10 * min(all_times) and min(all_times) > 0:
-        bins = np.logspace(np.log10(max(0.1, min(all_times))), np.log10(max(all_times) + 0.1), 30)
-        ax_overall.set_xscale('log')
-    else:
-        bins = 30
-
-    ax_overall.hist(all_times_array, bins=bins, edgecolor='black', alpha=0.7, color='steelblue')
-    ax_overall.axvline(np.mean(all_times_array), color='red', linestyle='--', linewidth=2, label=f'Mean: {np.mean(all_times_array):.2f}s')
-    ax_overall.axvline(np.median(all_times_array), color='green', linestyle='--', linewidth=2, label=f'Median: {np.median(all_times_array):.2f}s')
-    ax_overall.set_xlabel('Execution Time (seconds)')
-    ax_overall.set_ylabel('Frequency')
-    ax_overall.set_title(f'Overall Execution Time Distribution (n={len(all_times)})')
-    ax_overall.legend()
-    ax_overall.grid(True, alpha=0.3)
-
-    # Add text box with statistics
-    stats_text = f'Min: {min(all_times):.2f}s\nMax: {max(all_times):.2f}s\nMean: {np.mean(all_times_array):.2f}s\nMedian: {np.median(all_times_array):.2f}s\nTotal: {sum(all_times):.2f}s'
-    ax_overall.text(0.98, 0.95, stats_text, transform=ax_overall.transAxes, fontsize=9,
-                    verticalalignment='top', horizontalalignment='right',
-                    bbox=dict(boxstyle='round', facecolor='wheat', alpha=0.5))
-
-    # Per-category histograms
-    colors = plt.cm.Set2(np.linspace(0, 1, num_categories))  # type: ignore
-    for idx, (category_name, times) in enumerate(category_times_dict.items()):
-        ax = axes[idx + 1]
-        times_array = np.array(times)
-
-        # Use same binning logic
-        if max(times) > 10 * min(times) and min(times) > 0:
-            cat_bins = np.logspace(np.log10(max(0.1, min(times))), np.log10(max(times) + 0.1), 25)
-            ax.set_xscale('log')
-        else:
-            cat_bins = 25
-
-        ax.hist(times_array, bins=cat_bins, edgecolor='black', alpha=0.7, color=colors[idx])
-        ax.axvline(np.mean(times_array), color='red', linestyle='--', linewidth=2, label=f'Mean: {np.mean(times_array):.2f}s')
-        ax.axvline(np.median(times_array), color='green', linestyle='--', linewidth=2, label=f'Median: {np.median(times_array):.2f}s')
-        ax.set_xlabel('Execution Time (seconds)')
-        ax.set_ylabel('Frequency')
-        ax.set_title(f'{category_name} Execution Time Distribution (n={len(times)})')
-        ax.legend()
-        ax.grid(True, alpha=0.3)
-
-        # Add stats box
-        cat_stats_text = f'Min: {min(times):.2f}s\nMax: {max(times):.2f}s\nMean: {np.mean(times_array):.2f}s\nMedian: {np.median(times_array):.2f}s'
-        ax.text(0.98, 0.95, cat_stats_text, transform=ax.transAxes, fontsize=9,
-                verticalalignment='top', horizontalalignment='right',
-                bbox=dict(boxstyle='round', facecolor='wheat', alpha=0.5))
-
-    plt.tight_layout()
-
-    # Save histogram
-    histogram_path = os.path.join(folder, f'timing_histogram_{timestamp}.png')
-    plt.savefig(histogram_path, dpi=150, bbox_inches='tight')
-    plt.close()
-    logger.info(f"Timing histogram saved to: {histogram_path}")
-
-    # Also generate a box plot for comparison
-    if num_categories > 1:
-        fig2, ax2 = plt.subplots(figsize=(10, 6))
-        box_data = [times for times in category_times_dict.values()]
-        box_labels = list(category_times_dict.keys())
-
-        bp = ax2.boxplot(box_data, labels=box_labels, patch_artist=True)
-        for patch, color in zip(bp['boxes'], colors):
-            patch.set_facecolor(color)
-
-        ax2.set_ylabel('Execution Time (seconds)')
-        ax2.set_title('Execution Time Comparison by Category')
-        ax2.grid(True, alpha=0.3, axis='y')
-
-        # Rotate labels if they're long
-        plt.xticks(rotation=45, ha='right')
-        plt.tight_layout()
-
-        boxplot_path = os.path.join(folder, f'timing_boxplot_{timestamp}.png')
-        plt.savefig(boxplot_path, dpi=150, bbox_inches='tight')
-        plt.close()
-        logger.info(f"Timing boxplot saved to: {boxplot_path}")
-
-
-def save_results(category_stats, results, folder='results'):
-    """Save results with one JSON file per category, including timing data."""
-    folder = os.path.join(SCRIPT_DIR, '..', folder)
-
-    if not os.path.exists(folder):
-        os.makedirs(folder)
-
-    timestamp = datetime.datetime.now().strftime("%Y%m%d_%H%M%S")
-
-    # Save one file per category
-    for category_name, stats in category_stats.items():
-        # Convert Path keys to strings for JSON serialization
-        category_results = results[category_name]
-        results_serializable = {str(k): v for k, v in category_results.items()}
-
-        # Prepare timing stats (exclude raw times array for cleaner JSON)
-        timing_stats = {
-            'min': stats['timing'].get('min'),
-            'max': stats['timing'].get('max'),
-            'mean': stats['timing'].get('mean'),
-            'median': stats['timing'].get('median'),
-            'total': stats['timing'].get('total'),
-            'count': len(stats['timing'].get('times', []))
-        }
-
-        data = {
-            'category': category_name,
-            'points': stats['points'],
-            'case_occurrences': stats['case_occurrences'],
-            'execution_statuses': stats['execution_statuses'],
-            'dse_errors': stats['dse_errors'],
-            'witness_stats': stats['witness_stats'],
-            'timing': timing_stats,
-            'results': results_serializable
-        }
-
-        filename = f"results_{category_name}_{timestamp}.json"
-        filepath = os.path.join(folder, filename)
-
-        with open(filepath, 'w') as f:
-            json.dump(data, f, indent=4)
-
-        logger.info(f"[{category_name}] Results saved to {filepath}")
-
-
-def print_github_ci(total_points, category_stats, results):
-    """Print GitHub CI summary with per-category breakdown."""
-    def bool_to_emoji(value):
-        if value is None:
-            return "❌"
-        return "✅" if value else "❌"
-
-    summary_path = os.getenv("GITHUB_STEP_SUMMARY")
-    if summary_path is None:
-        raise EnvironmentError("GITHUB_STEP_SUMMARY is not set. Are you running inside GitHub Actions?")
-
-    with open(summary_path, "a") as f:
-        # Header
-        f.write("## 🧾 Symbolic Execution Summary\n\n")
-        f.write(f"**Total Points (All Categories):** `{total_points}`\n\n")
-
-        # Per-Category Summary
-        f.write("### 📊 Points by Category\n")
-        f.write("| Category | Points |\n")
-        f.write("|----------|--------|\n")
-        for category_name, stats in category_stats.items():
-            f.write(f"| {category_name} | {stats['points']} |\n")
-        f.write("\n")
-
-        # Detailed breakdown per category
-        for category_name, stats in category_stats.items():
-            f.write(f"## {category_name}\n\n")
-
-            # Case Occurrences
-            if stats['case_occurrences']:
-                f.write("### 📊 Case Occurrences\n")
-                f.write("| Case | Count |\n")
-                f.write("|------|-------|\n")
-                for k, v in stats['case_occurrences'].items():
-                    f.write(f"| {k} | {v} |\n")
-                f.write("\n")
-
-            # Execution Statuses
-            if stats['execution_statuses']:
-                f.write("### ⚙️ Execution Statuses\n")
-                f.write("| Status | Count |\n")
-                f.write("|--------|-------|\n")
-                for k, v in stats['execution_statuses'].items():
-                    f.write(f"| {k} | {v} |\n")
-                f.write("\n")
-
-            # DSE Errors
-            f.write(f"**DSE Errors:** `{stats['dse_errors']}`\n\n")
-
-            # Timing Stats
-            timing = stats.get('timing', {})
-            if timing.get('min') is not None:
-                f.write("### ⏱️ Timing Statistics\n")
-                f.write("| Metric | Value |\n")
-                f.write("|--------|-------|\n")
-                f.write(f"| Min | {timing['min']:.2f}s |\n")
-                f.write(f"| Max | {timing['max']:.2f}s |\n")
-                f.write(f"| Mean | {timing['mean']:.2f}s |\n")
-                f.write(f"| Median | {timing['median']:.2f}s |\n")
-                f.write(f"| Total | {timing['total']:.2f}s |\n")
-                f.write("\n")
-
-            # Witness Stats
-            if stats['witness_stats'] and any(stats['witness_stats'].values()):
-                f.write("### 🧷 Witness Stats\n")
-                f.write("| Validated | Count |\n")
-                f.write("|-----------|-------|\n")
-                for validated, count in stats['witness_stats'].items():
-                    f.write(f"| {bool_to_emoji(validated)} | {count} |\n")
-                f.write("\n")
-
-
-def select_target(ver_tasks: list[VerificationTask], target_name: str) -> Optional[VerificationTask]:
-    """Select a verification task by target name."""
-    for ver_task in ver_tasks:
-        command = ver_task.get('command')
-        if command and str(command['target']) == target_name:
-            return ver_task
-    return None
-
-
-def run_single_target(ver_tasks: list[VerificationTask]):
-    target = "autostub/Boolean_public_static_int_java_lang_Boolean_compare_boolean_boolean"
-
-    ver_task = select_target(ver_tasks, target)
-    if ver_task is None:
-        logger.error(f"Target {target} not found.")
-        return
-    logger.info(f"Running single target: {target}")
-    ver_task["command"]["log_dir"] = Path(str(ver_task["command"]["log_dir"]).replace('/logs/', '/logs-debug/')) # type: ignore
-    target_execution(ver_task)
-
-
-
-if __name__ == "__main__":
-    mode = Mode.PARALLEL  # Mode.SINGLE_TARGET
-
-    # Configure which properties/categories to run (None = all)
-    selected_categories = [
-        VerificationCategory.VALID_ASSERT_PRP,
-        #VerificationCategory.NO_RUNTIME_EXCEPTION_PRP
-    ]
-
-    logger.info(f"Running target execution script in {mode.value} mode...")
-    test_dir = SCRIPT_DIR.parent / "sv-benchmarks"
-    logger.info(f"Base directory: {test_dir}")
-    ver_tasks: list[VerificationTask] = extract_testcases(test_dir)
-    logger.info(f"Extracted {len(ver_tasks)} test cases.")
-
-    # Filter by selected categories if specified
-    if selected_categories is not None: # type: ignore
-        ver_tasks = [task for task in ver_tasks if task['category'] in selected_categories]
-        logger.info(f"Filtered to {len(ver_tasks)} test cases for categories: {[c.value for c in selected_categories]}")
-
-    if mode == Mode.SINGLE_TARGET: # type: ignore
-        config_file = "swat-debug.cfg"
-    elif mode == Mode.PARALLEL:
-        config_file = "sv-comp.cfg"
-    else:
-        raise ValueError(f"Invalid mode: {mode}")
-    ver_tasks_with_commands = generate_commands(ver_tasks, config_file)#[:10]
-    logger.info(f"Generated {len(ver_tasks_with_commands)} commands.")
-
-    # Check port availability before starting tests (sanity check)
-    # Note: Command generation already skips occupied ports, but this serves as a final validation
-    ports_available, occupied_ports = check_port_availability(ver_tasks_with_commands)
-    if not ports_available:
-        logger.warning(f"WARNING: {len(occupied_ports)} ports became occupied between command generation and execution.")
-        logger.warning(f"Occupied ports: {occupied_ports}")
-        logger.warning("This may cause some tests to fail. Consider restarting the script.")
-
-    if mode == Mode.SINGLE_TARGET: # type: ignore
-        run_single_target(ver_tasks_with_commands)
-    elif mode == Mode.PARALLEL:
-        run_parallel(ver_tasks_with_commands)
-    else:
-        raise ValueError(f"Invalid mode: {mode}")
-
-    logger.info("Done.")
-
diff --git a/targets/sv-comp/scripts/target_selection.py b/targets/sv-comp/scripts/target_selection.py
deleted file mode 100644
index a72fa95..0000000
--- a/targets/sv-comp/scripts/target_selection.py
+++ /dev/null
@@ -1,90 +0,0 @@
-from typing import Any
-from collections import defaultdict
-import yaml
-import logging
-from pathlib import Path
-from pprint import pformat
-from dtypes import ExpectedVerdict, VerificationCategory, VerificationTask
-
-logging.basicConfig(level=logging.INFO)
-logger = logging.getLogger(__name__)
-
-SCRIPT_DIR = Path(__file__).resolve().parent
-
-def validate_property_file_format(data: dict[str, Any]) -> bool:
-    # Validate the structure
-    return (
-        "format_version" in data and data["format_version"] == "2.0" and
-        "input_files" in data and isinstance(data["input_files"], list) and
-        "properties" in data and isinstance(data["properties"], list) and
-        len(data["properties"]) >= 1 and # type: ignore
-        "property_file" in data["properties"][0] and "expected_verdict" in data["properties"][0] and
-        "options" in data and "language" in data["options"] and data["options"]["language"] == "Java"
-    )
-
-def extract_testcases(path: Path) -> list[VerificationTask]:
-    ver_tasks: list[VerificationTask] = []
-
-    # Use Path.rglob to recursively find all YAML files
-    yaml_files = [*path.rglob("*.yml"), *path.rglob("*.yaml")]
-    for file_path in yaml_files:
-        logger.debug(f"Loading YAML file: {file_path}")
-        with open(file_path, 'r') as f:
-            try:
-                data: dict[str, Any] = yaml.safe_load(f)
-            except yaml.YAMLError as e:
-                raise ValueError(f"Error parsing YAML file {file_path}: {e}")
-
-            if not validate_property_file_format(data):
-                raise ValueError(f"Invalid format in YAML file: {file_path}")
-
-            for property in data["properties"]:
-                ver_task: VerificationTask = {
-                    'category': VerificationCategory(property['property_file'].split('/')[-1]),
-                    'verdict': ExpectedVerdict(property['expected_verdict']),
-                    'file_path': file_path,
-                    'input_files': data["input_files"],
-                    'command': None,
-                    'result': None
-                }
-                ver_tasks.append(ver_task)
-
-            logger.debug(f"Loaded test case: {file_path}")
-
-    return ver_tasks
-
-
-def print_testcase_statistics(ver_tasks: list[VerificationTask]) -> None:
-    """Print concise statistics about test cases by category."""
-    # Count verdicts for each category using nested defaultdict
-    stats: defaultdict[VerificationCategory, defaultdict[ExpectedVerdict, int]] = defaultdict(lambda: defaultdict(int))
-
-    for task in ver_tasks:
-        stats[task['category']][task['verdict']] += 1
-
-    logger.info(f"{'='*60}")
-    logger.info(f"Test Case Statistics (Total: {len(ver_tasks)})")
-    logger.info(f"{'='*60}")
-    logger.info(f"{'Property':<30} {'Safe':<10} {'Violation':<10}")
-    logger.info(f"{'-'*60}")
-
-    for category in VerificationCategory:
-        safe_count = stats[category][ExpectedVerdict.SAFE]
-        violation_count = stats[category][ExpectedVerdict.VIOLATION]
-        logger.info(f"{category.value:<30} {safe_count:<10} {violation_count:<10}")
-
-    logger.info(f"{'='*60}")
-
-
-if __name__ == "__main__":
-    logger.info("Testing testcase extraction script...")
-    test_dir = (SCRIPT_DIR / ".." / "sv-benchmarks").resolve()
-    logger.info(f"Base directory: {test_dir}")
-    test_cases = extract_testcases(test_dir)
-    logger.info(f"Loaded {len(test_cases)} test cases from directory: {test_dir}")
-
-    print_testcase_statistics(test_cases)
-
-    logger.info("\nFirst 3 test cases:")
-    for i, case in enumerate(test_cases[:3], 1):
-        logger.info(f"\nTest Case {i}:\n{pformat(dict(case), width=100)}")
\ No newline at end of file
diff --git a/targets/sv-comp/scripts/util.py b/targets/sv-comp/scripts/util.py
deleted file mode 100644
index f88041e..0000000
--- a/targets/sv-comp/scripts/util.py
+++ /dev/null
@@ -1,10 +0,0 @@
-import os
-from typing import Any
-
-
-IS_RUNNING_IN_CI: bool = os.getenv("CI", "false") == "true"
-
-def ci_print(message: Any) -> None:
-    """Print a message formatted for CI systems."""
-    if IS_RUNNING_IN_CI:
-        print(f"{message}")
\ No newline at end of file
diff --git a/targets/sv-comp/scripts/witness_validation.py b/targets/sv-comp/scripts/witness_validation.py
deleted file mode 100644
index 158821b..0000000
--- a/targets/sv-comp/scripts/witness_validation.py
+++ /dev/null
@@ -1,187 +0,0 @@
-import base64
-from contextlib import contextmanager
-import os
-import enum
-import logging
-import shutil
-import subprocess
-from typing import List, Optional
-from pathlib import Path
-from dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command
-
-logger = logging.getLogger(__name__)
-SCRIPT_DIR = Path(__file__).resolve().parent
-WITNESS_CREATION_PATH = (SCRIPT_DIR.parent / 'WitnessCreator' / 'build' / 'libs' / 'WitnessCreator.jar')
-WITNESS_VALIDATION_PATH = (SCRIPT_DIR.parent / 'wit4java' / 'bin' / 'wit4java')
-
-class ExecutionStatus(enum.Enum):
-    SUCCESS = "success"
-    ERROR = "error"
-    TIMEOUT = "timeout"
-
-
-
-def generate_and_validate_witness(ver_task: VerificationTask, output: List[str]) -> Optional[bool]:
-    """Extract witnesses from `output`, create witness files and validate them.
-
-    Returns True/False on validation result or None if no witness was found.
-    """
-    # 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
-
-    witness_dir = assemble_files(info)
-    logger.info("Generating witness files")
-    generate_witness(witness_dir, "\n".join(witnesses))
-    logger.info("Validating witness")
-    return validate_witness(info)
-
-
-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."""
-    cmd: List[str] = [str(WITNESS_VALIDATION_PATH), '--packages']
-    main_folder = ''
-
-    # find classpath entries (items after --classpath)
-    try:
-        classpath_index = info['command'].index('--classpath')
-        classpath_entries = info['command'][classpath_index + 1:]
-    except ValueError:
-        classpath_entries = []
-
-    for folder in classpath_entries:
-        try:
-            if 'Main.java' in os.listdir(folder):
-                main_folder = folder
-            else:
-                cmd.append(folder)
-        except Exception:
-            # ignore non-folders or missing paths
-            continue
-
-    cmd.extend(['--witness', str(Path(info['log_dir']) / 'witness' / 'witness.graphml')])
-    if main_folder:
-        cmd.append(main_folder)
-
-    _, output = run_command_with_timeout(cmd)
-    logger.info("Witness Validation Output")
-    log_output(output)
-    for line in output:
-        if "wit4java: Witness Correct" in line:
-            return True
-    return False
-        
-    
-@contextmanager
-def pushd(dirname):
-    """Context manager to temporarily change the working directory."""
-    original_dir = os.getcwd()
-    logger.info(f"Changing directory to: {dirname}")
-    os.chdir(dirname)
-    try:
-        yield
-    finally:
-        os.chdir(original_dir)
-
-
-
-def extract_last_round(out: List[str], marker: str = "============================== ROUND") -> str:
-    return "\n".join(out).split(marker)[-1]
-
-
-
-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 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)
-
-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."""
-
-    logger.info(f'[WITNESS] Running: {cmd}')
-    output = []
-    with subprocess.Popen(
-            cmd,
-            stdout=subprocess.PIPE,
-            stderr=subprocess.STDOUT,
-            universal_newlines=True,
-            bufsize=1
-    ) as proc:
-        try:
-            # 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()
-            output = [str(e)]
-            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