z3

z3-rs 0.19.7 (pinned in native/angr/Cargo.toml) DOES expose Array::store and Array::select in z3::ast::Array. Confirmed at z3-0.19.7/src/ast/array.rs:60 (select) and :103 (store). No version bump needed if Option B (Z3 array primitive) is ever pursued as Phase 3 of the lazy-memory plan. Per existing memory invariant-lazy-mem-deferred-2026-05-09 grep, no Array/ArraySort usage currently exists in native/angr/src/symbolic/.

Z3 AST construction & BV rewriting internals (mined from z3-4.13.0 source): C API (Z3_mk_bvadd, etc.) creates raw AST nodes WITHOUT simplification. The bv_rewriter (invoked by th_rewriter during solver preprocessing, NOT at node creation time) applies simplifications: Extract(Extract(x))→fused, Extract(Concat(...))→distributed, adjacent Concat extracts fused — i.e. Concat(Extract[h1:l1](x), Extract[h2:l2](x)) with l1==h2+1 fuses into a single Extract. Z3 uses hash-consing (ast_manager::m_ast_table) so structurally identical subexpressions share nodes. Z3 has NO native bitvector Reverse operation: both Python and Rust decompose Reverse to Extract+Concat chains, which the fusion rules above clean up; Extract is O(1) at bit-blast time. The QF_BV preprocessing pipeline (qfbv_tactic.cpp) runs: simplify → propagate_values → solve_eqs → elim_uncnstr → bv_size_reduction → simplify(som=true,flat=true,local_ctx=true) → simplify(hoist_mul=true) → max_bv_sharing → ackermannize_bv. max_bv_sharing also runs automatically in asserted_formulas.cpp preprocessing (line 304) to reorder AC ops for sharing before bit-blasting.

Z3AstPtr design: opted against the originally-spec'd <'ctx> lifetime parameter (task angr-6zpl described 'struct Z3AstPtr<'ctx> { ptr: NonNull<_>, _ctx: PhantomData<&'ctx Context> }'). Reason: with thread-local Z3 context, extraction sites take 'let ctx = Context::thread_local()' — an owned Rc-cloned Context. A returned Z3AstPtr<'ctx> tied to that local ctx wouldn't compile (ctx drops at function end). Solution: drop the lifetime parameter; store an owned Context clone in the struct (z3-rs's own Bool/BV pattern). Construction overhead is one Rc bump (~40ns) — negligible. Drop uses Context::get_z3_context() instead of caching a raw Z3_context, which would risk dangling if anyone tried to outlive the typed Context.

Z3 bit-blasting ITE cost: ITE(cond, bv_x, bv_y) creates one per-bit multiplexer — 4 SAT clauses per bit worst case (128 clauses for 32-bit). BUT ITE(cond, BV(1), BV(0)) with constant branches simplifies to just 'cond' (0 extra clauses). So our comparison ITE wrapping has ZERO extra bit-blast cost IF Z3's bool_rewriter detects the pattern. The real cost is: (1) extra Z3 AST nodes consuming memory/hash-table space, (2) rewriter must pattern-match to simplify, (3) structural difference affects hash-consing sharing with other constraints.

Z3 bv_sort_ac=true sounds free (just canonicalize AC-op args) but on the angr bench matrix it BLOWS UP defcon2016quals_baby-re by 7x (0.50s -> 3.71s) and adds +25% to flareon2015_2. Hypothesis: re-sorting Concat arg order defeats Extract-fusion patterns that the rest of the QF_BV pipeline relies on. Discovered in angr-ya00.1 (2026-05-19) bv_* sweep. Do NOT enable globally even though it pairs well with mul2concat on fairlight.

Z3 context sharing: CANNOT share Z3 context between Python and Rust threads — not thread-safe. Z3_translate() does deep structural copy with caching (obj_map cache, resets every 2^14 calls). Z3_solver_translate() copies full solver state including assertions and model converter. Z3_solver_to_string()/from_string() available for text-based round-trip. Assertions processing is DEFERRED until check() — assert() is O(1) append. For Rust-Python constraint transfer, Z3_translate() is most efficient (single AST tree pass with caching).

Z3 context sharing works: set_shared_z3_context(py_ctx.ctx.value) makes Rust create Z3 ASTs in Python's context. RPATH configured in .cargo/config.toml for pip Z3 library. z3-rs patched (native/z3-patched/) for public set_thread_local/new and borrowed flag in ContextInternal to prevent Z3_del_context on foreign contexts. KNOWN BUG: process exit segfaults due to C runtime cleanup ordering between Python and Rust Z3 destructors — harmless, does not affect benchmark harness (multiprocessing isolation). Next step: build Rust Z3 ASTs in shared context (angr-vq3) to eliminate constraint translation overhead.

Z3 fast-path constraint assertion: add_constraint_ast tries to extract raw Z3_ast from claripy.backends.z3.convert(ast).as_ast().value and assert directly to Rust solver via add_constraint_raw. Falls back to RustBV conversion if extraction fails. This preserves claripy's Z3 AST structure (flat Concat-of-bit-extracts) vs Rust's build_z3_ast structure (nested SignExt chains), which Z3 can solve 3-7x faster. Impact: hackcon2016 87s→36-65s.

Z3 FP support design (angr-bgv0, commit 769d1ee54): added BVOp::Float { kind: FloatOpKind, prec: FloatPrec } as a new BVOp variant rather than a new RustBV variant. Rationale: keeps result encoded as IEEE BV (so all downstream BV ops work), reuses Expression machinery for caching/simplification. build_fp_z3_ast_cached in symbolic/value.rs is the only place that talks to Z3 FP theory. Operands must be RustBVs of width prec.bits() (32 or 64); CmpEq/CmpLt/CmpLe produce 1-bit BVs via ITE wrapping. F16/F80/V128 are NOT supported — float_prec_of in vex/ops.rs returns None for them, falling back to InvalidFloatType.

When a Z3 module-level param needs to be pinned from PyO3-exposed Rust (e.g. smt.random_seed, sat.random_seed, parallel.*), use Z3_global_param_set via z3::set_global_param — NOT z3::Params::set_u32 + Solver::set_params. The solver-level path is empirically broken for these keys (iaol.1 — corrupts the solver, eval returns models violating constraints). The global path takes effect for every subsequent Solver::new but does NOT retroactively modify in-flight solvers, so the call must run BEFORE construction of any solver you want to affect. In RustExplorationManager.init, this means calling _apply_deterministic_z3_globals BEFORE constructing _RustExplorationManager(...). Idempotent — fine to guard with a module-level boolean since the pin is process-global anyway.

Z3 has NO native bitvector Reverse operation. Both Python and Rust decompose to Extract+Concat chains. Z3's bv_rewriter CAN fuse Concat(Extract[h1:l1](x), Extract[h2:l2](x)) when l1==h2+1 into single Extract. Extract is O(1) at bit-blast time. The QF_BV preprocessing pipeline (qfbv_tactic.cpp) runs: simplify → propagate_values → solve_eqs → elim_uncnstr → bv_size_reduction → simplify(som=true,flat=true,local_ctx=true) → simplify(hoist_mul=true) → max_bv_sharing → ackermannize_bv.

z3-hotpath attribution (angr-ovqja.1, 2026-06-23, commit b8e43fce2): counter-based ranking of the Z3-heavy bench set. KEY METHOD finding: wall-time is unreliable even for NON-bimodal benches — csaw_wyvern showed 3.6x z3_check_time_ns variance (141ms stale baseline vs ~520ms x2 fresh runs) at IDENTICAL z3_check_count(2473)/ast-cache counts. Always rank on structural counts (z3_check_count, z3_ast_cache_hit/miss, rust_solver_fork_count, z3_site_eval_upto_count, concretize_total_candidates), use time_ns only as coarse secondary. Hotspot ranking: H1 cold AST export cache / redundant rebuild (0% ast hit on rev250/flareon5/unbreakable_1; csaw rust_expr_eval_count=272261)->ovqja.3 STRONGEST. H2 eval_upto enumeration (sokohashv2=ONE 6.56s call, but enters cold so ovqja.4 warm-seed won't help it). H3 per-fork solver materialize in RustSolverContext::solver() context.rs (~L519): rebuilds fresh z3::Solver + re-asserts whole shared+local vector per fork; rev250 386ms/124 forks, unbreakable_1 254ms/102 forks -> NEW bead angr-2yyao. H4 hard branch-feasibility solves (fairlight z3_site_branch_true=10.9s/36 checks)->ovqja.2 solver tuning. H5 high-volume cheap unsat checks = low value, no child.

Z3 incremental solver discipline audit (angr-li83, 2026-06-02): three areas characterized in docs/advanced-topics/rust_engine.rst 'Solver incremental discipline'. (1) Push/pop never crosses fork boundary — SymContext::fork (context.rs:3432) sets solver=None and push_level=0; child gets lazy-materialized solver from z3_assertions_shared Arc. All in-flight push/pop is balanced inside with_z3_solver closures (check_branch_feasibility, eval_upto, min/max, range_seeded). bare_z3_push_depth invariant tracks any escape; debug_assert at fork. (2) assert_and_track has ONE call site (context.rs:1924) reached only via RustSolverContext.add_constraint_tracked_ast — never called by exploration steady state. Z3 soft-assert API not used at all. (3) Bool::simplify() called only in sample_simplify_skip (context.rs:907) at stride 64; simplified Bool is DROPPED, original sent to solver. Solver-internal preprocessing runs on first check() per batch. Concrete counters from ais3_crackme: z3_check=122 (48 sat + 48 branch_false + 25 branch_true + 1 eval); z3_branch_model_hit/miss = 23/25 (model fast-path skips one direction). z3_materialize=50 (one per state). lineage_* = 0 (default config). Branch check ~617us, satisfiable ~5.1ms each. Filed angr-ogko (P3) for ANGR_Z3_SIMPLIFY_STRIDE env override.

Z3 lazy-fork solver pattern (audit per angr-li83): SymContext::fork (native/angr/src/symbolic/context.rs:3432) sets child solver: Mutex::new(None). z3_materialize_count increments on first solver query per child. Parent's constraints propagate via z3_assertions_shared: Arc<Vecz3::ast::Bool> that is FROZEN on each fork — drained from local.z3_assertions when push_level==0, then shared by Arc::clone with all children. This avoids two failure modes: (a) Z3_solver_translate same-context bug (loses all assertions, see z3-solver-translate-same-context-bug-z3-solver); (b) eager O(n) assertion replay on forks that get pruned before they query. Verified counter: ais3_crackme has z3_materialize_count=50 for 49 found+active states (one per state, exactly once). Pre-pin: avoid trying to share or translate the parent's per-context Z3 Solver into the child — replay from z3_assertions_shared is the only sound path.

z3_materialize_time_ns counter = SymContext::solver() (native/angr/src/symbolic/context.rs) lazily building a fresh z3::Solver and replaying ALL shared+local assertions on first solver access of a forked context (O(n) per fork). Distinct from z3_site_eval (solver.check at CheckSite::Eval). On csgames2018 it is 150ms/45 and is the dominant residual AFTER fork-carries-model-cache landed (see angr-gorvf.18). The model-carry lets pure-eval children skip solver construction, but children that add a constraint / satisfiable-check / branch-fork still pay the replay. Lever to reach <=1.0s: incrementally seed the child solver from the parent rather than full replay (shared-lineage-solver machinery exists but is gated OFF by default, v5a5-slice-4c.3 baby-re BFS-thrash).

z3-source mining round 2 (epic angr-sijyb, 2026-07-26): follow-on to angr-ovqja (closed 2026-07-18), same external/z3 checkout (tag z3-4.13.0). ovqja covered solver-lifecycle + AST/concretize/FFI; this round targeted 3 angles it didn't: (1) claripy<->rustbv AST-structure mismatch behind the hackcon-z3-ast-structure 66s-vs-9s gap -- NEGATIVE RESULT, dead end at the Z3 layer: bv_rewriter.cpp::mk_extract (L718-810) already auto-canonicalizes Extract-of-Extract/Extract-of-Concat via default smt::context preprocessing, and Z3 has NO native BV Reverse op at all (Reverse is lowered to Concat-of-byte-Extracts by the CALLER before Z3 ever sees it, per value_z3.rs:276-279/1200-1202) so there's nothing to normalize; if the 7.5x gap is still real, it's upstream of Z3 (likely differing term/atom counts from lazy symbolic-memory reconstruction, not unnormalized ASTs) -- unmeasured, would need its own Z3_ast node-count comparison. (2) Model nondeterminism behind the 5 bimodal benches -- produced a real candidate: sat.phase=always_false (bypasses the history-dependent phase-cache m_phase/m_best_phase that init_search never resets across push/pop'd checks, sat_solver.cpp ~L1684-2004) survived adversarial review but ONLY as a soundness-gated spike -- filed as angr-sijyb.1; do not run variance experiments before the soundness check (see that bead, ties to avoid-z3-solver-set-params-for-random-seed's corruption precedent on the same sat.*-namespaced solver-params binding path). (3) Parallel/multi-context safety re-check post-work-stealing-scheduler -- NEGATIVE RESULT, reconfirms avoid-z3-parallel-enable independent of the scheduler: parallel_tactical.cpp/smt_parallel.cpp parallelize ONE hard query (cube-and-conquer spawning their own std::thread pool), a different problem shape than our many-independent-queries-across-N-single-threaded-Contexts workload; giveup() (parallel_tactical.cpp:308-319) structurally collapses incomplete sub-solves to Unknown regardless of angr's own threading. Do not re-open without a different Z3-side mechanism. Separate deliverable from this round: bd memory z3-upstream-wishlist (what we'd ask Z3 itself to change, not usage-side ideas).

Z3 model-cache optimization (commit 44fdf6450, 2026-05-01): On a SAT solver.check() call, get_model() is essentially free — Z3 already constructed it during the check. Caching this model lets check_branch_feasibility skip half its Z3 calls: M.eval(cond, completion=true).as_bool() returns the model's value for the branch condition; if true, can_be_true is proven without Z3 (only need to check negation); if false, can_be_false is proven. The cached model also survives add_constraint() calls when the new constraint is consistent with the model — letting it span multiple branch decisions. fairlight: 24.36s -> 10.65s (2.29x). branch_model_hit rate: 100% on fairlight.

Z3 mul2concat=true is a low-risk win on the angr bench matrix (angr-ya00.1, 2026-05-19, commit 764f54a6f): fairlight 21.66s -> 14.46s (-33%) on a 7-sample bimodal median, no regression beyond +0.8% on 8 other Z3-heavy benches. mul2concat rewrites x*2^k -> concat(x, 0^k), avoiding quadratic mul-by-shift blowup. Now set unconditionally in build_solver_params (native/angr/src/symbolic/context.rs).

z3-param survey on BUCKET-B (bimodal) benches — dva9j.2, NEGATIVE (extends z3-param-survey-negative-result to the bimodal set). Candidates som/bit2bool/local_ctx/pull_cheap_ite (all =true) via ANGR_Z3_PARAMS env (see angr-z3-params-env-override). KEY MEASUREMENT PITFALL: on bimodal benches (unbreakable_1, sokohashv2) z3_check_time_ns is NOISE-DOMINATED — baseline-vs-baseline swings +218% (unbreakable_1) / +20% (sokohashv2) with NO param change. The STABLE metric is rust_run_loop_time_ns (743-789ms unbreakable_1, within 6%); z3_check is useless for single-shot A/B on parallel/wave-mode benches because checks run off the run-loop thread. No candidate moved run_loop beyond noise; none regressed the baby-re guard (all +1.6..+4.7%, sat/unsat counts identical -> semantics preserved). Adopt nothing. angry-reverser skipped (avoid-list 35-67s OOM; same slow-mode class as sokohashv2 -> foregone). Real bimodal lever = qfbv tactic (ovqja.5), not Z3_solver_set_params knobs.

z3-hotpath param survey (angr-ovqja.2) NEGATIVE RESULT. Surveyed Z3 4.13 QF_BV-relevant solver params via the ANGR_Z3_PARAMS env override (no rebuild needed; see angr-z3-params-env-override) A/B'd on ekopartyctf2016_rev250 and csaw_wyvern with run_single.py --counters-json + bench_diff.py. Candidates: relevancy=0, bv.size_reduce=true, smt.bv.eq_axioms=false, cache_all=true, and relevancy=0+bv.size_reduce combined. ALL deltas (-3.5%..+1.0% on z3_check_time_ns / z3_site_satisfiable_time_ns) fell INSIDE the measured run-to-run noise floor: a baseline-vs-baseline rerun on the same bench swung rust_run_loop_time_ns by 1.9% and z3_check_time_ns by 0.2-0.8% with NO param change. Deterministic counters (z3_sat_count/z3_unsat_count) were unchanged for every candidate, confirming semantics preserved but no search-effort reduction. CONCLUSION: adopt nothing. Z3 4.13 QF_BV autotuned defaults + the two params already baked into build_solver_params (bv_extract_prop=true, mul2concat=true) are optimal for our symbolic-CTF workload; pure solver-param config offers no measurable win on top. The real solver levers are the qfbv tactic on bimodal benches (ovqja.5/tactic work), not Z3_solver_set_params knobs. The ANGR_Z3_PARAMS tooling (committed f12e16677) is retained for future A/B surveys.

Background param catalog (from Z3 source mining, kept for future surveys): (1) bv_extract_prop=false by Z3 default — enabling propagates extraction inward through arithmetic, reducing constraint structure (we bake it true). (2) bit2bool=true — converts 1-bit BV to Bool terms. (3) som=true in QF_BV pipeline — sum-of-monomials normal form for arithmetic. (4) local_ctx=true — cheap local context simplifications. (5) pull_cheap_ite=true — hoists simple ITEs. (6) Z3_simplify_ex() available via C API for pre-assertion simplification with custom params. (7) elim_ite=true in bool_rewriter — eliminates ITE in favor of and/or. NOTE: bv_sort_ac is NOT safe — see z3-bv-sort-ac-bench-killer.

native/z3-patched/src/solver.rs:54 has Solver::from_string(s: Into<Vec>) → wraps Z3_solver_from_string. Display impl for Solver at :625 wraps Z3_solver_to_string and produces full SMT-LIB2 (declarations + assertions). SymContext::debug_solver_string() already exposes the to_string side. No need to write FFI shims — both directions exist.

Per-site Z3 check profiling: native/angr/src/symbolic/context.rs has CheckSite enum (Satisfiable/BranchTrue/BranchFalse/Eval/EvalUpto/MinInit/MinSearch/MaxInit/MaxSearch) and per-site count+time atomics. Stats appear in get_solver_stats() as z3_site_count and z3_site_time_ns when count>0. Use this to attribute solver.check() time to call sites when investigating Z3-bound benchmarks.

Z3 push/pop is O(1): just records trail position + reinit stack position + inconsistency flag (~50 bytes). No clause copying. Pop is O(unassigned_vars) — unassigns and shrinks trail vector. Bit-blasting cache survives push/pop (not re-evaluated). Assertions are deferred — Z3_solver_assert() is O(1), just appends to formula store. All preprocessing (rewriting, simplification, bit-blasting) happens during first check() call.

ANGR_Z3_TACTIC=qfbv (angr-ya00, 2026-05-20, commit 2e27425ba) bench impact, 3-sample medians: securityfest_fairlight 18.87->3.04s (-84%, 6.2x), ekopartyctf2016_sokohashv2 9.42->3.68s (-61%, 2.6x), mma_howtouse 6.04->5.63s (-7%). REGRESSIONS: csgames2018 1.04->2.88s (+177%), flareon2015_2 3.51->4.48s (+24%). Shape: qfbv skips Z3 portfolio dispatch and goes straight to bv-specialized pipeline — hash-cracker problems benefit (one big constraint set), CTF binaries with many small checks pay per-check qfbv overhead. NOT shipped as default. Available via env var (Default/Pipeline/QfbvSmart variants in TacticSpec at native/angr/src/symbolic/context.rs).

Z3-roundtrip tests for IR rewrite rules in symbolic::value: must pin every symbolic with concrete values via constraint, then call ctx.eval() — purely structural assertions about the produced RustBV tree miss semantic bugs (e.g., wrong byte order). The 11 tests added in angr-p8cz (commit 2870a3429) at value.rs::tests::test_pre_z3_extract_* and test_extract_over_reverse_* use a raw_extract_node helper that bypasses extract_into to verify the Z3-emission hook independently of the construction-time hook. This is the right pattern for any rewrite that has dual hook points.

z3-rs 0.19 Ast::wrap (impl_ast! macro at z3-0.19.7/src/ast/mod.rs:358) ALWAYS calls Z3_inc_ref internally. So old code passing usize → Ast::wrap was already correct: Bool::wrap takes its own ref independent of whatever the caller did. Net effect of adding Z3AstPtr (inc_ref in ctor, dec_ref in Drop) on top of this pattern: one extra Z3_inc_ref + Z3_dec_ref per assertion (~20ns). Negligible in practice; the bench gate at threshold 0.15 stayed green across all 16 fast-tier benches.

z3-rs 0.19 RoundingMode constructor names use 'towards' (round_towards_zero/negative/positive) NOT 'toward'. Only the 'nearest_ties_to_*' variants drop the directional prefix. Easy to copy-paste from Z3 C API names (Z3_mk_fpa_round_toward_zero) and end up with a compile error. See native/angr/src/symbolic/value.rs build_fp_round_to_int_cached.

Z3 solver params for BV optimization: (1) bv_extract_prop=false by default — enabling propagates extraction inward through arithmetic, reducing constraint structure. (2) bit2bool=true — converts 1-bit BV to Bool terms. (3) som=true in QF_BV pipeline — sum-of-monomials normal form for arithmetic. (4) local_ctx=true — cheap local context simplifications. (5) pull_cheap_ite=true — hoists simple ITEs. (6) Z3_simplify_ex() available via C API for pre-assertion simplification with custom params. (7) elim_ite=true in bool_rewriter — eliminates ITE in favor of and/or.

Z3_solver_translate same-context bug: Z3_solver_translate(ctx, solver, ctx) when source==dest context returns a solver with 0 assertions (all lost). This is the underlying z3-rs Solver::clone() behavior. Fix: create fresh solver + replay cached Z3 Bool assertions instead of translate. Affects all solver forks in SymContext::fork(). The z3_assertions_cache Vecz3::ast::Bool field caches each assertion at assume_true/assume_false/add_constraint_raw time for O(n) replay without RustBV→Z3 AST rebuild.

STALE NOTE (2026-07-26): the ovqja.3 finding below ('RustBV::Expression has no stored ast') is now WRONG -- it shipped and is live. RustBV::Expression carries a memo: RefCell<Optionz3::ast::BV> field, checked/populated at native/angr/src/symbolic/value_z3.rs:65-93 (to_z3_ast/to_z3_ast_cached); a prior top-level conversion is reused via refcount bump rather than rebuilding the whole compound tree, gated only by a thread-local-context liveness check (stale after a context swap, which never happens in production). Confirmed via Explore pass 2026-07-26 feeding into follow-on epic angr-sijyb (z3-mining round 2: AST-structure mismatch, model-nondeterminism, parallel-safety angles this original mining didn't cover).

ORIGINAL (2026-06-23): z3-source mining session (epic angr-ovqja, 2026-06-23): checked external/z3 out to tag z3-4.13.0 (matches runtime lib) and mined it for better-Z3-use ideas in rust-symex. 2 research agents (solver-lifecycle + AST/concretize/FFI) -> adversarial peer review -> 3 beads FILED, 4 REJECTED. FILED (all blocked-by attribution leaf ovqja.1): ovqja.3 persistent per-Expression Z3 AST memo (RustBV::Expression has no stored ast, to_z3_ast rebuilds whole compound tree every call; only Symbolic leaves cached; subsumes a range() single-frame idea) -- NOW SHIPPED, see stale note above; ovqja.4 warm-model seed for eval_upto first solution (narrow: only when model_cache warm at entry) -- also shipped (solving_ops.rs skips a check on iteration 0 of eval_upto); ovqja.5 route qfbv_smart push/pop loops to incremental smt solver (tactic2solver re-bit-blasts every check per z3-4.13.0 tactic2solver.cpp check_sat_core2; opt-in ANGR_Z3_TACTIC only, lowest value) -- DEFERRED, see angr-ovqja.5. REJECTED with reasons: Z3_solver_translate per-fork base-sharing (same-context translate is NOT the bit-blast-sharing primitive assumed; v5a5/3ms1 already cover & rejected this space via BFS-thrash); auto_config=false (same heuristic-witness-corruption class as iaol1-seed-pin-empirically-broken; route vetted param work through ovqja.2 instead); skip snapshot SMT-LIB2 round-trip (cold uncounted path; the round-trip is a deliberate correctness mechanism per hackcon-z3-ast-structure / angr-82g6). Key invariant reconfirmed: production uses a SINGLE thread-local Z3 context (engine.rs set_thread_local), zero production with_z3_context swaps, fork() doesn't swap -- so AST-memo cross-context risk is inert in prod but needs a #[serde(skip)] + with_z3_context regression test.

Z3 universality test pattern for VEX ops with NO claripy reference (angr-tukg.8 added this variant): instead of building a 'Python parity' reference (impossible without an _op_generic_X in claripy), build a 'spec-replay' reference using the SAME RustBV primitives as the helper but inlined in the test. Any encoding drift (wrong cap, swapped then/else branches, off-by-one in extract, sign-bit confusion) surfaces as a SAT counter-example — but bugs in the spec itself are NOT caught. This is weaker than full Python parity but still catches structural encoding errors. Use #[cfg(feature='vex-engine-z3')] gate + push()/add_constraint(got._eq(py).not())/pop. Examples: test_vqshl_16x4_symbolic_universal_unsigned, test_vqsal_16x4_symbolic_universal_signed at vex/ops.rs. When checking the bd description / claripy irop.py for _op_generic_X, mention this fallback as an option if no reference exists.

z3-sys 0.10.4 default-feature build (no 'bundled'/'vcpkg'/'gh-release'): probes pkg-config for z3 to get include_paths, then reads Z3_SYS_Z3_HEADER. If env var is unset, it uses the bundled 'wrapper.h' (which contains '#include <z3.h>') with -I flags from pkg-config. So on Debian/Ubuntu with libz3-dev installed, no env var is needed — pkg-config returns /usr/include and bindgen finds <z3.h>. This is the default 'just works' path; previous .cargo/config.toml setup was actively breaking it.

Z3 th_rewriter (invoked during solver preprocessing on asserted formulas) delegates to bv_rewriter.mk_app_core() for BV ops. This means Extract simplification, Concat fusion, and is_eq_bit pattern matching happen AUTOMATICALLY on asserted constraints — but it's extra work compared to just constructing clean ASTs from the start. The th_rewriter also has a special is_eq_bit case (th_rewriter.cpp:148) that can recognize eq(x, bit_value) patterns from our ITE wrapping, but produces different intermediate structure than native Bool assertions.

Z3-universality parity test pattern for VEX ops with explicit angr Python references: when angr/engines/vex/claripy/irop.py defines _op_Iop_X explicitly (e.g. _op_Iop_Reverse32sIn64_x2 at line 599), reconstruct the same Concat pattern using RustBV extract + concat_le_elements, then assert via ctx.add_constraint(got._eq(&py).not()) that the negation is UNSAT. Wrap in ctx.push() / ctx.pop() to keep solver state clean across tests. Use #[cfg(feature='vex-engine-z3')] gate. Example: test_vec_reverse_32in64_x2_symbolic_matches_python_ref in vex/ops.rs. Key detail: claripy's bit-index convention (arg[127:96] = high 32 bits) maps to RustBV.extract(127, 96, &ctx) with the same indices; concat_le_elements indexes 0 → LSB so push slices in LSB→MSB order.