From 8aa954fca84bc9a5920e5025b98c88309dd1517c Mon Sep 17 00:00:00 2001
From: Nico Winkel <71224607+k0lja@users.noreply.github.com>
Date: Fri, 19 Jun 2026 13:38:43 +0200
Subject: [PATCH 01/12] added sv-comp zip ci

---
 .github/workflows/gradle.yml                  |  61 ++++-
 scripts/package-svcomp.sh                     | 170 +++++++++++++
 scripts/svcomp-package/README.md              |  19 ++
 scripts/svcomp-package/compile-target.sh      |  35 +++
 scripts/svcomp-package/run-swat.sh            |  66 +++++
 scripts/svcomp-package/run_swat.py            | 235 ++++++++++++++++++
 scripts/svcomp-package/smoketest.sh           |  12 +
 scripts/svcomp-package/smoketest/Main.java    |  10 +
 .../smoketest/common/Verifier.java            |  60 +++++
 9 files changed, 667 insertions(+), 1 deletion(-)
 create mode 100755 scripts/package-svcomp.sh
 create mode 100644 scripts/svcomp-package/README.md
 create mode 100755 scripts/svcomp-package/compile-target.sh
 create mode 100755 scripts/svcomp-package/run-swat.sh
 create mode 100755 scripts/svcomp-package/run_swat.py
 create mode 100755 scripts/svcomp-package/smoketest.sh
 create mode 100644 scripts/svcomp-package/smoketest/Main.java
 create mode 100644 scripts/svcomp-package/smoketest/common/Verifier.java

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 138dd91..a9705ee 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -3,12 +3,17 @@ 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:
     runs-on: ubuntu-latest
     permissions:
-      contents: read
+      contents: write
     steps:
     - uses: actions/checkout@v5
     - name: Set up JDK 17
@@ -20,6 +25,60 @@ jobs:
       uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
     - name: Build
       run: ./gradlew build -x test
+    - name: Build SV-COMP JAR artifacts
+      if: github.event_name != 'pull_request'
+      run: ./gradlew --no-daemon :symbolic-executor:copyJar :targets:sv-comp:WitnessCreator:shadowJar
+    - name: Set SV-COMP package metadata
+      id: svcomp_metadata
+      if: github.event_name != 'pull_request'
+      run: |
+        if [[ "${GITHUB_REF_TYPE}" == "tag" ]]; then
+          version="${GITHUB_REF_NAME}"
+        else
+          version="${GITHUB_SHA::7}"
+        fi
+
+        artifact_name="swat-svcomp-${version}"
+        zip_name="${artifact_name}.zip"
+
+        echo "artifact-name=${artifact_name}" >> "${GITHUB_OUTPUT}"
+        echo "version=${version}" >> "${GITHUB_OUTPUT}"
+        echo "zip-name=${zip_name}" >> "${GITHUB_OUTPUT}"
+    - name: Download SV-COMP reference runtime
+      if: github.event_name != 'pull_request'
+      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
+      if: github.event_name != 'pull_request'
+      env:
+        SWAT_SVCOMP_VERSION: ${{ steps.svcomp_metadata.outputs.version }}
+        SWAT_SVCOMP_REFERENCE_DIR: ${{ runner.temp }}/swat-reference/swat-verify
+      run: scripts/package-svcomp.sh
+    - name: Upload SV-COMP ZIP artifact
+      if: github.event_name != 'pull_request'
+      uses: actions/upload-artifact@v4
+      with:
+        name: ${{ steps.svcomp_metadata.outputs.artifact-name }}
+        path: build/distributions/${{ steps.svcomp_metadata.outputs.zip-name }}
+        if-no-files-found: error
+    - name: Create or update GitHub release
+      if: github.event_name == 'push' && startsWith(github.ref, 'refs/tags/')
+      env:
+        GH_TOKEN: ${{ github.token }}
+        ZIP_NAME: ${{ steps.svcomp_metadata.outputs.zip-name }}
+      run: |
+        tag="${GITHUB_REF_NAME}"
+        zip_path="build/distributions/${ZIP_NAME}"
+
+        if gh release view "${tag}" > /dev/null 2>&1; then
+          gh release upload "${tag}" "${zip_path}" --clobber
+        else
+          gh release create "${tag}" "${zip_path}" \
+            --title "SWAT ${tag}" \
+            --notes "Automated SWAT SV-COMP package."
+        fi
 
   test:
     needs: build
diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh
new file mode 100755
index 0000000..8628ebd
--- /dev/null
+++ b/scripts/package-svcomp.sh
@@ -0,0 +1,170 @@
+#!/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 only for
+# the pinned SV-COMP Python environment:
+#
+# - .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)}"
+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"
+}
+
+repo_file() {
+  local rel="$1"
+  local path="${ROOT_DIR}/${rel}"
+  [[ -f "$path" ]] || fail "missing repository 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"
+
+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
+copy_artifact_file \
+  "$(repo_file libs/java-library-path/java-smt-latest.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..443ca4d
--- /dev/null
+++ b/scripts/svcomp-package/run_swat.py
@@ -0,0 +1,235 @@
+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 = 180) -> tuple[ExecutionStatus, list[str]]:
+    """Executes the given command and returns output from both STDOUT and STDERR."""
+
+    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);
+  }
+}

From 2b6fd70c829c0a86fddcc658ed0957b8e54d66d0 Mon Sep 17 00:00:00 2001
From: Nico Winkel <71224607+k0lja@users.noreply.github.com>
Date: Sat, 20 Jun 2026 07:33:20 +0200
Subject: [PATCH 02/12] fiex java smt jar

---
 scripts/package-svcomp.sh | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh
index 8628ebd..823f28e 100755
--- a/scripts/package-svcomp.sh
+++ b/scripts/package-svcomp.sh
@@ -12,8 +12,8 @@ set -euo pipefail
 # - 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 only for
-# the pinned SV-COMP Python environment:
+# 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/
 #
@@ -50,10 +50,12 @@ artifact_file() {
   printf '%s\n' "$path"
 }
 
-repo_file() {
+reference_file() {
   local rel="$1"
-  local path="${ROOT_DIR}/${rel}"
-  [[ -f "$path" ]] || fail "missing repository file: ${path}"
+  [[ -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"
 }
 
@@ -146,9 +148,8 @@ 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
-copy_artifact_file \
-  "$(repo_file libs/java-library-path/java-smt-latest.jar)" \
-  "$PACKAGE_DIR/libs/java-library-path/java-smt-latest.jar"
+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"
 

From c420233d2f2fbfd6f29246dee60e08bf0164d7e2 Mon Sep 17 00:00:00 2001
From: Nils Loose <44154987+nils-loose@users.noreply.github.com>
Date: Wed, 24 Jun 2026 11:58:57 +0100
Subject: [PATCH 03/12] Add missing step to prepare z3 dependencies

---
 .github/workflows/gradle.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index a9705ee..2d2810b 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -23,6 +23,8 @@ 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
     - name: Build SV-COMP JAR artifacts

From 1d742b1222027e662b4d8be87813e2fb595bcbb1 Mon Sep 17 00:00:00 2001
From: Nils Loose <loose.nils@gmail.com>
Date: Wed, 24 Jun 2026 12:12:09 +0000
Subject: [PATCH 04/12] Split build and pkg task

---
 .github/workflows/gradle.yml | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index a9705ee..8ae44e2 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -13,7 +13,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     permissions:
-      contents: write
+      contents: read
     steps:
     - uses: actions/checkout@v5
     - name: Set up JDK 17
@@ -23,14 +23,32 @@ 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
+
+  package:
+    needs: build
+    if: github.event_name != 'pull_request'
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+    - uses: actions/checkout@v5
+    - name: Set up JDK 17
+      uses: actions/setup-java@v4
+      with:
+        java-version: '17'
+        distribution: 'temurin'
+    - name: Setup Gradle
+      uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
+    - name: Prepare Solver Dependencies
+      run: ./gradlew copyNativeLibs
     - name: Build SV-COMP JAR artifacts
-      if: github.event_name != 'pull_request'
       run: ./gradlew --no-daemon :symbolic-executor:copyJar :targets:sv-comp:WitnessCreator:shadowJar
     - name: Set SV-COMP package metadata
       id: svcomp_metadata
-      if: github.event_name != 'pull_request'
       run: |
         if [[ "${GITHUB_REF_TYPE}" == "tag" ]]; then
           version="${GITHUB_REF_NAME}"
@@ -45,19 +63,16 @@ jobs:
         echo "version=${version}" >> "${GITHUB_OUTPUT}"
         echo "zip-name=${zip_name}" >> "${GITHUB_OUTPUT}"
     - name: Download SV-COMP reference runtime
-      if: github.event_name != 'pull_request'
       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
-      if: github.event_name != 'pull_request'
       env:
         SWAT_SVCOMP_VERSION: ${{ steps.svcomp_metadata.outputs.version }}
         SWAT_SVCOMP_REFERENCE_DIR: ${{ runner.temp }}/swat-reference/swat-verify
       run: scripts/package-svcomp.sh
     - name: Upload SV-COMP ZIP artifact
-      if: github.event_name != 'pull_request'
       uses: actions/upload-artifact@v4
       with:
         name: ${{ steps.svcomp_metadata.outputs.artifact-name }}
@@ -141,4 +156,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

From e634499c035a0ab1151842681e2caf74815cff3b Mon Sep 17 00:00:00 2001
From: Nils Loose <loose.nils@gmail.com>
Date: Wed, 24 Jun 2026 12:49:23 +0000
Subject: [PATCH 05/12] Add release mechanism

---
 .github/workflows/gradle.yml | 135 ++++++++++++++++++++++++++---------
 scripts/package-svcomp.sh    |   9 +++
 2 files changed, 109 insertions(+), 35 deletions(-)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 8ae44e2..994aed3 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -26,42 +26,82 @@ jobs:
     - 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 != 'pull_request'
+    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: Set up JDK 17
-      uses: actions/setup-java@v4
+    - name: Download JARs
+      uses: actions/download-artifact@v4
       with:
-        java-version: '17'
-        distribution: 'temurin'
-    - name: Setup Gradle
-      uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
-    - name: Prepare Solver Dependencies
-      run: ./gradlew copyNativeLibs
-    - name: Build SV-COMP JAR artifacts
-      run: ./gradlew --no-daemon :symbolic-executor:copyJar :targets:sv-comp:WitnessCreator:shadowJar
-    - name: Set SV-COMP package metadata
-      id: svcomp_metadata
+        name: release-jars-${{ github.sha }}
+        path: ${{ runner.temp }}/release-jars
+    - name: Determine release channel
+      id: meta
       run: |
-        if [[ "${GITHUB_REF_TYPE}" == "tag" ]]; then
-          version="${GITHUB_REF_NAME}"
-        else
-          version="${GITHUB_SHA::7}"
+        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
 
-        artifact_name="swat-svcomp-${version}"
-        zip_name="${artifact_name}.zip"
+        # 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 "artifact-name=${artifact_name}" >> "${GITHUB_OUTPUT}"
-        echo "version=${version}" >> "${GITHUB_OUTPUT}"
-        echo "zip-name=${zip_name}" >> "${GITHUB_OUTPUT}"
+        {
+          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}"
@@ -69,30 +109,55 @@ jobs:
         unzip -q "${RUNNER_TEMP}/swat-verify.zip" -d "${RUNNER_TEMP}/swat-reference"
     - name: Pack SV-COMP ZIP
       env:
-        SWAT_SVCOMP_VERSION: ${{ steps.svcomp_metadata.outputs.version }}
+        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: ${{ steps.svcomp_metadata.outputs.artifact-name }}
-        path: build/distributions/${{ steps.svcomp_metadata.outputs.zip-name }}
+        name: swat-svcomp-${{ steps.meta.outputs.version }}
+        path: build/distributions/${{ steps.meta.outputs.zip-name }}
         if-no-files-found: error
-    - name: Create or update GitHub release
-      if: github.event_name == 'push' && startsWith(github.ref, 'refs/tags/')
+    - name: Publish release
+      if: steps.meta.outputs.release == 'true'
       env:
         GH_TOKEN: ${{ github.token }}
-        ZIP_NAME: ${{ steps.svcomp_metadata.outputs.zip-name }}
+        CHANNEL: ${{ steps.meta.outputs.channel }}
+        ZIP_NAME: ${{ steps.meta.outputs.zip-name }}
+        ROLLING: ${{ steps.meta.outputs.rolling }}
+        PRERELEASE: ${{ steps.meta.outputs.prerelease }}
       run: |
-        tag="${GITHUB_REF_NAME}"
         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 gh release view "${tag}" > /dev/null 2>&1; then
-          gh release upload "${tag}" "${zip_path}" --clobber
+        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
-          gh release create "${tag}" "${zip_path}" \
-            --title "SWAT ${tag}" \
-            --notes "Automated SWAT SV-COMP package."
+          # 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:
diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh
index 823f28e..ee8ad2a 100755
--- a/scripts/package-svcomp.sh
+++ b/scripts/package-svcomp.sh
@@ -23,6 +23,9 @@ 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}"
@@ -120,6 +123,12 @@ 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"

From cdf7c4aaaf9fda64721e2884db0ffb7ec8e8010d Mon Sep 17 00:00:00 2001
From: Nils Loose <44154987+nils-loose@users.noreply.github.com>
Date: Wed, 24 Jun 2026 22:09:40 +0100
Subject: [PATCH 06/12] Let SWAT use the full SV-COMP time budget (#32)

SWAT's internal time cutoffs pre-empt it well before benchexec's competition
limit (15 min):

- run_swat.py hard-killed the symbolic-execution run at 180s (the default
  run_command_with_timeout). Default is now None (no internal cutoff);
  benchexec enforces the wall/CPU limit externally.

- the SV-COMP exploration's Z3 solves were capped at 60s. Removed, but ONLY
  for the sv-comp path: Z3Handler.solve / StrategyService.solve_branch now take
  a timeout (default 60s, unchanged for passive/http/target/simple drivers),
  and SVCompDriver / SVCompHandler pass None. solve_with_optimization is left
  as-is (it is not on the sv-comp solve_branch path).

Net: SWAT explores with the full SV-COMP budget; other modes keep their 60s
solver timeout.

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 scripts/svcomp-package/run_swat.py            | 8 ++++++--
 symbolic-explorer/driver/SVCompDriver.py      | 2 +-
 symbolic-explorer/solver/SolverHandler.py     | 5 +++--
 symbolic-explorer/strategy/StrategyService.py | 4 ++--
 symbolic-explorer/svcomp/SVCompHandler.py     | 2 +-
 5 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py
index 443ca4d..6b88333 100755
--- a/scripts/svcomp-package/run_swat.py
+++ b/scripts/svcomp-package/run_swat.py
@@ -53,8 +53,12 @@ def determine_result(output: List[str], property_file: str) -> Verdict:
 
 
 
-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."""
+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 = []
diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py
index a0081e8..67de334 100644
--- a/symbolic-explorer/driver/SVCompDriver.py
+++ b/symbolic-explorer/driver/SVCompDriver.py
@@ -258,7 +258,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"}')
diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py
index dd9a0ee..343d861 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).
 
@@ -432,7 +432,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

From 0e6cad55b4acebe33f9a0227be53ebc269af9f50 Mon Sep 17 00:00:00 2001
From: solid-eureka <119814169+solid-eureka@users.noreply.github.com>
Date: Sun, 28 Jun 2026 09:14:43 +0000
Subject: [PATCH 07/12] Fix StringValue.invokeReplace()

The old version mistakenly modified the 'this' Object, causing unexpected behaviour.
---
 .../uzl/its/swat/symbolic/shadow/Frame.java   | 26 +++++--
 .../value/reference/lang/StringValue.java     | 77 +++++++++++--------
 .../data/BinaryExecutionTree/Tree.py          | 22 +++---
 symbolic-explorer/driver/SVCompDriver.py      |  3 +
 symbolic-explorer/solver/SolverHandler.py     |  2 +
 5 files changed, 77 insertions(+), 53 deletions(-)

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/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-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py
index 6636395..5ee5365 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:
     """
@@ -130,8 +130,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 +142,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 +154,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/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py
index 67de334..19ea7b3 100644
--- a/symbolic-explorer/driver/SVCompDriver.py
+++ b/symbolic-explorer/driver/SVCompDriver.py
@@ -222,6 +222,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:
diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py
index 343d861..471f0f8 100755
--- a/symbolic-explorer/solver/SolverHandler.py
+++ b/symbolic-explorer/solver/SolverHandler.py
@@ -391,6 +391,8 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000)
         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

From 54dd68d454cc8731bf992f30b14d481bdee17cd2 Mon Sep 17 00:00:00 2001
From: solid-eureka <119814169+solid-eureka@users.noreply.github.com>
Date: Tue, 30 Jun 2026 09:58:40 +0000
Subject: [PATCH 08/12] Remove pygraphviz import

---
 symbolic-explorer/data/BinaryExecutionTree/Tree.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/symbolic-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py
index 5ee5365..ad6c2b0 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:
     """

From 5104d5c2e36017b4dec520af8b570ee022ed9c75 Mon Sep 17 00:00:00 2001
From: Nico Winkel <71224607+k0lja@users.noreply.github.com>
Date: Wed, 1 Jul 2026 09:35:05 +0200
Subject: [PATCH 09/12] added venv build process

---
 .github/workflows/gradle.yml            | 22 ++++++++++--------
 scripts/package-svcomp.sh               | 30 +++++++++----------------
 scripts/svcomp-package/requirements.txt | 19 ++++++++++++++++
 scripts/svcomp-package/run-swat.sh      | 12 +++++++---
 4 files changed, 52 insertions(+), 31 deletions(-)
 create mode 100644 scripts/svcomp-package/requirements.txt

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 994aed3..46c92aa 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -6,8 +6,7 @@ on:
   workflow_dispatch:
 
 env:
-  SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content
-  SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6
+  SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64
 
 jobs:
   build:
@@ -49,7 +48,7 @@ jobs:
         github.ref == 'refs/heads/dev' ||
         startsWith(github.ref, 'refs/tags/')
       ))
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     permissions:
       contents: write
     steps:
@@ -102,16 +101,21 @@ jobs:
           echo "rolling=${rolling}"
           echo "prerelease=${prerelease}"
         } >> "${GITHUB_OUTPUT}"
-    - name: Download SV-COMP reference runtime
+    - name: Build SV-COMP Python runtime
+      env:
+        VENV_DIR: ${{ runner.temp }}/svcomp-runtime/${{ env.SVCOMP_VENV_DIR_NAME }}
       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"
+        mkdir -p "$(dirname "${VENV_DIR}")"
+        /usr/bin/python3 -m venv --copies "${VENV_DIR}"
+        "${VENV_DIR}/bin/python3" -m pip install --no-deps -r scripts/svcomp-package/requirements.txt
+        "${VENV_DIR}/bin/python3" -m pip check
+        "${VENV_DIR}/bin/python3" -m pip freeze --all > "${VENV_DIR}/requirements.freeze.txt"
+        "${VENV_DIR}/bin/python3" -c "import fastapi, pydantic, z3"
     - 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_RUNTIME_DIR: ${{ runner.temp }}/svcomp-runtime
         SWAT_SVCOMP_COMMIT: ${{ github.sha }}
         SWAT_SVCOMP_REF: ${{ github.ref_name }}
         SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }}
@@ -221,4 +225,4 @@ jobs:
         java-version: '17'
         distribution: 'temurin'
     - name: Generate and submit dependency graph
-      uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
\ No newline at end of file
+      uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh
index ee8ad2a..accf707 100755
--- a/scripts/package-svcomp.sh
+++ b/scripts/package-svcomp.sh
@@ -11,13 +11,12 @@ set -euo pipefail
 # - 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:
+# Set SWAT_SVCOMP_RUNTIME_DIR to a runtime package root that contains the
+# pinned SV-COMP Python environment:
 #
 # - .venv_ubuntu_24_04_1__x86_64/
 #
-# Z3 is taken from the vendored Linux distribution ZIP in this repository.
+# Z3 and JavaSMT are taken from the vendored files in this repository.
 #
 ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
 cd "$ROOT_DIR"
@@ -32,13 +31,14 @@ 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:-}"
+RUNTIME_DIR="${SWAT_SVCOMP_RUNTIME_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"
+JAVA_SMT_JAR="${ROOT_DIR}/libs/java-library-path/java-smt-latest.jar"
 
-if [[ -n "$REFERENCE_DIR" ]]; then
-  REFERENCE_DIR="$(cd "$REFERENCE_DIR" && pwd)"
+if [[ -n "$RUNTIME_DIR" ]]; then
+  RUNTIME_DIR="$(cd "$RUNTIME_DIR" && pwd)"
 fi
 
 fail() {
@@ -53,15 +53,6 @@ artifact_file() {
   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
@@ -137,6 +128,7 @@ 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 "$SUPPORT_DIR/requirements.txt" "$PACKAGE_DIR/requirements.txt"
 install -m 0644 targets/sv-comp/sv-comp.cfg "$PACKAGE_DIR/sv-comp.cfg"
 
 EXECUTOR_JAR="$(first_artifact_file \
@@ -157,13 +149,13 @@ 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)"
+[[ -f "$JAVA_SMT_JAR" ]] || fail "missing JavaSMT JAR: ${JAVA_SMT_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}"
+[[ -n "$RUNTIME_DIR" ]] || fail "SWAT_SVCOMP_RUNTIME_DIR must point to a runtime package root containing ${VENV_DIR_NAME}"
+copy_artifact_tree "${RUNTIME_DIR}/${VENV_DIR_NAME}" "${PACKAGE_DIR}/${VENV_DIR_NAME}"
 
 mkdir -p "$DIST_DIR"
 ZIP_PATH="${DIST_DIR}/${PACKAGE_NAME}.zip"
diff --git a/scripts/svcomp-package/requirements.txt b/scripts/svcomp-package/requirements.txt
new file mode 100644
index 0000000..5c32b0a
--- /dev/null
+++ b/scripts/svcomp-package/requirements.txt
@@ -0,0 +1,19 @@
+annotated-types==0.7.0
+anyio==4.6.2.post1
+boto==2.49.0
+certifi==2025.11.12
+charset-normalizer==3.4.4
+click==8.1.7
+fastapi==0.115.5
+h11==0.14.0
+idna==3.10
+pydantic==2.10.0
+pydantic_core==2.27.0
+PyYAML==6.0.2
+requests==2.32.5
+sniffio==1.3.1
+starlette==0.41.3
+typing_extensions==4.12.2
+urllib3==2.5.0
+uvicorn==0.32.1
+z3-solver==4.15.4.0
diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh
index fc21ac2..424a318 100755
--- a/scripts/svcomp-package/run-swat.sh
+++ b/scripts/svcomp-package/run-swat.sh
@@ -60,7 +60,13 @@ done
 
 
 SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
-source "$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/activate"
+VENV_PYTHON="$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/python3"
+
+if [ ! -x "$VENV_PYTHON" ]; then
+    echo "Error: Python runtime not found at $VENV_PYTHON"
+    exit 1
+fi
+
 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
+"$VENV_PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1
+cat out.log

From b5eb2ddee950175d9611eaaa91ed7958c932d13c Mon Sep 17 00:00:00 2001
From: Nico Winkel <71224607+k0lja@users.noreply.github.com>
Date: Wed, 1 Jul 2026 10:03:41 +0200
Subject: [PATCH 10/12] added pr artefact build

---
 .github/workflows/gradle.yml | 43 ++++++++++++++++++++++++++++--------
 1 file changed, 34 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 46c92aa..8d08a93 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -29,7 +29,6 @@ jobs:
     - 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 }}
@@ -42,6 +41,7 @@ jobs:
   package:
     needs: build
     if: >-
+      github.event_name == 'pull_request' ||
       github.event_name == 'workflow_dispatch' ||
       (github.event_name == 'push' && (
         github.ref == 'refs/heads/main' ||
@@ -50,7 +50,13 @@ jobs:
       ))
     runs-on: ubuntu-24.04
     permissions:
-      contents: write
+      contents: read
+    outputs:
+      channel: ${{ steps.meta.outputs.channel }}
+      zip-name: ${{ steps.meta.outputs.zip-name }}
+      rolling: ${{ steps.meta.outputs.rolling }}
+      prerelease: ${{ steps.meta.outputs.prerelease }}
+      artifact-name: ${{ steps.meta.outputs.artifact-name }}
     steps:
     - uses: actions/checkout@v5
     - name: Download JARs
@@ -97,6 +103,7 @@ jobs:
           echo "channel=${channel}"
           echo "version=${version}"
           echo "zip-name=${zip_name}"
+          echo "artifact-name=swat-svcomp-${version}"
           echo "release=${release}"
           echo "rolling=${rolling}"
           echo "prerelease=${prerelease}"
@@ -123,19 +130,37 @@ jobs:
     - name: Upload SV-COMP ZIP artifact
       uses: actions/upload-artifact@v4
       with:
-        name: swat-svcomp-${{ steps.meta.outputs.version }}
+        name: ${{ steps.meta.outputs.artifact-name }}
         path: build/distributions/${{ steps.meta.outputs.zip-name }}
         if-no-files-found: error
+
+  publish-release:
+    needs: package
+    if: >-
+      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:
+    - name: Download SV-COMP ZIP artifact
+      uses: actions/download-artifact@v4
+      with:
+        name: ${{ needs.package.outputs.artifact-name }}
+        path: ${{ runner.temp }}/svcomp-package
     - 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 }}
+        GH_REPO: ${{ github.repository }}
+        CHANNEL: ${{ needs.package.outputs.channel }}
+        ZIP_NAME: ${{ needs.package.outputs.zip-name }}
+        ROLLING: ${{ needs.package.outputs.rolling }}
+        PRERELEASE: ${{ needs.package.outputs.prerelease }}
       run: |
-        zip_path="build/distributions/${ZIP_NAME}"
+        zip_path="${RUNNER_TEMP}/svcomp-package/${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")"
 

From 1fcc7db166cbf262c7ebc1ecba144cbfcebb03d6 Mon Sep 17 00:00:00 2001
From: Nico Winkel <71224607+k0lja@users.noreply.github.com>
Date: Wed, 1 Jul 2026 11:14:11 +0200
Subject: [PATCH 11/12] javasmt fix

---
 .github/workflows/gradle.yml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index 8d08a93..df65972 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -28,6 +28,22 @@ jobs:
       run: ./gradlew --no-daemon build -x test
     - name: Build WitnessCreator JAR
       run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar
+    - name: Collect JavaSMT JAR
+      run: |
+        java_smt_dir="${HOME}/.gradle/caches/modules-2/files-2.1/org.sosy-lab/java-smt"
+        if [[ ! -d "$java_smt_dir" ]]; then
+          echo "JavaSMT Gradle cache directory not found: $java_smt_dir" >&2
+          exit 1
+        fi
+
+        java_smt_jar="$(find "$java_smt_dir" -type f -name 'java-smt-*.jar' ! -name '*-sources.jar' ! -name '*-javadoc.jar' | sort | tail -n 1)"
+        if [[ -z "$java_smt_jar" ]]; then
+          echo "JavaSMT JAR not found in Gradle cache: $java_smt_dir" >&2
+          exit 1
+        fi
+
+        mkdir -p build/svcomp-runtime
+        cp "$java_smt_jar" build/svcomp-runtime/java-smt-latest.jar
     - name: Upload JARs
       uses: actions/upload-artifact@v4
       with:
@@ -35,6 +51,7 @@ jobs:
         path: |
           symbolic-executor/lib/symbolic-executor.jar
           targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar
+          build/svcomp-runtime/java-smt-latest.jar
         if-no-files-found: error
         retention-days: 1
 
@@ -64,6 +81,11 @@ jobs:
       with:
         name: release-jars-${{ github.sha }}
         path: ${{ runner.temp }}/release-jars
+    - name: Install JavaSMT packaging artifact
+      run: |
+        mkdir -p libs/java-library-path
+        cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \
+          libs/java-library-path/java-smt-latest.jar
     - name: Determine release channel
       id: meta
       run: |

From 5095ea40e60f5e0f6aafde284b0a7dfb872ae435 Mon Sep 17 00:00:00 2001
From: Nico Winkel <71224607+k0lja@users.noreply.github.com>
Date: Wed, 1 Jul 2026 12:15:37 +0200
Subject: [PATCH 12/12] Use external WitnessCreator release

---
 .github/workflows/gradle.yml                  |  23 ++-
 scripts/package-svcomp.sh                     |  31 +--
 settings.gradle                               |   3 +-
 targets/sv-comp/WitnessCreator/build.gradle   |  44 -----
 .../WitnessCreator/src/main/java/App.java     | 180 ------------------
 .../main/java/witness/WitnessAssumption.java  |  33 ----
 .../src/main/java/witness/WitnessEdge.java    |  35 ----
 .../src/main/java/witness/WitnessNode.java    |  29 ---
 .../sv-comp/WitnessCreator/witness.graphml    | 134 -------------
 .../witnesses/default_violation.st            |  56 ------
 .../WitnessCreator/witnesses/witness.st       |  70 -------
 11 files changed, 39 insertions(+), 599 deletions(-)
 delete mode 100755 targets/sv-comp/WitnessCreator/build.gradle
 delete mode 100755 targets/sv-comp/WitnessCreator/src/main/java/App.java
 delete mode 100755 targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java
 delete mode 100755 targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java
 delete mode 100755 targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java
 delete mode 100644 targets/sv-comp/WitnessCreator/witness.graphml
 delete mode 100755 targets/sv-comp/WitnessCreator/witnesses/default_violation.st
 delete mode 100755 targets/sv-comp/WitnessCreator/witnesses/witness.st

diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml
index df65972..65c9273 100644
--- a/.github/workflows/gradle.yml
+++ b/.github/workflows/gradle.yml
@@ -7,6 +7,8 @@ on:
 
 env:
   SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64
+  WITNESS_CREATOR_VERSION: v0.1.1
+  WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814
 
 jobs:
   build:
@@ -26,8 +28,6 @@ jobs:
       run: ./gradlew copyNativeLibs
     - name: Build
       run: ./gradlew --no-daemon build -x test
-    - name: Build WitnessCreator JAR
-      run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar
     - name: Collect JavaSMT JAR
       run: |
         java_smt_dir="${HOME}/.gradle/caches/modules-2/files-2.1/org.sosy-lab/java-smt"
@@ -50,7 +50,6 @@ jobs:
         name: release-jars-${{ github.sha }}
         path: |
           symbolic-executor/lib/symbolic-executor.jar
-          targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar
           build/svcomp-runtime/java-smt-latest.jar
         if-no-files-found: error
         retention-days: 1
@@ -86,6 +85,23 @@ jobs:
         mkdir -p libs/java-library-path
         cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \
           libs/java-library-path/java-smt-latest.jar
+    - name: Download WitnessCreator runtime
+      run: |
+        version="${WITNESS_CREATOR_VERSION}"
+        zip_name="witness-creator-${version#v}.zip"
+        zip_path="${RUNNER_TEMP}/${zip_name}"
+        runtime_dir="${RUNNER_TEMP}/witness-creator-runtime"
+
+        curl --fail --location --retry 3 \
+          --output "${zip_path}" \
+          "https://github.com/SWAT-project/WitnessCreator/releases/download/${version}/${zip_name}"
+        echo "${WITNESS_CREATOR_SHA256}  ${zip_path}" | sha256sum --check -
+
+        mkdir -p "${runtime_dir}"
+        unzip -q "${zip_path}" -d "${runtime_dir}"
+        test -f "${runtime_dir}/WitnessCreator/build/libs/WitnessCreator.jar"
+        test -f "${runtime_dir}/WitnessCreator/witnesses/default_violation.st"
+        test -f "${runtime_dir}/WitnessCreator/witnesses/witness.st"
     - name: Determine release channel
       id: meta
       run: |
@@ -145,6 +161,7 @@ jobs:
         SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }}
         SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars
         SWAT_SVCOMP_RUNTIME_DIR: ${{ runner.temp }}/svcomp-runtime
+        SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator
         SWAT_SVCOMP_COMMIT: ${{ github.sha }}
         SWAT_SVCOMP_REF: ${{ github.ref_name }}
         SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }}
diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh
index accf707..c3a5e78 100755
--- a/scripts/package-svcomp.sh
+++ b/scripts/package-svcomp.sh
@@ -9,7 +9,14 @@ set -euo pipefail
 # else. The artifact root must contain:
 #
 # - symbolic-executor/lib/symbolic-executor.jar
-# - targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar
+#
+# Set SWAT_SVCOMP_WITNESS_CREATOR_DIR to the extracted WitnessCreator runtime
+# root from https://github.com/SWAT-project/WitnessCreator. The root must
+# contain:
+#
+# - build/libs/WitnessCreator.jar
+# - witnesses/default_violation.st
+# - witnesses/witness.st
 #
 # Set SWAT_SVCOMP_RUNTIME_DIR to a runtime package root that contains the
 # pinned SV-COMP Python environment:
@@ -32,6 +39,7 @@ DIST_DIR="${ROOT_DIR}/build/distributions"
 SUPPORT_DIR="${ROOT_DIR}/scripts/svcomp-package"
 ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)"
 RUNTIME_DIR="${SWAT_SVCOMP_RUNTIME_DIR:-${SWAT_SVCOMP_REFERENCE_DIR:-}}"
+WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_DIR:-}"
 VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}"
 LINUX_Z3_DIST="z3-4.15.4-x64-glibc-2.39"
 LINUX_Z3_ZIP="${ROOT_DIR}/libs/${LINUX_Z3_DIST}.zip"
@@ -41,18 +49,15 @@ if [[ -n "$RUNTIME_DIR" ]]; then
   RUNTIME_DIR="$(cd "$RUNTIME_DIR" && pwd)"
 fi
 
+if [[ -n "$WITNESS_CREATOR_DIR" ]]; then
+  WITNESS_CREATOR_DIR="$(cd "$WITNESS_CREATOR_DIR" && pwd)"
+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"
-}
-
 first_artifact_file() {
   local path
   for rel in "$@"; do
@@ -138,11 +143,11 @@ copy_artifact_file "$EXECUTOR_JAR" "$PACKAGE_DIR/symbolic-executor/lib/symbolic-
 
 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"
+[[ -n "$WITNESS_CREATOR_DIR" ]] || fail "SWAT_SVCOMP_WITNESS_CREATOR_DIR must point to the extracted WitnessCreator runtime root"
+[[ -f "$WITNESS_CREATOR_DIR/build/libs/WitnessCreator.jar" ]] || fail "missing WitnessCreator JAR: ${WITNESS_CREATOR_DIR}/build/libs/WitnessCreator.jar"
+[[ -f "$WITNESS_CREATOR_DIR/witnesses/default_violation.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/default_violation.st"
+[[ -f "$WITNESS_CREATOR_DIR/witnesses/witness.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/witness.st"
+copy_artifact_tree "$WITNESS_CREATOR_DIR" "$PACKAGE_DIR/WitnessCreator"
 
 install_z3_runtime_file z3 0755
 install_z3_runtime_file libz3.so
diff --git a/settings.gradle b/settings.gradle
index defcd23..2f822f5 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -6,7 +6,6 @@ rootProject.name = "SWAT"
 
 include 'symbolic-executor'
 include 'annotations'
-include 'targets:sv-comp:WitnessCreator'
 
 include 'targets:instruction-tests:IFXX'
 include 'targets:instruction-tests:I2X'
@@ -83,4 +82,4 @@ dependencyResolutionManagement {
 include 'targets:applications:modelmapper-test-app'
 findProject(':targets:applications:modelmapper-test-app')?.name = 'modelmapper-test-app'
 include 'targets:applications:reflection-test-app'
-findProject(':targets:applications:reflection-test-app')?.name = 'reflection-test-app'
\ No newline at end of file
+findProject(':targets:applications:reflection-test-app')?.name = 'reflection-test-app'
diff --git a/targets/sv-comp/WitnessCreator/build.gradle b/targets/sv-comp/WitnessCreator/build.gradle
deleted file mode 100755
index 78e0867..0000000
--- a/targets/sv-comp/WitnessCreator/build.gradle
+++ /dev/null
@@ -1,44 +0,0 @@
-buildscript {
-    repositories {
-        gradlePluginPortal()
-    }
-    dependencies {
-        classpath 'com.github.johnrengelman:shadow:8.1.1'
-    }
-}
-
-plugins {
-    id 'java'
-    id 'com.github.johnrengelman.shadow' version '8.1.1'
-}
-
-group = 'org.example'
-version = '1.0-SNAPSHOT'
-
-apply plugin: 'com.github.johnrengelman.shadow'
-apply plugin: 'java'
-
-shadowJar {
-    archiveBaseName.set('WitnessCreator')
-    archiveClassifier.set('')
-    archiveVersion.set('')
-}
-
-repositories {
-    mavenCentral()
-}
-
-dependencies {
-
-    implementation 'org.antlr:ST4:4.3.4'
-
-}
-
-
-jar {
-    manifest {
-        attributes(
-                'Main-Class': 'App'
-        )
-    }
-}
\ No newline at end of file
diff --git a/targets/sv-comp/WitnessCreator/src/main/java/App.java b/targets/sv-comp/WitnessCreator/src/main/java/App.java
deleted file mode 100755
index 37f7d43..0000000
--- a/targets/sv-comp/WitnessCreator/src/main/java/App.java
+++ /dev/null
@@ -1,180 +0,0 @@
-import java.io.BufferedReader;
-import java.io.IOException;
-import java.io.InputStream;
-import java.io.InputStreamReader;
-import java.nio.file.Files;
-import java.nio.file.Paths;
-import java.util.ArrayList;
-import java.util.Base64;
-import java.util.LinkedList;
-import java.util.List;
-
-import org.stringtemplate.v4.ST;
-import org.stringtemplate.v4.STGroup;
-import org.stringtemplate.v4.STRawGroupDir;
-
-import witness.WitnessAssumption;
-import witness.WitnessEdge;
-import witness.WitnessNode;
-
-public class App {
-
-    public static void main(String[] args) {
-
-
-        String path = args[1];
-        System.out.println("source path: " + path);
-
-        List<WitnessAssumption> witness = new LinkedList<>();
-        if(args[0].trim().length() == 0) {
-            System.out.println("No witness record, assuming default assertion violation");
-            (new App()).saveDefaultviolationWitness(path);
-        } else {
-            String param = new String(Base64.getDecoder().decode(args[0]));
-            String[] lines = param.split("\n");
-            for (String line : lines) {
-                line = line.substring(line.indexOf("[WITNESS]") + 10).trim();
-                // decode line base64
-                byte[] decodedBytes = Base64.getDecoder().decode(line);
-                line = new String(decodedBytes);
-
-                String[] parts = line.split("@@@");
-                if (parts.length != 4) {
-                    System.out.println("Received line:" + line);
-                    throw new RuntimeException("Invalid witness line: " + line);
-                }
-
-                String value = parts[0].trim();
-                int lineNumber = Integer.parseInt(parts[1].trim()); // account for 0-based line numbers
-                String className = parts[2].trim();
-                String description = parts[3].trim();
-
-                // Escape XML special characters in scope to avoid XML parse errors
-                // (e.g., <init> contains angle brackets that break XML parsing)
-                String scope = "L" + className + ";." + description;
-                scope = scope.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;");
-                witness.add(new WitnessAssumption(value, className + ".java", scope, lineNumber));
-            }
-            (new App()).checkAndSaveWitness(path, witness);
-            }
-        }
-
-
-
-    private void saveDefaultviolationWitness(String path){
-        STGroup group = new STRawGroupDir("witnesses", '$','$');
-        ST st = group.getInstanceOf("default_violation");
-        String result = st.render();
-        try {
-            System.out.println("Writing default violation witness to file: " + path + "/" + "witness.graphml");
-            Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes());
-        } catch (IOException e) {
-            System.err.println("Error writing witness to file: " + e.getMessage());
-        }
-    }
-    private void checkAndSaveWitness(String path, List<WitnessAssumption> witness) {
-
-
-        List<WitnessNode> nodes = new ArrayList<>();
-        List<WitnessEdge> edges = new ArrayList<>();
-
-        int nodeId = 0;
-        WitnessNode initNode = new WitnessNode(nodeId++);
-        nodes.add(initNode);
-        initNode.addData("entry", "true");
-        WitnessNode curNode = initNode;
-
-        for (WitnessAssumption wa : witness) {
-            String loc = getLineOfCode(path, wa.getClazz(), wa.getLine());
-            String assumption = computeAssumption(loc, wa);
-
-            WitnessNode prevNode = curNode;
-            curNode = new WitnessNode(nodeId++);
-            nodes.add(curNode);
-            WitnessEdge edge = new WitnessEdge(prevNode, wa, assumption, curNode);
-            edges.add(edge);
-        }
-
-        curNode.addData("violation", "true");
-
-        STGroup group = new STRawGroupDir("witnesses", '$','$');
-        ST st = group.getInstanceOf("witness");
-        st.add("nodes", nodes);
-        st.add("edges", edges);
-        String result = st.render();
-        try {
-            System.out.println("Writing violation witness to file: " + path + "/" + "witness.graphml");
-            Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes());
-        } catch (IOException e) {
-            System.out.println("Error writing witness to file: " + e.getMessage());
-        }
-    }
-
-    private String getLineOfCode(String path, String filename, int line) {
-        String absolutePath = path + "/" + filename;
-        try {
-            // Open absolutePath as a stream
-            InputStream is = Files.newInputStream(Paths.get(absolutePath));
-            if (is == null) {
-                System.out.println("Could not find file: " + absolutePath);
-                return null;
-            }
-            BufferedReader res = new BufferedReader(new InputStreamReader(is));
-            String loc = "";
-            for (int i = 0; i<line; i++) {
-                loc = res.readLine();
-            }
-            System.out.println("Line of code: " + loc);
-            return loc;
-        } catch (IOException e) {
-            System.out.println("Exception reading file: " + e.getMessage());
-            return null;
-        }
-    }
-
-    private String computeAssumption(String lineOfCode, WitnessAssumption wa) {
-        if (lineOfCode == null) {
-            return "true";
-        }
-
-        // Check if this is a string type by looking for nondetString() in the line
-        boolean isStringType = lineOfCode.contains("nondetString()");
-
-        int idx = lineOfCode.indexOf("Verifier");
-        if (idx < 0) {
-            return "true";
-        }
-        lineOfCode = lineOfCode.substring(0, idx).trim();
-        idx = lineOfCode.lastIndexOf("=");
-        if (idx < 0) {
-            // No assignment found - this is likely a return statement or direct call
-            // Use the witness value directly (e.g., "true", "false", or a literal value)
-            return wa.getValue();
-        }
-        // Check if this is a comparison (==) not an assignment (=)
-        // If the character before '=' is also '=', this is a comparison, not an assignment
-        if (idx > 0 && lineOfCode.charAt(idx - 1) == '=') {
-            // This is a comparison like "if (pos == ..." - no variable assignment
-            return wa.getValue();
-        }
-        lineOfCode = lineOfCode.substring(0, idx).trim();
-        String[] parts = lineOfCode.split(" ");
-        String id = parts[parts.length-1].trim();
-
-        // For string types, always use .equals() format with properly quoted value
-        if (isStringType) {
-            String value = wa.getValue();
-            // Add quotes around the value if not already present
-            if (!value.startsWith("\"")) {
-                // Escape any quotes and backslashes within the string value
-                value = value.replace("\\", "\\\\").replace("\"", "\\\"");
-                value = "\"" + value + "\"";
-            }
-            return id + ".equals(" + value + ")";
-        }
-
-        // For primitive types, use assignment format
-        return id + " = " + wa.getValue();
-    }
-
-} 
\ No newline at end of file
diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java
deleted file mode 100755
index d841c67..0000000
--- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java
+++ /dev/null
@@ -1,33 +0,0 @@
-package witness;
-
-public class WitnessAssumption {
-
-    private String scope;
-    private String value;
-    private final String clazz;
-    private final int line;
-
-    public WitnessAssumption(String value, String clazz, String scope, int line) {
-        this.scope = scope;
-        this.value = value;
-        this.clazz = clazz;
-        this.line = line;
-    }
-
-    public String getScope() {
-        return scope;
-    }
-
-    public String getValue() {
-        return value;
-    }
-
-    public String getClazz() {
-        return clazz;
-    }
-
-    public int getLine() {
-        return line;
-    }
-
-}
diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java
deleted file mode 100755
index 47fc961..0000000
--- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java
+++ /dev/null
@@ -1,35 +0,0 @@
-package witness;
-
-public class WitnessEdge {
-
-    private final WitnessNode source;
-
-    private final WitnessNode dest;
-
-    private final WitnessAssumption witness;
-
-    private final String assumption;
-
-    public WitnessEdge(WitnessNode source, WitnessAssumption witness, String assumption, WitnessNode dest) {
-        this.source = source;
-        this.dest = dest;
-        this.witness = witness;
-        this.assumption  = assumption;
-    }
-
-    public WitnessNode getSource() {
-        return source;
-    }
-
-    public WitnessNode getDest() {
-        return dest;
-    }
-
-    public WitnessAssumption getWitness() {
-        return witness;
-    }
-
-    public String getAssumption() {
-        return assumption;
-    }
-}
\ No newline at end of file
diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java
deleted file mode 100755
index 8ccc62e..0000000
--- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java
+++ /dev/null
@@ -1,29 +0,0 @@
-package witness;
-
-import java.util.HashMap;
-import java.util.Map;
-
-public class WitnessNode {
-
-    private final int id;
-
-    private final Map<String, String> data;
-
-    public WitnessNode(int id) {
-        this.id = id;
-        this.data = new HashMap<>();
-    }
-
-    public int getId() {
-        return id;
-    }
-
-    public Map<String, String> getData() {
-        return data;
-    }
-
-    public void addData(String key, String value) {
-        this.data.put(key, value);
-    }
-
-}
\ No newline at end of file
diff --git a/targets/sv-comp/WitnessCreator/witness.graphml b/targets/sv-comp/WitnessCreator/witness.graphml
deleted file mode 100644
index 99e9ee6..0000000
--- a/targets/sv-comp/WitnessCreator/witness.graphml
+++ /dev/null
@@ -1,134 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
-  <key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
-    <default>&lt;command-line&gt;</default>
-  </key>
-  <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
-  <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
-  <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
-    <default>false</default>
-  </key>
-  <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
-    <default>false</default>
-  </key>
-  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
-    <default>false</default>
-  </key>
-  <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
-    <default>false</default>
-  </key>
-  <key attr.name="cyclehead" attr.type="boolean" for="edge" id="cyclehead">
-    <default>false</default>
-  </key>
-  <key attr.name="threadId" attr.type="int" for="edge" id="threadId">
-    <default>0</default>
-  </key>
-  <key attr.name="createThread" attr.type="int" for="edge" id="createThread">
-    <default>0</default>
-  </key>
-  <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
-  <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
-  <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
-  <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
-  <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
-  <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
-  <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
-  <key attr.name="control" attr.type="string" for="edge" id="control"/>
-  <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
-  <key attr.name="assumption.resultfunction" attr.type="string" for="edge" id="assumption.resultfunction"/>
-  <key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
-  <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
-  <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
-  <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
-  <graph edgedefault="directed">
-      <data key="witness-type">violation_witness</data>
-      <data key="producer">SWAT</data>
-      <!-- data key="specification">na</data>
-      <data key="programfile">na</data>
-      <data key="programhash">na</data>
-      <data key="architecture">64bit</data>
-      <data key="sourcecodelang">Java</data -->
-    <node id="sink"/>
-
-       <node id="n0">
-             <data key="entry">true</data> 
-       </node>
-       <node id="n1">
-       </node>
-       <node id="n2">
-       </node>
-       <node id="n3">
-       </node>
-       <node id="n4">
-       </node>
-       <node id="n5">
-       </node>
-       <node id="n6">
-       </node>
-       <node id="n7">
-       </node>
-       <node id="n8">
-       </node>
-       <node id="n9">
-             <data key="violation">true</data> 
-       </node>
-
-
-       <edge source="n0" target="n1">
-         <data key="originfile">Main.java</data>
-         <data key="startline">12</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n1" target="n2">
-         <data key="originfile">Main.java</data>
-         <data key="startline">13</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n2" target="n3">
-         <data key="originfile">Main.java</data>
-         <data key="startline">14</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n3" target="n4">
-         <data key="originfile">Main.java</data>
-         <data key="startline">15</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n4" target="n5">
-         <data key="originfile">Main.java</data>
-         <data key="startline">16</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n5" target="n6">
-         <data key="originfile">Main.java</data>
-         <data key="startline">17</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n6" target="n7">
-         <data key="originfile">Main.java</data>
-         <data key="startline">18</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n7" target="n8">
-         <data key="originfile">Main.java</data>
-         <data key="startline">19</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> <edge source="n8" target="n9">
-         <data key="originfile">Main.java</data>
-         <data key="startline">20</data>
-         <data key="threadId">0</data>
-         <data key="assumption">true</data>
-         <data key="assumption.scope">java::LMain;.main([Ljava/lang/String;)V</data>
-       </edge> 
-
-  </graph>
-</graphml>
\ No newline at end of file
diff --git a/targets/sv-comp/WitnessCreator/witnesses/default_violation.st b/targets/sv-comp/WitnessCreator/witnesses/default_violation.st
deleted file mode 100755
index 81cb4a6..0000000
--- a/targets/sv-comp/WitnessCreator/witnesses/default_violation.st
+++ /dev/null
@@ -1,56 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
-  <key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
-    <default>&lt;command-line&gt;</default>
-  </key>
-  <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
-  <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
-  <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
-    <default>false</default>
-  </key>
-  <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
-    <default>false</default>
-  </key>
-  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
-    <default>false</default>
-  </key>
-  <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
-    <default>false</default>
-  </key>
-  <key attr.name="cyclehead" attr.type="boolean" for="edge" id="cyclehead">
-    <default>false</default>
-  </key>
-  <key attr.name="threadId" attr.type="int" for="edge" id="threadId">
-    <default>0</default>
-  </key>
-  <key attr.name="createThread" attr.type="int" for="edge" id="createThread">
-    <default>0</default>
-  </key>
-  <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
-  <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
-  <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
-  <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
-  <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
-  <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
-  <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
-  <key attr.name="control" attr.type="string" for="edge" id="control"/>
-  <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
-  <key attr.name="assumption.resultfunction" attr.type="string" for="edge" id="assumption.resultfunction"/>
-  <key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
-  <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
-  <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
-  <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
-  <graph edgedefault="directed">
-      <data key="witness-type">violation_witness</data>
-      <data key="producer">SWAT</data>
-      <!-- data key="specification">na</data>
-      <data key="programfile">na</data>
-      <data key="programhash">na</data>
-      <data key="architecture">64bit</data>
-      <data key="sourcecodelang">Java</data -->
-    <node id="sink"/>
-    <node id="n0">
-        <data key="entry">true</data> <data key="violation">true</data>
-    </node>
-  </graph>
-</graphml>
\ No newline at end of file
diff --git a/targets/sv-comp/WitnessCreator/witnesses/witness.st b/targets/sv-comp/WitnessCreator/witnesses/witness.st
deleted file mode 100755
index 6e7e57a..0000000
--- a/targets/sv-comp/WitnessCreator/witnesses/witness.st
+++ /dev/null
@@ -1,70 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
-  <key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
-    <default>&lt;command-line&gt;</default>
-  </key>
-  <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
-  <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
-  <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
-    <default>false</default>
-  </key>
-  <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
-    <default>false</default>
-  </key>
-  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
-    <default>false</default>
-  </key>
-  <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
-    <default>false</default>
-  </key>
-  <key attr.name="cyclehead" attr.type="boolean" for="edge" id="cyclehead">
-    <default>false</default>
-  </key>
-  <key attr.name="threadId" attr.type="int" for="edge" id="threadId">
-    <default>0</default>
-  </key>
-  <key attr.name="createThread" attr.type="int" for="edge" id="createThread">
-    <default>0</default>
-  </key>
-  <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
-  <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
-  <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
-  <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
-  <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
-  <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
-  <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
-  <key attr.name="control" attr.type="string" for="edge" id="control"/>
-  <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
-  <key attr.name="assumption.resultfunction" attr.type="string" for="edge" id="assumption.resultfunction"/>
-  <key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
-  <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
-  <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
-  <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
-  <graph edgedefault="directed">
-      <data key="witness-type">violation_witness</data>
-      <data key="producer">SWAT</data>
-      <!-- data key="specification">na</data>
-      <data key="programfile">na</data>
-      <data key="programhash">na</data>
-      <data key="architecture">64bit</data>
-      <data key="sourcecodelang">Java</data -->
-    <node id="sink"/>
-
-   $nodes:{ n |
-    <node id="n$n.id$">
-    $n.data.keys:{k |
-      <data key="$k$">$n.data.(k)$</data> }$
-    </node>
-   }$
-
-   $edges:{ e |
-    <edge source="n$e.source.id$" target="n$e.dest.id$">
-      <data key="originfile">$e.witness.clazz$</data>
-      <data key="startline">$e.witness.line$</data>
-      <data key="threadId">0</data>
-      <data key="assumption">$e.assumption$</data>
-      <data key="assumption.scope">java::$e.witness.scope$</data>
-    </edge> }$
-
-  </graph>
-</graphml>
\ No newline at end of file