ordeal 0.12.0 solver-performance regression HANGS div/rem trap-preservation VCs — pinned back to 0.9.1

[avrabe]

Symptom

Every CI run since the ordeal 0.9.1 → 0.12.0 bump (#825, 5cb5d33) HUNG the
Test job (pure-Rust ordeal default) and the Z3 Verification job for 4–6h,
timing out. Last green CI on main was 61acec99 (2026-07-20 21:45:27) — using
ordeal 0.9.1, three seconds before #825 merged. No commit with ordeal 0.12
has ever passed CI.

Root cause

ordeal 0.12.0 has a solver-performance regression on signed 64-bit AND even
32-bit bvsrem/bvsdiv queries. Confirmed by isolating the pre-existing
(#753, v0.43) 32-bit test translation_validator::tests::rems_single_zero_guard_is_exactly_right
(an I32RemS Sdiv+Mls trap-preservation VC) — it runs in <1s on 0.9.1 and HANGS
(>240s, killed) on 0.12.0 with #844 already reverted. #844's native i64
bvsrem/bvurem made it dramatically worse but was not the sole cause.

Fix (this repo)

Pinned ordeal = "=0.9.1" in crates/synth-verify/Cargo.toml — the exact
last-green version — and removed the #836 BvTerm::Urem match arms (that variant
only exists in 0.12). #844 (native i64 rem) reverted (db0f1f2), tracked for
re-land in #848. This restores the exact solver stack that was green on 2026-07-20.

Upstream (ordeal)

The bvsrem/bvsdiv perf regression between 0.9.1 and 0.12.0 should be reported
to and fixed in ordeal. Re-adopt 0.12+ (and re-land #844/#848) only once the
regression is fixed AND native i64 rem lands behind a per-query solver timeout.

Process gap (see also the dependabot auto-merge workflow)

0.9 → 0.12 is breaking by 0.x semver convention but dependabot classifies it
as "minor", so .github/workflows/dependabot-auto-merge.yml (#838) auto-merged a
breaking solver bump straight to main with no human gate. The workflow must HOLD
0.x minor bumps (or exempt/pin the solver dep). Follow-up.