Add a Z3 per-query timeout to the translation validator (bounds i64 verification; re-enable ignored i64 inline tests)

[avrabe]

Why

The #145 fix (PR #146) makes inline_functions' Z3 translation validator
attempt the real equivalence solve on i64 functions (previously it panicked
during eq-construction and fast-reverted). The verifier has a size threshold
(LOOM_Z3_MAX_INSTRUCTIONS, default 2000) but no wall-clock per-query
timeout, so a single i64 bitvector formula that hits a Z3 slow-solve cliff
can grind/hang.

Observed: the test_inline_i64_* tests (full inline + i64 Z3 verify) hang the
CI Test matrix (a job ran >75 min). They were #[ignore]'d in PR #146 to
unblock the matrix; this issue tracks the proper fix and their re-enable.

Risk this addresses

Without a query timeout, a real i64-heavy module (the gale-ffi /
compiler_builtins case from #145 — ~824 functions) may verify very slowly
when run through loom optimize, trading #145's "no-op + 21 MB spam" for
"slow/grind." A timeout converts that into bounded verify-or-revert.

Proposed fix

• Set a Z3 solver per-check() timeout (e.g. via the timeout solver param,
  configurable through a LOOM_Z3_TIMEOUT_MS env, sane default).
• On Unknown (timeout), the existing logic already treats it as
  "cannot prove" → conservative revert. So a slow solve becomes a fast,
  sound revert.
• Re-enable the 5 #[ignore]'d tests in loom-core/src/lib.rs
  (test_inline_i64_*, test_inline_i64_loop_kinduction_no_panic) once the
  timeout bounds them.

Falsification

Wrong if, with the timeout in place, the i64 inline tests still hang, OR a
genuinely-fast i64 proof is now spuriously timed-out and reverted (regressing
the i64-inlining win). Tune the default so common i64 functions solve well
within it.

Refs: #145