Given the engine can afford days of compute (fuzzing-grade), widen the
solver budgets so hard queries resolve instead of timing out:
- checkAdaptive escalation ceiling raised to 1 hour per query (was 8x base)
- budget_seconds 7200 -> 604800 (7 days)
- per_tu_timeout 900 -> 86400 (24h)
A single hard query getting up to an hour of escalating compute is cheap
relative to a lost vulnerability.
The 1800s solver budget, 6s per-query timeout, and 300s per-TU watchdog were
too tight for large security scans (e.g. 780-file yams), causing Z3 "unknown"
results and preempted TUs. Raise to 7200s budget, 30s per-query, and 900s
per-TU so slow-but-productive TUs finish and complex queries resolve.
- int-overflow: unsigned wrap is defined, not UB — split to
fold.unsigned-wrap so signed-UB findings aren't drowned; on by
default (--report-unsigned-wrap=false opts out)
- use-after-free: model return/throw as path-terminating so
`delete p; return;` in an error branch can't poison the fall-through
- oob-access: real sizeof for complete structs (was 1); recognize
std::min/clamp/modulo index bounds
- memory-leak: static-storage singletons + return-to-caller are
caller-owned, not leaks
YAMS scan: UAF 4→0, struct-OOB ~10→0, singleton-leak ~15→0,
min/modulo-bound OOB →0. 137/137 tests pass.
