Repository navigation
Use the full SV-COMP time and memory budget #51
Description
Make sure SWAT uses the full SV-COMP resource budget. bench-defs swat.xml: timelimit="15 min" (CPU time), hardtimelimit="16 min", memlimit="15 GB", cpuCores="4".
Already done on dev: internal 180 s run cutoff and 60 s Z3 timeout removed (#32).
Still to check:
- CPU time vs. wall time: JVM (GC/JIT threads) + explorer + Z3 consume CPU time in parallel, so the 15 min CPU budget may run out well before 15 min wall time — measure on long-running tasks
- Memory:
SVCompDriver.build_commandpasses-Xmx32g(defaultmem=32), above the 15 GB limit, and explorer memory comes on top — set heap so JVM + explorer stay under 15 GB - No remaining caps that end exploration early (iteration limits, per-run timeouts, e.g. the unused 60 s default in
svcomp/SVCompHandler.py) - Verify with a BenchExec run using the competition limits (count
TIMEOUT/OUT OF MEMORYvs.unknown)
Activity
nils-loose commentedon Oct 15, 2026
Data from the full Java run (2026-10-15, no memory limit enforced): 21 runs grew past 15 GB RSS with
-Xmx32g(up to 72 GB). In SV-COMP they would end as OUT OF MEMORY, including 8 currently correct SAFE results (BellmanFord-, Tsp-). Tasks: BellmanFord-, Tsp-, BufferedBlockCipher, DistinguishedNameParser, jbmc-regression/array1. Suggest-Xmx12gor deriving it from the limit. Full list: section "Memory" in the local campaign report.nils-loose commentedon Oct 20, 2026
#88 (merged into
devthrough #92) covers most of this:SVCompHandler.pyis removed.Still open:
solid-eureka commentedon Oct 27, 2026
Part of this is in #109: a wall-clock deadline in
ResourceBudget(a run stops before the wall limit as well as the CPU limit) and an executorDeadlockWatchdog(a deadlocked run ends with UNKNOWN instead of hanging until the wall timeout). The BenchExec campaign and a per-round executor budget are still open.🤖 Generated with Claude Code