Saturation Meets SMT: Locality-Aware Reachability over Logical Predicates (Accompanying Artifact)

The artifact accompanies the paper “Saturation Meets SMT: Locality-Aware Reachability over Logical Predicates” submitted to FMCAD 2026. It contains everything needed to reproduce the paper’s figures from pre-recorded benchmark results and to re-run the benchmarks from scratch. The artifact is organized into three main directories:- benchmarking/: benchmark definitions, tool binaries, execution scripts, and benchmark results- plots/: scripts and data for regenerating all figures and tables from the paper- third-party-licenses/: license files for bundled third-party tools The artifact bundles Theta 6.28.0, ITS-reach 0.2.20250911075655, LTSmin 3.0.2, Z3 4.5.0, and BenchExec 3.30-dev. Requirements:- Docker- sudo access for temporarily adjusting an AppArmor kernel setting required by BenchExec on Ubuntu 24.04+ The artifact was tested on Ubuntu 24.04.3 LTS (x86_64). The plots directory already contains the raw BenchExec result files used in the paper, so reviewers can regenerate all figures immediately without re-running benchmarks. The generated output is a self-contained PDF containing all plots and tables from the paper. The benchmarks cover three domains:- DVE models from the BEEM suite- Petri net models from the 2025 Model Checking Contest- Software concurrency benchmarks from the SV-COMP concurrency category A smoke test is included and runs 5 models from each domain across most tool configurations in roughly 30 seconds. The full benchmark set contains 300 DVE models, 1617 Petri net models, and 726 software concurrency benchmarks across 20 tool configurations. Each task runs with a 15-minute timeout, 15 GB memory limit, and 2 CPU cores. Full execution may take weeks on a single machine and is primarily intended for compute clusters. Scripts for VerifierCloud / BenchCloud execution are included. For detailed instructions, command-line options, and output locations, please refer to the included README files:- main README: overall artifact structure and quick start- benchmarking/README.md: benchmark execution and cluster usage- plots/README.md: figure regeneration and plotting pipeline