test: [repo] Install Z3 on the ubuntu CI legs so solver-gated tests run (AGENTS.adoc CI guidance) #62

Umbrella: #53 (CI hygiene & estate-conformance top-up — 2026-10-10).

Evidence

AGENTS.adoc ("CI & Solver Detection") says CI should install at least one solver and ensure it is on PATH (e.g. apt-get install z3 on Ubuntu runners). CI.yml installs none — so every solver-gated test skips on all 9 matrix legs. Concretely, the Z3 unsat-core fix from #47 / PR #49 (set-option! name mapping + get_unsat_core on check_sat) has never executed in CI; it was verified locally against Z3 4.13.3 only. A green matrix currently means "the non-solver tests pass", not "the package works with a solver".

Fix

Install Z3 on the ubuntu legs (sudo apt-get update && sudo apt-get install -y z3 on ubuntu-latest only, before Run tests), keeping the documented graceful-skip behaviour for legs without a solver (macos/windows). This matches AGENTS.adoc's own guidance and makes the test (*) legs exercise the solver path they exist for.

Acceptance criteria

• ubuntu CI legs run Pkg.test() with z3 on PATH; solver-gated tests (Z3 unsat core, statistics against real Z3 output) execute rather than skip
• non-ubuntu legs keep the skip behaviour; AGENTS.adoc's "document this in CI logs" expectation is met by the install step being visible in the log
• The CI matrix stays green with the solver present (no loosened tests)

Fixed in the follow-up PR on arena/cbd1e29d-smtlib-jl; closes when it merges.

References

AGENTS.adoc (CI & Solver Detection), #47 (unsat-core fix), TOOLING-VERSION-INTEGRITY Rule 3 (gates must prove execution).