Re-land native i64.rem_u/rem_s value model behind a per-query solver timeout (reverted #844)

[avrabe]

Context

#844 replaced the I64RemU/I64RemS HAVOC in synth-verify's arm_semantics
with a real native 64-bit remainder (dividend.bvsrem/bvurem(&divisor) via
ordeal 0.12 BvTerm::Urem). Valuable enrichment — it closes a trap-only-VC gap
where a wrong-destination i64 rem lowering was accepted as Verified.

Problem (why reverted)

A 64-bit bvsrem/bvurem is the hardest bitvector class, and it hangs both
solvers: pure-Rust ordeal default (→ CI Test job) and the Z3 differential
(→ CI Z3 Verification job). Every CI run since #844 ran 4–6h and timed out;
last green CI on main was 2026-07-20 (61acec99). #844 was reverted (db0f1f2)
to un-hang CI and unblock the v0.50.0 tag. The revert is byte-invisible
(verify-only, no codegen change; frozen anchors untouched).

Fix for re-landing (v0.51)

Re-land the native value model with a per-query solver timeout so a hard
bvurem/bvsrem degrades to unknown instead of hanging. Evaluate: ordeal
per-query resource bound; a bounded-solver harness returning Unknown past a
budget; or a bounded-width decidable abstraction.

Acceptance: the i64-rem value VC (wrong-dest rejected / correct-dest Verified,
the #844 non-vacuity gate) runs in seconds; Test + Z3 jobs stay green.
Tracked under VCR-VER-002 / epic #242.