Totally Correct Local Solvers for (Side-Effecting) Constraint Systems

Artifact for **Totally Correct Local Solvers for (Side-Effecting) Constraint Systems**. Submitted to VMCAI 2027. The artifact provides the Docker environment and scripts to check compilation/proofs, rerun benchmarks, and generate the paper's tables and figures from recorded measurements. The solver definitions, proofs, extracted libraries, and adapters are maintainedin [tc-solvers](https://github.com/kalmera/tc-solvers) (will be made publicon paper acceptance). Proof checking is done using the Rocq Prover 9.1.Benchmarks use SV-COMP 2026 tasks and are run using the BenchExec tool.Artifact workflow is automated using Python scripts. For Badges: Available, Functional No paid licenses or accounts are needed. After downloading the ZIP andinstalling Docker, the evaluation needs no external connection. No reviewertelemetry is collected. The package includes native images for x86-64 andARM64 architectures. Requirements: - Docker accessible to your ordinary user, Python 3.9 or newer, and a nativex86-64 or ARM64 machine. - Two CPU cores available to Docker; **8 GiB Docker RAM** for proofs, or **4 GiB**for smoke, sequential benchmarks, and figures. Parallel benchmarks needadditional cores and memory capacity; the setup script suggests a process limit. - **10 GiB free after unpacking** for loading the native images and evaluation.If Docker and the artifact use separate filesystems, allow 8 GiB in Dockerstorage and 2 GiB alongside the artifact for outputs. - Linux: rootful Docker, cgroup v2, and permission for nested user namespaces.On hosts that restrict these namespaces, an administrator-installed AppArmorprofile may be needed (provided). On macOS: Docker Desktop. On our server, the proof checking took about 13 minutes. Using serial execution (`--jobs 1`), the 100-task benchmark took 36 minutes,and the full 1030-task benchmark took 5.3 hours on our server.Benchmarks can be run in parallel, but this may introduce some noise into the results.