Link libz3 instead of spawning the z3 binary

The compiler talks to z3 by spawning it and piping SMT-LIB2 over stdin. Linking the library instead removes a runtime dependency, makes the solver version a link-time fact, and makes the missing-solver state (#374) unrepresentable.

Where we are

Four call sites spawn z3 -in -smt2, write a QF_BV script to stdin, and scan stdout for sat/unsat:

src/hir/seam.rs:217      run_z3
src/hir/seam.rs:331      persistent solver
src/hir/prover.rs:46
src/hir/check/raw.rs:1129

seam.rs already keeps a persistent solver reused across every seam in a compilation, with a one-time preamble and a benchmark for marginal per-seam cost. So the obvious "stop paying for process spawn" argument is largely already banked — that work is done, and performance is not the main reason to do this.

The reasons that remain

1. It closes hiraditya/Vx.1#374 by construction. Today a missing z3 makes every obligation report success. Linked, the solver cannot be absent at run time, because there is no run-time lookup.

2. The version becomes a link-time fact. hiraditya/Vx.1#367 exists because two machines in this project were running z3 4.8.12 and 4.15.4 — seven years apart — on a component that decides proof obligations. Pinning a binary is a convention; linking a library is a build artifact.

3. It removes z3 from the runtime requirements of a shipped binary. hiraditya/Vx.1#368 currently has to ship a 19–29 MB z3 executable alongside vxc and document it as a required tool. Linked, that disappears.

4. Structured results instead of parsed stdout. The current code greps for a line equal to sat/unsat and string-slices the model out of (get-value ...) output. The API returns a verdict and a model object.

What it costs, honestly

The build dependency moves from run time to build time. Mostly already paid: scripts/setup_linux.sh installs libz3-dev, and Homebrew's z3 ships headers.

Static vs dynamic is a genuine tension. Homebrew ships no libz3.a (verified absent), so:

• dynamic reintroduces exactly the install_name_tool problem that hiraditya/Vx.1#368 just got rid of — Homebrew's libLLVM hard-codes /opt/homebrew/opt/z3/lib/libz3.4.15.dylib while upstream ships install_name libz3.dylib;
• static needs either a self-built z3 or the z3 crate's bundled feature, which compiles z3 from source — a multi-minute C++ build on every fresh checkout and in CI, and it would noticeably slow the image in hiraditya/Vx.1#369.

Worth noting: vxc currently links libz3.dylib and references zero Z3 symbols. That dependency is spurious — llvm-config --link-static --system-libs emits it because Homebrew's LLVM was configured with Z3 for the clang static analyser. So today we pay the dependency and get none of the benefit.

Migration is smaller than it looks. The scripts are already SMT-LIB2 text, so Z3_parse_smtlib2_string keeps the existing formula generation and replaces only the plumbing. Rewriting the encodings against the AST API is a separate, optional step.

Suggested sequencing

1. Fix hiraditya/Vx.1#374 first — fail closed on a missing solver. Small, and correct regardless of what happens here.
2. Decide static vs dynamic, since it determines whether this helps or hurts hiraditya/Vx.1#368/#369. Static is the only option that actually removes the packaging problem.
3. Introduce the library behind the existing run_z3-shaped interface, keeping SMT-LIB2 text and parse_smtlib2_string, so the four call sites do not change.
4. Record the linked z3 version in --diagnostics-json provenance.

Keep the process path as a fallback only if there is a real need to swap solvers; otherwise it is a second code path discharging proof obligations, which is its own liability.

Review the four call sites in src/hir/seam.rs, src/hir/prover.rs, and src/hir/check/raw.rs, then inspect scripts/setup_linux.sh and the current build configuration. Start with the existing run_z3-shaped interface and its SMT-LIB2 flow. Done means the solver is linked rather than spawned, existing call sites remain supported, and the linked version is recorded in --diagnostics-json provenance.