# ENV — `proof-estate-lean-z3`

Measured 2026-09-17 on the machine that built this packet, under the estate proof environment
(`env -u LC_ALL PATH="/opt/homebrew/opt/python@3.11/libexec/bin:$HOME/.local/bin:$HOME/.elan/bin:$HOME/.cargo/bin:/opt/homebrew/bin:$PATH"`, stdin `/dev/null`):

| tool | version | probe |
|---|---|---|
| macOS | 26.6, arm64 | `sw_vers`, `uname -m` |
| python3 | 3.11.14 (`/opt/homebrew/opt/python@3.11/libexec/bin/python3`) | `python3 --version` |
| z3 (Python binding) | 4.15.4 | `python3 -c "import z3; print(z3.get_version_string())"` |
| cvc5 (Python binding) | 1.3.4 — optional; without it the witness runs Z3 only and says so | `python3 -c "import cvc5; print(cvc5.__version__)"` |

**Required tool, and the ENV branch.** `repro.sh` exits 69 with an `ENV:` line when `python3` cannot import `z3`,
because the witness would SKIP and reproduce nothing. Measured: with `PATH=/usr/bin:/bin` (the system interpreter,
which has no z3) the script printed `ENV: …` and exited 69.

**Lean.** This witness runs no Lean. The claim's Lean lane is not exercised here (see `EXPECTED.md`). For a run
that does involve Lean, the Lean 4 toolchain is `~/.elan/bin/lean` (probe: `~/.elan/bin/lean --version` →
`Lean (version 4.34.0, arm64-apple-darwin24.6.0, commit 293d5d0c…, Release)`). **`/opt/homebrew/bin/lean` is a
different program** (it reports `lean 1.0.223`), so never trust whichever `lean` comes first on `PATH`.

**Runtime.** 1.2 to 1.3 s. It writes only `__pycache__` under `proofs/z3/` and a temporary file under `$TMPDIR`.