chore(build): remove bundled Z3 support

.agents/skills/build-openshell-mxc-windows/SKILL.md

@@ -265,7 +265,7 @@ MXC on Windows. Each other `compute-driver-*` feature installs its own Windows
 rejection stub without linking that driver crate. The default
 `in-tree-compute-drivers` alias enables all five features. An MXC-only build
 uses `--no-default-features --features compute-driver-mxc` (add `telemetry`
-and `bundled-z3` as needed).
+and `openshell-server/prebuilt-z3` as needed).
 
 | Driver | Windows build behavior | Runtime behavior |
 |---|---|---|

CONTRIBUTING.md

@@ -309,17 +309,17 @@ Project requirements:
 - Rust 1.94+
 - Python 3.11+
 - Docker (running)
-- CMake 3.16+ (only required when building with the `bundled-z3` feature)
 
 ### Z3 installation
 
 The `openshell-prover` crate and standalone `openshell-prover-cli` binary link
 directly against Z3. The `openshell-server` crate depends on the prover, and
 the `openshell-gateway` binary crate depends on `openshell-server` in turn.
-These packages forward a `bundled-z3` feature to
-`openshell-prover/bundled-z3`. The `openshell-cli` crate does not depend on Z3.
-On macOS and Linux, install the system Z3 development package; `z3-sys`
-discovers it through `pkg-config`.
+The `openshell-cli` crate does not depend on Z3. The Nix development shell
+supplies Z3. For builds outside that shell on macOS and Linux, install the
+system Z3 development package; `z3-sys` discovers it through `pkg-config`.
+The linker uses the installed static or shared library. The Nix development
+shell provides a static Z3 library.
 
 ```bash
 # macOS
@@ -332,14 +332,17 @@ sudo apt install libz3-dev
 sudo dnf install z3-devel
 ```
 
-If you prefer not to install Z3 system-wide, use the bundled Z3 feature. This
-compiles Z3 from source during the Rust build and requires CMake 3.16+:
+To build Z3 from source instead, enable `vendored-z3` (requires CMake and a C++
+compiler):
 
 ```bash
-cargo build -p openshell-prover --features bundled-z3
-cargo build -p openshell-prover-cli --features bundled-z3
+cargo build -p openshell-prover --features vendored-z3
+cargo build -p openshell-prover-cli --features vendored-z3
 ```
 
+Local gateway image and E2E builds enable `vendored-z3` so their
+copied gateway binaries do not need a shared Z3 library in the runtime image.
+
 For x86-64 and ARM64 Windows MSVC builds, use one of these Z3 paths:
 
 - Prebuilt Z3 (the default for `windows:*` tasks): `z3-sys` downloads the
@@ -353,14 +356,12 @@ For x86-64 and ARM64 Windows MSVC builds, use one of these Z3 paths:
   target-compatible MSVC Z3 library and `Z3_SYS_Z3_HEADER` at the full path to `z3.h`.
   The `windows:*` tasks use this path automatically when `Z3_LIBRARY_PATH_OVERRIDE`
   is set.
-- Bundled Z3: for direct Cargo builds, pass `--features bundled-z3` so `z3-sys`
-  builds Z3 from source.
 
 `openshell-prover` itself has no `bindgen`/`libclang` dependency, so building
 just this crate does not require `LIBCLANG_PATH`:
 
 ```powershell
-cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundled-z3
+cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features prebuilt-z3
 ```
 
 ### Windows full build

Cargo.toml

@@ -143,7 +143,7 @@ k8s-openapi = { version = "0.24", features = ["v1_29"] }
 uuid = { version = "1.10", features = ["v4"] }
 signal-hook = "0.3"
 
-# SMT solver (uses system libz3; enable z3/bundled via the prover's bundled-z3 feature for local dev without system z3)
+# SMT solver (system libz3 by default; opt into vendored source or a prebuilt release)
 z3 = "0.21"
 
 [workspace.lints.rust]

crates/openshell-gateway/Cargo.toml

@@ -73,7 +73,7 @@ telemetry = ["openshell-core/telemetry", "openshell-server/telemetry"]
 ## telemetry-on build. Kept in sync with `default` by
 ## `rust:verify:defaults-without-telemetry`.
 defaults-without-telemetry = ["in-tree-compute-drivers"]
-bundled-z3 = ["openshell-server/bundled-z3"]
+vendored-z3 = ["openshell-server/vendored-z3"]
 
 [lints]
 workspace = true

crates/openshell-prover-cli/Cargo.toml

@@ -15,7 +15,7 @@ name = "openshell-prover"
 path = "src/main.rs"
 
 [features]
-bundled-z3 = ["openshell-prover/bundled-z3"]
+vendored-z3 = ["openshell-prover/vendored-z3"]
 prebuilt-z3 = ["openshell-prover/prebuilt-z3"]
 
 [dependencies]

crates/openshell-prover/Cargo.toml

@@ -11,7 +11,7 @@ license.workspace = true
 repository.workspace = true
 
 [features]
-bundled-z3 = ["z3/bundled"]
+vendored-z3 = ["z3/vendored"]
 prebuilt-z3 = ["z3/gh-release"]
 
 [dependencies]

crates/openshell-server/Cargo.toml

@@ -120,7 +120,7 @@ default = ["telemetry"]
 ## On by default; build with `--no-default-features` for a telemetry-free gateway
 ## that contains no telemetry endpoint, HTTP client, or emission code.
 telemetry = ["openshell-core/telemetry"]
-bundled-z3 = ["openshell-prover/bundled-z3"]
+vendored-z3 = ["openshell-prover/vendored-z3"]
 prebuilt-z3 = ["openshell-prover/prebuilt-z3"]
 test-support = []