v5a5

DURING v5a5 slice 4c.3 step 2 canary measurement (2026-05-24 iter 6, angr-awqp), ais3_crackme was the ONE canary that WON under use_shared_lineage_solver=True: 0.88s -> 0.71s (1.24x faster, 5-sample median). The other three regressed or were neutral (baby-re 6.79x slower, unbreakable_0 1.53x slower, r100 flat). This is the FIRST positive workload signal for the lineage-shared trunk on a real bench. Reason unknown — ais3 has very few states (1-2 active at a time) and short BFS depth, so the BFS-thrash that kills baby-re may simply not happen. Potential follow-up: profile ais3 with the opt-in flag to find the predictor (e.g. active-state count distribution, fork depth, query interleaving pattern) that distinguishes WIN workloads from LOSE workloads. If the predictor is cheap to compute at runtime, runtime-thrash-detection (alternative (c) in angr-3ms1) becomes viable.

alt-a (engine-level per-state query batching) for the v5a5 lineage architecture likely reduces to simply setting use_lifo=True (already a knob in RustExplorationManager). DESIGN PASS 2026-05-23 iter 10 (angr-3ms1 NOTES) found that with LIFO, push_to_active_or_drop pushes successors to back, pop_back retrieves the newest (a direct descendant of the last-stepped state). Consecutive states share a lineage chain → hot-cache hit rate ~100% → no push/pop thrash. The CURRENT BFS default (pop_front) interleaves across siblings, giving thrash. Next experiment: extend bench_lineage_push_pop_vs_assumptions in native/angr/benches/vex_engine.rs with a 'simulated LIFO pop order' variant. If LIFO variant matches per_state_batched (~13ms) instead of BFS-thrash (~32.7ms), Flavor-1 alt-a is confirmed cheaply. Without re-landing the reverted slice 4c.3 (fork-time lineage materialization), only the microbench can test this hypothesis on the main branch — production lineage fires only in the Callable path today. Flavor-2 (lineage-aware stash order) and Flavor-3 (K-step engine batching) are only needed if Flavor 1 doesn't work or BFS exploration order must be preserved.

angr-3ms1 LIFO hypothesis CONFIRMED via microbench (commit 5e59ff48b, 2026-05-23). Two new variants added to bench_lineage_push_pop_vs_assumptions in native/angr/benches/vex_engine.rs: push_pop_lifo_chain (200-deep descendant chain, every switch_to is 0 pops + 1 push) and push_pop_lifo_dfs_tree (depth-8 binary tree DFS-preorder, siblings share FrameId prefixes, transitions amortized O(2) pops + O(2) pushes). Criterion 10-sample medians: push_pop_lifo_chain 10.3 ms (FASTER than per_state_batched 13.2 ms by 22%; 3.16x faster than BFS thrash 32.6 ms); push_pop_lifo_dfs_tree 13.0 ms (matches per_state_batched within 1%; 2.5x faster than BFS thrash). Per-state-solver baselines for LIFO workloads: chain 1.77 sec, dfs_tree 1.56 sec — both ~100-150x slower than the lineage variant, so the shared trunk dominates regardless of access pattern. NEXT STEP: re-land slice 4c.3 (fork-time lineage materialization, with a bare_z3_push_depth correctness gate to fix the fork-inside-push bug), wire a Python-side use_lifo=True default for lineage workloads, and measure baby-re. If baby-re recovers to baseline (~0.72s) or better, Flavor-1 of angr-3ms1 alt-a is the right path. Flavor-2 (lineage-aware stash order) and Flavor-3 (K-step engine batching) remain unnecessary.

v5a5/3ms1 alternative (d) — Z3 check-with-assumptions instead of push/pop — measured NEGATIVE on a synthetic BFS-thrash microbench (commit 561aa838b, 2026-05-23). Spike module: native/angr/src/symbolic/lineage_assumptions.rs (SharedLineageSolverAssumptions with per-frame (tag => assertion) at base + check_assumptions(&tag_list)). Bench: bench_lineage_push_pop_vs_assumptions in native/angr/benches/vex_engine.rs. Workload: 50 states × 10 frames each, 2-frame shared ancestor, 200 queries. Results (criterion 10-sample median): push_pop_bfs_thrash 32.7ms; assumptions_bfs_thrash 68.7ms (2.1x SLOWER); push_pop_per_state_batched 13.1ms; assumptions_per_state_batched 51.9ms (3.9x SLOWER); per_state_solvers_bfs_thrash 1230ms (38x slower than push/pop, but biased by per-iter fresh-solver construction so not a clean comparison). Assumption-based approach loses to push/pop in both workloads — the hypothesised learned-clause preservation never overcomes the per-check overhead of growing assertion tables and check_assumptions bookkeeping. Conclusion: do NOT pursue (d) integration. Remaining 3ms1 alternatives: (a) engine-level per-state query batching — restructures BFS to per-state batching, large engine change, unmeasured; (b) per-state solvers with shared trunk — defeats lineage purpose; (c) runtime thrash-detect + lineage dismantle — preserves materialize-cost where BFS doesn't dominate, sacrifices it where it does, unmeasured. The 6 unit tests and 4 criterion benches stay in the tree as a building block; if any future evidence challenges this verdict, the bench can be re-run.

v5a5-bare-z3-push-depth-counter-design

When testing v5a5 lineage perf, the defcon2016quals_baby-re bench is the canary: 0.72s baseline, will balloon to 4-5s if the lineage solver thrashes across BFS-interleaved cross-state queries. Run with: for i in 1 2 3 4 5; do .venv/bin/python tests/benchmarks/run_single.py defcon2016quals_baby-re --engine rust 2>&1 | grep '^OK'; done — variance is low (within 10% across runs), so any consistent >1.5s reading signals real thrashing.

iter 4 (2026-05-23, commit 2a25fca35) landed step-1b of the angr-3ms1 slice 4c.3 re-land: use_shared_lineage_solver: AtomicBool on SymContext, with PyO3 setter on PyRustSimState (py_set_use_shared_lineage_solver), and a use_shared_lineage_solver=False kwarg on RustExplorationManager.init that pushes the flag onto every seed state in _add_rust_state. The child SymContext::fork inherits the parent's AtomicBool value, so a single setter call on a seed state propagates the opt-in to every descendant without per-fork plumbing. Default off keeps slice-1c's gate inert. 2 new Rust unit tests + 2 new Python integration tests (test_init_kwarg_use_shared_lineage_solver_default_off, test_init_kwarg_use_shared_lineage_solver_on); 928 Rust + 493 Python tests pass. Step 1c (the materialization gate itself, gating fork-time SharedLineageSolver minting on parent.use_shared_lineage_solver() && parent.bare_z3_push_depth() == 0) is the next slice — tracked in angr-dv0c.

iter 5 (2026-05-24, commit 5631a99d9) landed step-1c of the angr-3ms1 slice 4c.3 re-land: the fork-time SharedLineageSolver materialization gate. SymContext::fork() now mints a fresh SharedLineageSolver and seeds it with frozen_shared as base assertions when BOTH parent.use_shared_lineage_solver()==true AND parent.bare_z3_push_depth()==0; otherwise inherits parent's lineage Arc as before (None default). The parent's own lineage is NOT touched — only the child gets the new lineage. So in opt-in mode, every fork from a None-lineage parent mints a brand-new lineage for the child; the parent keeps lineage=None. Subsequent forks of the child also mint fresh (gate keeps passing), so siblings DO NOT share a lineage Arc — each subtree has its own. This is a literal reading of the bead description ('mint a fresh SharedLineageSolver and install it in the child's lineage'); whether it matches the design intent for 'sharing' will be revealed by the step 2 canary (angr-awqp). 5 new Rust unit tests; 933/933 lib + 493/493 Python + 15/15 gate pass.

iter 12 (2026-05-23, commit f7d0fa27a) landed step-2 of the angr-3ms1 Flavor-1 plan: added exploration_strategy='bfs'|'dfs' kwarg to RustExplorationManager.init. The kwarg wires through self.set_exploration_strategy(...) (rust_manager.py:3086) so validation lives in one place. Default unchanged (bfs). Added 3 regression tests under TestExplorationStrategy in tests/engines/test_rust_exploration.py: test_init_kwarg_strategy_dfs / _bfs_default / _invalid. 491/491 passed (one Z3 nondeterminism flake on test_model_stability_constraint_order; passes on retry). This is PREP-ONLY — without slice 4c.3 re-land the lineage barely fires on benchmarks (Callable path only). DOES NOT change defaults; users still get BFS unless they explicitly opt in. The next iteration's job: re-land slice 4c.3 (fork-time SharedLineageSolver materialization) gated by bare_z3_push_depth==0 (per v5a5-bare-z3-push-depth-counter-design), then measure baby-re via run_single.py with exploration_strategy='dfs'.

v5a5/hk7k design decision (2026-05-22): SharedLineageSolver uses globally-monotonic FrameId (AtomicU64) for prefix matching, NOT Arc::ptr_eq on RustBV. Reason: ptr_eq is fragile across fork boundaries (RustBV identity can split when cloned). Monotonic id assigned at constraint-add time guarantees: (a) sibling states descended from a common ancestor share the SAME id for every ancestor constraint (because the ancestor's constraints were assigned ids BEFORE either sibling existed), and (b) the constraints added independently by sibling A and sibling B get distinct ids even if they happen to be equivalent BV expressions. LCP by id is O(min(|a|,|b|)) without any Z3 calls. The integration MUST mint a FrameId at the moment a constraint is added to a state (via lineage::mint_frame_id()) and propagate that id into the ScopePath, NOT defer id assignment to fork time.

v5a5/hk7k design refinement (2026-05-23 slice 4c.3-prep). The hot-state cache the design memo calls for can be implemented WITHOUT adding a per-SymContext state_token: when FrameIds are globally unique AND minted only at constraint-add time, '''same tail FrameId at same depth''' is equivalent to '''same path''' (proof: every path containing frame id K descended from the unique state that pushed K, so all paths ending at depth D with tail id K share the same D-1 ancestor frames). This lets SharedLineageSolver::switch_to short-circuit to (0,0) in O(1) with just a length+tail-id comparison, no extra state-identity plumbing needed. The earlier design note in angr-v5a5 description suggested '''track last_state_id''' as the cache key — turns out the implicit FrameId-uniqueness invariant gives us a simpler, plumbing-free implementation that achieves the same goal. Keep this approach until evidence emerges that it misses real-world hot patterns.

iter 5 (2026-05-23) on rust-symex confirmed the v5a5-slice-4c.3-retry-failed-bfs-thrash-fundamental finding by independently re-implementing fork-time SharedLineageSolver materialization. Saw the EXACT same correctness failure (test_fork_inside_push_isolation: ctx_a.satisfiable() returns False after pop+add(z!=20)) that the v5a5-bare-z3-push-depth-counter-design memo predicts — without the bare push-depth gate, lineage materialization clobbers a bare-push frame and y==10 leaks from scope 1 to scope 0. The iter-3 memo explicitly says 'do NOT retry vanilla fork-time materialization expecting different perf — the hot-cache prep is verified necessary-but-insufficient.' iter 5 heeded that and reverted before re-running the bench canary. Filed angr-3ms1 capturing the four architectural alternatives (a) per-state query batching at engine level (b) per-state solvers with shared trunk (c) runtime thrash detection + lineage dismantle (d) Z3 check-with-assumptions instead of push/pop.

angr-v5a5 spike SKELETON landed 2026-05-22 (commit 5b5689e2c). New isolated module native/angr/src/symbolic/lineage.rs adds the SharedLineageSolver + ScopePath + ScopeFrame data structures and switch_to() mechanics, NOT yet wired into SymContext. Key design points: (1) FrameId is globally monotonic AtomicU64 — sibling states share prefix-by-id because ancestor's constraints were assigned ids before either sibling existed; LCP by id is O(min(|a|,|b|)) with zero Z3 calls. (2) ScopeFrame.z3_assertion is the already-derived Bool (post-negation for is_true=false), so push-time is pure z3.assert(). (3) switch_to returns (pops, pushes); same-path-twice is a true no-op (the BFS-thrashing hot path). (4) Telemetry counters (lineage_switch_count/hot/push/pop) ready for get_solver_stats hookup. 9 unit tests pass. The NEXT SLICE wires SymContext::fork to populate a lineage: Option<Arc<Mutex>>, threads solver()/is_sat/eval/min/max through with_solver, and decides base-assertion ownership. The Option-typing lets integration land gradually — None falls back to existing lazy-materialize path.

angr-v5a5 SLICE 2 landed 2026-05-22 (commit e029683d0). SymContext gained two Z3-gated fields: lineage: Mutex<Option<Arc<Mutex>>> and scope_path: Mutex, both starting None/empty and inert in slice 2 (solver() still lazy-materializes; assume_* still appends to local_constraints). fork() captures parent.lineage.lock().as_ref().map(Arc::clone) and installs on child; child.scope_path = empty. Three small accessors added: lineage_arc() (telemetry/debug clone), scope_path_len() (telemetry), and set_lineage_for_testing() (#[cfg(test)] only). Three new lib tests cover: lineage starts None, fork keeps None when parent None, fork Arc::clones parent lineage (verified via Arc::ptr_eq). cargo test --release --lib 894/894, pytest 488/488, perf-neutral. Next slice creates lineage on first fork.

angr-v5a5 SLICE 3a landed 2026-05-22 (commit a4baf9348). Wired super::lineage::lineage_stats() into native/angr/src/symbolic/context.rs::get_solver_stats() and reset_lineage_stats() into reset_solver_stats(). Surfaces 4 new keys via mgr.get_solver_stats(): lineage_switch_count, lineage_switch_hot_count, lineage_push_count, lineage_pop_count. Always 0 today because no fork() yet creates a SharedLineageSolver — slice 3a is pure observability plumbing. New unit test test_lineage_telemetry_surfaced verifies key presence (cannot assert exact values because the LINEAGE_* atomics are global and race with other parallel tests). Lib: 895/895 (was 894). Exploration: 488/488. Bench gate: 15/15. Next slice (3b): introduce SymContext::with_z3_solver(&self, f: impl FnOnce(&Solver) -> R) -> R dispatcher — today a passthrough to self.solver() (lineage branch dead). Slice after that (3c): migrate one or two callers (probably eval/is_sat first). Slice 4: actual fork() lineage materialization (the risky bit). Sequencing was deliberate — observability lands first so when the integration goes in, the impact is measurable on the same commit.

angr-v5a5 SLICE 3b landed 2026-05-22 (commit e66ae95e3). Added SymContext::with_z3_solver(&self, f: impl FnOnce(&z3::Solver) -> R) -> R in native/angr/src/symbolic/context.rs. Pure dispatcher: None branch holds self.solver() (lazy materialize) and calls f; Some branch snapshots scope_path under its mutex (then drops), locks the lineage Arc, and calls SharedLineageSolver::with_solver(&path, f). Locking contract: snapshot scope_path BEFORE locking lineage Arc to prevent deadlock with concurrent solver queries from sibling states. f must not re-enter into with_z3_solver or self.solver() (same invariant as today's direct callers). Two new cfg(test) cfg(feature=vex-engine-z3) tests: test_with_z3_solver_no_lineage_uses_local_solver (assumes x==5, closure sees per-context constraints; inside push/assert(x==42)/pop returns Unsat) and test_with_z3_solver_routes_to_lineage (set_lineage_for_testing(arc), call with_z3_solver, assert lineage_switch_count advanced). Counts post-slice: cargo test --release --lib 897/897 (was 895), engine tests 488/488, run_regression --rust-only --skip-bimodal --threshold 0.15 15/15.

angr-v5a5 SLICE 3c landed 2026-05-22 (commit 76f530947). Migrated the first caller — SymContext::debug_solver_string (native/angr/src/symbolic/context.rs:1234) — from 'let solver = self.solver(); format!("{}", solver)' to 'self.with_z3_solver(|solver| format!("{}", solver))'. Removed #[allow(dead_code)] from with_z3_solver since it now has a real caller. Production behavior unchanged: no SymContext has a lineage Arc installed yet (fork() integration is slice 4), so the None branch fires and lazily looks up self.solver() — same as before. Chose debug_solver_string as canary because it has no Z3 guard returns and no recursive solver paths; reverting is a one-line diff. Verification: cargo check --release clean, cargo test --release --lib 897/897 unchanged, engine tests 488/488 (45.95s), run_regression --rust-only --skip-bimodal --threshold 0.15 15/15. Next: slice 3d migrates a slightly larger caller (assume_true's solver().assert chain around context.rs:1262/1279 is the recommended pick from session.md handoff).

Slice 3d of angr-v5a5: migrated SymContext::add_constraint (context.rs:1278) to with_z3_solver dispatcher. This is the hot path — assume_true/assume_false/add_bv_constraint all funnel through add_constraint, so every fork-driven constraint assert now flows through the dispatcher. Behavior unchanged today (lineage Arc is still None on every SymContext until slice 4 installs SharedLineageSolver on fork). Commit 77a6b1fc9. Verified: cargo check release clean, cargo lib 897/897, test_rust_exploration.py 488/488 (45.7s), run_regression.py --rust-only --skip-bimodal --threshold 0.15 15/15 perf-neutral. Doc comment on with_z3_solver updated to reflect 3c+3d and list remaining callers: eval, is_sat, min, max, check_branch_feasibility, push/pop, transaction_*. add_constraint_raw at line 1261 was NOT migrated this slice — it shares the same one-line assert pattern but its caller set is different (only the Python claripy raw-Z3-ast bridge); decide separately whether 3e migrates it or moves to eval/is_sat next.

Slice 3e of angr-v5a5 landed 2026-05-22 (commit bb0eb64b9). Migrated SymContext::add_constraint_raw (native/angr/src/symbolic/context.rs:1261) from self.solver().assert(&constraint) to self.with_z3_solver(|solver| solver.assert(&constraint)). add_constraint_raw is the unsafe Python-side raw-Z3-AST bridge (called from claripy when a constraint already exists as a Z3_ast pointer in the shared Z3 context); same one-line pattern as slice 3d (add_constraint). Behavior unchanged today (lineage Arc still None on every SymContext until slice 4 wires fork()-time creation). Doc on with_z3_solver updated to list remaining callers: add_constraint_tracked, eval, is_sat, min, max, check_branch_feasibility, push/pop, transaction_*. Verified: cargo check release clean; cargo test --release --lib 897/897; tests/engines/test_rust_exploration.py 488/488 (45.79s); run_regression.py --rust-only --skip-bimodal --threshold 0.15 15/15 perf-neutral. Next slice 3f candidate: add_constraint_tracked at context.rs:1378 (one-line assert_and_track call, same trivial pattern — keeps the warm-up streak going before tackling eval/is_sat/min/max which return non-trivial Z3 guard types). push/pop intentionally deferred: their semantics fundamentally change under lineage (a single shared Z3 stack means push/pop from one state would affect siblings), so they need a real scope_path-aware redesign in slice 4, not a passthrough migration.

Slice 3f of angr-v5a5 landed 2026-05-22 (commit 1b95fe8f4). Migrated SymContext::add_constraint_tracked_indexed (native/angr/src/symbolic/context.rs:1378) off self.solver().assert_and_track(...) onto the with_z3_solver dispatcher. Identical one-line swap pattern to slices 3d and 3e — closure body is solver.assert_and_track(&constraint, &track_bool); both args are already borrowed in the original, no lifetime threading. Doc comment on with_z3_solver updated to record the migration and trim add_constraint_tracked off the still-pending callers list. Remaining callers: eval, is_sat, min, max, check_branch_feasibility, push/pop (deferred to slice 4 — semantics break under shared stack), transaction_* (also deferred to slice 4). Behavior unchanged in production: no SymContext has a lineage Arc installed today, so the None branch of with_z3_solver still fires. Verification: cargo check release clean; cargo lib tests 897/897; pytest tests/engines/test_rust_exploration.py 488/488 (45.78s); run_regression.py --rust-only --skip-bimodal --threshold 0.15 15/15. Next slice 3g candidate: is_sat (one .check() + optional .get_model() — moderate complexity, no recursive entry, first non-trivial migration) OR eval/min/max (model evaluation loops with multi-step solver interactions). Avoid push/pop/transaction_* until slice 4 redesigns them as scope_path-aware. The handoff note at .ralph/state/session.md called this caller add_constraint_tracked but the actual function name is add_constraint_tracked_indexed — only one tracked variant exists in context.rs.

Slice 3g of angr-v5a5 landed 2026-05-22 (commit 4de797fcd). Migrated SymContext::is_sat (native/angr/src/symbolic/context.rs:1492) off self.solver() onto the with_z3_solver dispatcher. First non-trivial migration: returns a value (bool) AND performs an in-closure side effect (post-check get_model() that populates model_cache). Pattern: cache short-circuit happens before with_z3_solver; sat_cache.set(Some(result)) happens after with_z3_solver returns. The get_model() call MUST live inside the closure because model_cache.borrow_mut() needs the same solver that .check() ran against — both must be under the same lock acquisition (same solver, since outside the closure we'd lose the lock). Closure captures self by shared reference for model_cache access; this works fine alongside the &self in with_z3_solver because both are immutable borrows. Doc comment on with_z3_solver updated to record the migration and trim is_sat off the still-pending callers list. Remaining callers: eval, min, max, check_branch_feasibility, push/pop (slice 4), transaction_* (slice 4). Behavior unchanged in production: no SymContext has a lineage Arc installed today, so the None branch of with_z3_solver still fires. Verification: cargo check release clean (7.42s); cargo lib tests 897/897; pytest tests/engines/test_rust_exploration.py 488/488 (45.53s); run_regression.py --rust-only --skip-bimodal --threshold 0.15 15/15. Next slice 3h candidate: eval is the natural follow-up (model evaluation loop, single check + get_model + eval ast under model; similar in-closure-with-side-effect shape to is_sat but multi-step). check_branch_feasibility is more complex (predicted-bool optimisation + conditional check). min/max use push/check/pop and should defer to slice 4.

Slice 3h of angr-v5a5 landed 2026-05-22 (commit 2d37d7724). Migrated SymContext::eval (native/angr/src/symbolic/context.rs:1650) off the direct 'let solver = self.solver();' pattern onto the with_z3_solver dispatcher. First migration with THREE Z3 ops sharing one solver lock acquisition inside the closure: timed_check(solver, CheckSite::Eval), solver.get_model(), and model.eval(ast, true). Pattern decisions: (1) cache short-circuits (concrete value via bv.as_u128(); cached model lookup) stay OUTSIDE the closure — no solver lock needed to hit them, no point acquiring; (2) sat_cache.set() runs INSIDE the closure because it captures the just-completed check's outcome; (3) model_cache.borrow_mut() runs INSIDE the closure too — model_cache is a RefCell separate from the solver Mutex so no nested-locking concern, same as is_sat (slice 3g); (4) the '?' operator on get_model() and model.eval() returns from the CLOSURE (Option), not from eval — so a None model still lets sat_cache.set(Some(true)) have already fired before the closure returns None to the caller, which matches the original behavior. The original 'drop(solver); ... model_cache.borrow_mut()' was historical paranoia — the model object owns its own ref-counted Z3 reference, and model_cache is a RefCell so it doesn't conflict with the solver Mutex guard. Updated with_z3_solver doc comment to record slice 3h. Behavior unchanged in production (no SymContext has a lineage Arc, so None branch fires). Remaining callers: eval_wide (1719), check_branch_feasibility (1575), min (1969), max (2087), push/pop (slice 4), transaction_* (slice 4). Verification: cargo check release clean (7.46s); cargo lib tests 897/897 (1.13s); pytest tests/engines/test_rust_exploration.py 488/488 (45.62s); run_regression.py --rust-only --skip-bimodal --threshold 0.15 15/15. Next slice 3i candidate: eval_wide is the natural follow-up — same check/get_model/eval(ast)/extract pattern as eval, just no model_cache write (eval_wide doesn't populate the cache today). Could batch eval_wide with eval in a future slice if the diff stays tight, but the next-slice author should land it as its own commit to keep blast radius small.

Slice 3i of angr-v5a5 landed 2026-05-22 (commit 08c602e66). Migrated SymContext::eval_wide (native/angr/src/symbolic/context.rs:~1713) off the direct self.solver() pattern onto the with_z3_solver dispatcher. Same three-Z3-ops-under-one-lock shape as slice 3h's eval (check, get_model, model.eval), but returning Option<Vec> via extract_bv_value_wide for widths >128 bits. No model_cache or sat_cache writes — the original eval_wide had neither, so migration was purely mechanical to preserve behavior. Closure return type is Option<Vec>; '?' on get_model() and model.eval() returns from the closure cleanly. Concrete fast path stays outside the closure. Verification: cargo check clean; cargo test --lib 897/897; pytest test_rust_exploration 488/488; run_regression --rust-only --skip-bimodal --threshold 0.15 = 15/15. Behavior inert in production (no SymContext has a lineage Arc; None branch fires). Remaining no-scope-stack callers: check_branch_feasibility. Defer min/max/transaction_*/push/pop to slice 4 (real scope stack work). Next recommended slice: 3j = check_branch_feasibility.

Slice 3j of angr-v5a5 landed 2026-05-22 (commit 5adbe6a20). Migrated SymContext::check_branch_feasibility (native/angr/src/symbolic/context.rs:1575) off the direct 'let solver = self.solver();' pattern onto the with_z3_solver dispatcher. Eighth caller migrated and the last one in the 'no scope-stack' subset before slice 4 lineage materialization. Pattern: the predicted Option calculation (model_cache.borrow().as_ref().and_then(m.eval).and_then(b.as_bool)) lives inside the closure, so acquisition order is solver-then-model_cache (matching pre-slice code). Three-armed match — Some(true): one push/check/pop on bool_ast.not(), Some(false): one push/check/pop on bool_ast, None: two push/check/pop pairs with early return (false,true) from the closure if can_true is false. All push/pop pairs balanced inside the closure, so Z3 scope stack returns to pre-closure depth before f returns — safe under both None (per-context) and Some (shared-lineage) dispatch. Verification: cargo check clean (7.47s), cargo test --release --lib 897/897, pytest test_rust_exploration.py 488/488 in 46.52s, run_regression.py --rust-only --skip-bimodal 15/15 in 20.3s. Remaining direct-solver callers: min/max (push/check/pop binary search across iterations — real scope changes), transaction_*, bare push/pop. All defer to slice 4.

Slice 3k of angr-v5a5 landed 2026-05-22 (commit 777bcf72c). Batch-migration of the FOUR remaining flat direct-solver callers to with_z3_solver in one commit: add_constraints_raw_batch (assert N under one lock); unsat_core (read get_unsat_core and stringify INSIDE the closure, then iterate against constraint_trackers OUTSIDE — keeps the two locks from nesting); get_all_constraints_str (one-line wrap of get_assertions().iter().map(format).collect()); z3_assertion_count (one-line wrap of get_assertions().len()). Bundled because each migration is the same one-line wrap pattern as slice 3c/d/e and individually noise-level — four separate commits would have been churn. With slice 3k COMPLETE the entire 'no scope-stack' subset of direct-solver callers is migrated. The 9 remaining self.solver() call sites (eval_upto:1824, eval_upto_wide:1891, min:2011, max:2126, min_with_hint:2256, can_be_value:2334, push:2349, pop:2358, transaction_*) all manipulate Z3's scope stack across multiple operations and need slice 4's scope_path threading rather than a single with_z3_solver wrap. Verification: cargo check 7.50s clean, cargo test --lib 897/897 in 1.14s, pytest 488/488 in 45.46s, run_regression --rust-only --skip-bimodal 15/15 in 20.2s. Behavior unchanged in production: no SymContext has a lineage Arc yet, so the None branch fires.

Slice 4 (the lineage fork-materialization) is blocked on a constraint-consistency invariant that's bigger than a single session: lighting up fork() to populate SharedLineageSolver MUST coincide with making sure NO direct-solver caller bypasses the lineage. As of slice 3k there are still 9 direct self.solver() callers (eval_upto:1824, eval_upto_wide:1891, min:2011, max:2126, min_with_hint:2256, can_be_value:2334, push:2349, pop:2358, transaction_*) — these all DO scope-stack ops AND don't go through with_z3_solver, so once lineage is Some they'd materialize a stale per-context solver and use it (wrong constraints). Additionally, add_constraint via with_z3_solver Some-branch ASSERTS-AT-TOP-OF-STACK rather than appending a ScopeFrame to scope_path — so after fork the first assume_true puts the new constraint at base level (scope 0 if scope_path is empty), making it visible to ALL siblings instead of just the asserting state — corrupts the lineage. Recommended slice 4 plan: (a) migrate the 9 scope-stack callers to a NEW dispatcher with_z3_solver_scoped that accepts a closure with controlled push/pop semantics on scope_path; (b) refactor add_constraint/add_constraint_raw/add_constraint_tracked_indexed to append a ScopeFrame to scope_path AND switch_to it when lineage is Some, instead of just asserting; (c) only AFTER (a)+(b) land, light up fork() to materialize a lineage. Without that ordering, slice 4a in isolation would be production-buggy. Skeleton/3a-3k already prepared the data structures, the dispatcher, and the read-only paths — the writes are the remaining hard part.

angr-v5a5 SLICE 4a.1 landed 2026-05-22 (commit 8e08ad871). Migrated SymContext::eval_upto (native/angr/src/symbolic/context.rs:1819) to with_z3_solver. First scope-stack-caller migration after slice 3k closed the no-scope-stack subset. Pattern: outer push/pop is balanced INSIDE the closure (same as slice 3j check_branch_feasibility), so Z3 scope depth returns to pre-closure level before f returns — safe for both None and Some dispatch paths. Inside the closure, n iterations of check/get_model/assert-exclude run under one solver lock acquisition. The 5 remaining balanced-in-one-call callers are eval_upto_wide (:1891), min (:2011), max (:2126), min_with_hint (:2256), can_be_value (:2334); each is a separate 4a.2..4a.6 commit following the same template. The spans-multiple-calls callers (push:~2349, pop:~2358, transaction_) bracket caller-provided work across function boundaries and can NOT use with_z3_solver — they need a separate scope_path API (slice 4b). Verification: cargo check --release clean (7.39s), cargo test --release --lib 897/897 (1.10s), tests/engines/test_rust_exploration.py 488/488 (45.43s), run_regression --rust-only --skip-bimodal --threshold 0.15 15/15 (20.2s, perf-neutral). KEY INSIGHT: the slice-4-blocker-analysis memo recommended a NEW with_z3_solver_scoped dispatcher, but for the balanced-in-one-call subset (6 of the 9 callers) the EXISTING with_z3_solver works — the closure is responsible for leaving Z3 depth unchanged, exactly as slice 3j already demonstrated. The new dispatcher is likely only needed for the spans-multiple-calls subset (push/pop/transaction_) where the work crosses function boundaries.

angr-v5a5 SLICE 4a.2 landed 2026-05-22 (commit 59624d31c). Migrated SymContext::eval_upto_wide (native/angr/src/symbolic/context.rs:1871) to with_z3_solver. Same pattern as slice 4a.1 (eval_upto): outer push/pop balanced INSIDE the closure, n iterations of check/get_model/assert-exclude run under one solver lock acquisition. The byte-array sibling of eval_upto differs only in extract_bv_value_wide and make_bv_from_bytes (constant constructor for arbitrary width); the lock-acquisition and push/pop shape are identical. Closure-parameter timed_check(&solver, ...) becomes timed_check(solver, ...). Doc comment on with_z3_solver updated to record slice 4a.2. Four remaining balanced-in-one-call callers to go: min (:2011), max (:2126), min_with_hint (:2256), can_be_value (~:2334). Spans-multiple-calls subset (push, pop, transaction_*) still deferred to slice 4b. Verification: cargo check --release clean (7.38s), cargo test --release --lib 897/897 (1.11s), tests/engines/test_rust_exploration.py 488/488 (46.00s), run_regression --rust-only --skip-bimodal --threshold 0.15 15/15 (20.3s, perf-neutral). KEY INSIGHT (reaffirmed from 4a.1): for the balanced-in-one-call subset the EXISTING with_z3_solver works — closure is responsible for leaving Z3 depth unchanged. The new with_z3_solver_scoped dispatcher recommended in slice-4-blocker-analysis is only needed for the spans-multiple-calls subset.

angr-v5a5 SLICE 4a.3 landed 2026-05-22 (commit f310f5672). Migrated SymContext::min (native/angr/src/symbolic/context.rs:1998) to with_z3_solver. Third caller in slice-4a sub-batch and FIRST WITH NESTED PUSH/POP. Pattern: outer push/pop brackets a binary-search loop with per-iteration push/check/pop pairs (and, in signed case, an additional has_negative pre-check push/check/pop). All push/pop pairs balanced when closure returns. Witness lookup via cached_model_eval(&ast) stays OUTSIDE the closure (borrows model_cache only, no solver lock); inside closure 'timed_check(&solver, ...)' becomes 'timed_check(solver, ...)' since closure param is already '&z3::Solver'. Closure returns Option so Some(lo) propagates. Doc comment on with_z3_solver expanded to record 4a.3. Verification: cargo check 7.44s clean, cargo test 897/897 1.11s, pytest 488/488 45.74s, run_regression 15/15 perf-neutral 20.4s. Three remaining 4a.4..4a.6 callers (max ~:2116, min_with_hint, can_be_value); session.md previously gave line numbers ~:2256 and ~:2334 for those two but grep finds no current matches — they may not exist yet under those names, or session.md line numbers are stale. Verify before claiming 4a.4.

angr-v5a5 SLICE 4a.4 landed 2026-05-22 (commit 26354e1da). Migrated SymContext::max (native/angr/src/symbolic/context.rs:2116) to with_z3_solver — dual of 4a.3 (min). Same nested-push/pop shape: outer push/pop brackets binary-search loop with per-iteration push/check/pop pairs; signed case has additional has_non_negative pre-check push/check/pop. Mechanical: solver=self.solver() moves into closure, timed_check(&solver,...) becomes timed_check(solver,...), closure returns Option. Witness lookup via cached_model_eval stays outside (no solver lock). IMPORTANT NAMING NOTE: session.md/notes referred to remaining callers as 'min_with_hint' and 'can_be_value' — those functions DO NOT EXIST. The actual names are 'range_seeded' (:2247, takes smallest_known/largest_known seeds — the 'min_with_hint' analog) and 'solution' (:2332, single push/assert/check/pop — the 'can_be_value' analog). Verify with grep before claiming subsequent slices. Verification: cargo check 7.43s clean, lib 897/897 1.14s, pytest 488/488 45.28s, regression 15/15 perf-neutral 20.5s.

angr-v5a5 SLICE 4a.5 landed 2026-05-22 (commit dc609b156). Migrated SymContext::range_seeded (native/angr/src/symbolic/context.rs ~:2255) to with_z3_solver. Pattern is the same as slices 4a.3/4a.4: outer push/pop brackets two binary-search loops each with nested per-iteration push/check/pop pairs; all pairs balanced inside the closure. Inside-closure timed_check uses solver (already &z3::Solver). Closure return type Option<(u128, u128)>. Note: outer max_val is captured by the closure (used to set the second loop's hi), then shadowed by inner let max_val = lo; before the final Some((min_val, max_val)) — same shape as the pre-migration code. After this slice the balanced-in-one-call subset of slice-4a has one caller left (solution ~:2340). cargo check 7.57s; cargo test --lib 897/897 1.14s; pytest 488/488 45.61s; bench gate 15/15 pass 20.6s perf-neutral.

angr-v5a5 SLICE 4a.6 landed 2026-05-22 (commit f552f3cd7). Migrated SymContext::solution (native/angr/src/symbolic/context.rs:2348) from direct self.solver() to with_z3_solver. Single push/assert/check/pop balanced inside the closure — simplest of the slice-4a migrations. timed_check(&solver,...) becomes timed_check(solver,...) since closure parameter is already &z3::Solver. Fast-path concrete check and AST construction stay outside the closure (no Z3 ops). Updated the with_z3_solver doc-comment to record slice 4a.6 completing the balanced-in-one-call subset (6/6: eval_upto, eval_upto_wide, min, max, range_seeded, solution). Verified: cargo check 7.45s clean; cargo test --lib 897/897 (1.06s); pytest 488/488 (45.47s); run_regression --rust-only --skip-bimodal --threshold 0.15 15/15 (20.3s), perf-neutral. Slice 4b (spans-multiple-calls: push, pop, transaction_begin/_commit/_rollback) is next and likely needs a separate scope_path API.

Slice 4b of angr-v5a5 is wrapper-side complete (2026-05-22). Both SymContext::push() and pop() now dispatch through scope_savepoint_push/pop helpers (commits 98722a153 + 2f631c68a). transaction_begin/_commit/_rollback inherit the new dispatch transitively since they delegate to push()/pop() -- no separate migration needed. Only slice 4c remains: actually lighting up fork()-time lineage materialization (constructing a SharedLineageSolver and attaching it to the lineage field of a SymContext when a state forks). Until then the Some branch of both helpers is unreachable in production. Hazard discovered iter 16: regression suite reported a spurious 322% regression on defcon2016quals_baby-re after slice 4b.3 landed -- five single-shot runs were all 0.45-0.47s, well under baseline; cause was warm-up noise inside the batch, not a real regression. Don't trust a single noisy regression result on baby-re; re-run before assuming a real regression.

angr-v5a5 SLICE 4b.1 landed 2026-05-22 (commit b3de8abd9). Introduces scope-savepoint infrastructure on SymContext. New field scope_savepoints: Mutex<Vec> (Z3-gated). New private methods scope_savepoint_push() and scope_savepoint_pop() that dispatch by lineage: None branch directly Z3-push/pops the per-context solver (preserves pre-slice behavior of bare self.solver().push()/pop(1)); Some branch records current scope_path.len() on scope_savepoints, and pop truncates scope_path back to the saved length. No public-API callers migrated yet — push()/pop() and transaction_* untouched. Slice 4b.2 (push migration) and 4b.3 (pop migration) are next. Test-only push_scope_frame_for_testing helper added so unit tests can populate scope_path before checking truncation. Five new tests pass: test_scope_savepoints_start_empty, test_scope_savepoint_none_branch_skips_stack, test_scope_savepoint_some_branch_records_depth, test_scope_savepoint_truncates_scope_path, test_scope_savepoint_nested_lifo. Cargo test 902/902, pytest 488/488, regression 15/15 perf-neutral.

Slice 4b.2 landed (commit 98722a153): public SymContext::push() now calls scope_savepoint_push() instead of bare self.solver().push(). One-line swap as planned. Cache invalidation stays in push() (helper does not touch sat_cache/model_cache). scope_savepoint_push lost its #[allow(dead_code)]; scope_savepoint_pop keeps it until slice 4b.3 wires up pop(). Verification: cargo check clean, cargo test 902/902, pytest 488/488, run_regression 15/15 perf-neutral.

Slice 4c.1 of angr-v5a5 landed 2026-05-22 (commit 4d7d6231c). Migrates SymContext::add_constraint (native/angr/src/symbolic/context.rs:~1294) off self.with_z3_solver(|s| s.assert(&c)) onto a lineage-aware dispatch. None branch: bare self.solver().assert(&c) — byte-identical to the pre-slice behavior. Some branch: mint a fresh ScopeFrame::new(true, constraint.clone()), append to self.scope_path under its mutex, drop the lock, take the lineage Arc lock, call switch_to(&path_snapshot) which pushes the new frame onto the shared Z3 solver in a fresh scope. The 'is_true: true' on the new frame is metadata only — switch_to reads frame.z3_assertion which is the already-derived Z3 Bool (callers do negation in assume_false). The slice-4-blocker-analysis memo identified this as the bug-shaped piece: with_z3_solver Some-branch asserts at scope = scope_path.len() = 0 for a freshly forked state, which would have leaked the constraint to all siblings via the lineage base. Three new unit tests under #[cfg(feature='vex-engine-z3')]: test_add_constraint_none_branch_no_scope_path (None branch leaves scope_path empty); test_add_constraint_some_branch_appends_scope_frame (Some branch mints one frame and switch_to pushes onto shared solver); test_add_constraint_sibling_isolation (two siblings sharing one SharedLineageSolver see independent constraint sets after each adds a different constraint to the same named symbol). Verification: cargo check --release clean (7.40s), cargo test --release --lib 905/905 (1.15s, +3 from 902), make rebuild-cargo built, pytest 488/488 (45.16s), run_regression --rust-only --skip-bimodal --threshold 0.15 15/15 (20.5s, perf-neutral). First batch run flagged spurious 345% baby-re regression — confirmed noise (isolated runs land at 0.46-0.49s vs 0.72s baseline). Remaining 4c work: 4c.2 mirror the dispatch on add_constraint_raw and add_constraint_tracked_indexed (also add_constraints_raw_batch); 4c.3 light up fork()-time lineage materialization in production. The full slice 4 closeout will be 4c.3 — only after all three constraint-add paths are scope-frame aware can production fork() safely mint a real SharedLineageSolver.

Slice 4c.2 of angr-v5a5 landed 2026-05-22 (commit ba6807387). Migrates SymContext::add_constraint_raw (native/angr/src/symbolic/context.rs:~1290) off self.with_z3_solver(|s| s.assert(&c)) onto a lineage-aware dispatch, identical shape to slice 4c.1 for add_constraint. None branch: bare self.solver().assert(&constraint) — byte-identical to pre-slice. Some branch: mint ScopeFrame::new(true, constraint.clone()), append to self.scope_path under its mutex, drop the lock, take the lineage Arc lock, call switch_to(&path_snapshot). The constraint.clone() is a ref-bump on the Z3 AST wrapped from the raw pointer. is_true: true is metadata only — switch_to reads frame.z3_assertion. Three new unit tests under #[cfg(feature='vex-engine-z3')]: test_add_constraint_raw_none_branch_no_scope_path, test_add_constraint_raw_some_branch_appends_scope_frame, test_add_constraint_raw_sibling_isolation. New raw_entry helper lifts a width-1 RustBV's Z3 Bool AST into a raw pointer via std::mem::forget to keep the Z3 ref-count alive until add_constraint_raw rewraps it (matches production claripy bridge shape). Verification: cargo check --release clean (4.54s), cargo test --release --lib 908/908 (1.12s, +3 from 905), make rebuild-cargo built+copied, pytest 488/488 (45.08s), run_regression --rust-only --skip-bimodal --threshold 0.15 15/15 (20.5s, perf-neutral). Remaining 4c work: 4c.2b add_constraint_tracked_indexed (tracker bool plumbing + switch_to); 4c.2c add_constraints_raw_batch (batched fast path — N frames under one lock, single switch_to at the end); 4c.3 light up fork()-time SharedLineageSolver materialization in production (only safe AFTER 4c.2b/c close the remaining constraint-add paths).

Slice 4c.2b of angr-v5a5 landed 2026-05-22 (commit d230baa3f). Migrates SymContext::add_constraint_tracked_indexed (native/angr/src/symbolic/context.rs:1467) off self.with_z3_solver(|s| s.assert_and_track(&c, &t)) onto lineage-aware inline dispatch, same shape as slices 4c.1 and 4c.2. None branch (today's only production path): self.solver().assert_and_track(&constraint, &track_bool) -- byte-identical to pre-slice, full unsat-core fidelity preserved. Some branch (set_lineage_for_testing only): mint ScopeFrame::new(true, constraint.clone()), push to self.scope_path under its mutex, drop the lock, take the lineage Arc lock, call switch_to(&path_snapshot). The tracker still registers in constraint_trackers via the existing block above the dispatch (so the returned index is stable across None/Some), but switch_to uses plain z3.assert(), so unsat-core fidelity is INTENTIONALLY DEFERRED in the Some branch -- get_unsat_core() won't report the tracker on a lineage-installed context. Full lineage-mode unsat-core would require an assert_and_track-aware switch_to and a tracker field on ScopeFrame, queued as future work. Three new unit tests under #[cfg(feature='vex-engine-z3')]: test_add_constraint_tracked_indexed_none_branch_no_scope_path (None: no frame minted; constraint enforced; unsat_core returns BOTH tracker indices for deliberately UNSAT pair, confirming full fidelity), test_add_constraint_tracked_indexed_some_branch_appends_scope_frame (Some: one frame minted; loaded_depth==1), test_add_constraint_tracked_indexed_sibling_isolation (A's tracked constraint not visible from B). Verification: cargo check --release clean (7.5s), cargo test --release --lib 911/911 (+3 from 908), make rebuild-cargo built+copied, pytest tests/engines/test_rust_exploration.py 488/488 (45.74s), run_regression --rust-only --skip-bimodal --threshold 0.15 15/15 (20.3s, perf-neutral). Remaining 4c work: 4c.2c add_constraints_raw_batch (batched fast path, N frames under one local_constraints lock + single switch_to at the end); 4c.3 light up fork()-time SharedLineageSolver materialization in production (only safe AFTER 4c.2c closes the last constraint-add path).

Slice 4c.2c of angr-v5a5 landed 2026-05-22 (commit 6f6aac13c). Migrates SymContext::add_constraints_raw_batch (native/angr/src/symbolic/context.rs:~1397) off the with_z3_solver dispatcher onto its own lineage-aware inline match — same shape as 4c.1/4c.2/4c.2b but with N constraints per call. None branch acquires the per-context solver guard once and asserts all N inside (byte-identical to the pre-slice with_z3_solver call). Some branch mints N fresh ScopeFrame's under one scope_path.lock() acquisition, snapshots, drops the lock, then makes a single switch_to call that walks the divergent suffix and asserts each new frame on the shared solver — N ref-bumps but only one lineage Mutex round-trip. With 4c.2c COMPLETE, all four constraint-add paths are now lineage-aware. Next slice 4c.3 lights up fork()-time SharedLineageSolver materialization in production. Three new unit tests added: test_add_constraints_raw_batch_none_branch_no_scope_path, test_add_constraints_raw_batch_some_branch_appends_scope_frames (3 frames, loaded_depth=3), test_add_constraints_raw_batch_sibling_isolation. cargo test 914/914, pytest 488/488, regression 15/15.

Slice 4c.3 (fork-time SharedLineageSolver materialization in SymContext::fork) attempted iter 21+22 and reverted. Two bugs: (1) CORRECTNESS — child SymContext was built with empty scope_path; when the rust_state_proxy._ensure_solver later forked a successor, the proxy's ctx had the lineage Arc but empty scope_path, so the first query's switch_to([]) popped off in-flight per-state constraints (test_strlen_symbolic_constrained_min_max). Fix: scope_path: Mutex::new(self.scope_path.lock().clone()) at the fork site. (2) PERFORMANCE — even with the correctness fix, defcon2016quals_baby-re regressed ~10x (0.45s→4-5s) because BFS interleaves queries across many states sharing one lineage Mutex, and switch_to(path) thrashes pop-N/push-N on every cross-state query. The unit tests have ≤5 states and don't exercise the BFS thrash pattern. Next attempt MUST include a hot-state/last-loaded cache in SharedLineageSolver to skip switch_to when the next query is on the same state as the previous one; without that BFS contention dominates the per-state materialization savings.

Slice 4c.3 (angr-3ms1 Flavor-1 step 1) cannot be landed as an unconditional fork-time materialization, even with the bare_z3_push_depth gate. Reason: iter-3 already validated the gate (488/488 tests passed) but baby-re still regressed 10x because BFS thrash is fundamental to the workload. Any new re-land MUST: (1) add the bare_z3_push_depth correctness gate, AND (2) tie the materialization itself to an engine-level opt-in (e.g. a flag on RustExplorationManager or on SymContext) that defaults OFF, so BFS workloads keep the current None-lineage behavior. The exploration_strategy='dfs' kwarg landed in iter-12 (commit f7d0fa27a) is one place to wire this — when strategy='dfs', enable lineage materialization at construction. The CI gate (run_regression.py --rust-only --skip-bimodal --threshold 0.15) runs default BFS and would catch the 10x regression on baby-re — do NOT land an unconditional change. This makes slice 4c.3 a 3-piece change (correctness gate + opt-in flag + DFS wiring), not the 1-piece change implied by the design memo. Discovered 2026-05-23 iter 13 while assessing risk before claiming the bead.

Slice 4c.3-prep of angr-v5a5 landed 2026-05-23 (commit caa07ebf5). Adds an O(1) hot-cache fast path to SharedLineageSolver::switch_to in native/angr/src/symbolic/lineage.rs. The check: when target_path.len() == loaded_path.len() AND target_path.last().id == loaded_path.last().id, return (0, 0) immediately without walking common_prefix_len. Justification: FrameIds are globally unique and assigned only at constraint-add time, so the frame at depth K is determined by the state that originally pushed it — same tail id at same depth implies path identity. New atomic LINEAGE_SWITCH_FAST_PATH_COUNT is the strict O(1)-only subset of LINEAGE_SWITCH_HOT_COUNT; surfaced via lineage_stats() ([(name,u64); 5] — was 4). The lineage_stats() callers in context.rs iterate by destructuring so the array shape change is transparent. test_counters_increment was reworked to look up counters by name (closure read(name, snap)) to avoid positional index drift. Three new tests: test_switch_fast_path_counter_only_fires_on_same_path (returns (0,1)→(0,0)→(1,0) and ≥1 fp hit), test_switch_fast_path_deep_path_repeated_reentry (10-frame path re-entered 100x, every switch_to returns (0,0)), test_switch_fast_path_does_not_collide_on_different_tails (same-length, divergent-tail paths return (1,1) — pops/pushes are the race-free behavioral proof since global counters can't prove negative '''did not fire'''). Verification: 917/917 cargo unit tests (+3), 488/488 Python tests, 15/15 bench gate (perf-neutral as designed: no production fork() installs lineage yet).

Slice 4c.3 retry (with hot-cache prep landed in commit caa07ebf5) FAILED AGAIN on 2026-05-23 iter 3. The full fork-time SharedLineageSolver materialization was implemented and tested correctly (488/488 Python tests pass, 919/919 lib tests pass — added bare_z3_push_depth counter to gate materialization on no-outstanding-bare-pushes, plus 3 new tests covering materialization/scope_path-clone/transaction-deferral). Bench canary defcon2016quals_baby-re regressed 10x: 0.46s baseline → 3.89-5.13s (5-sample), same magnitude as the iter21+22 failure. ROOT CAUSE: the hot-cache fast path in switch_to only achieved 15.6% hit rate (15/96 switches) on this benchmark — exactly matching the theoretical 1/N expected hit rate for BFS uniformly interleaving queries across N=5-10 active states. Z3 check time exploded from 25.6ms baseline (29 checks, 0.88ms avg) to 3,972ms with lineage (29 checks, 137ms avg) — a 155x per-check slowdown. The per-check cost increase is NOT explained by push/pop overhead (only ~400 z3 stack ops total) — it's likely Z3's incremental solver re-deriving learned clauses after each push. CONCLUSION: BFS-style cross-state query interleaving is fundamentally incompatible with the shared-lineage architecture. A consecutive-same-state hot cache cannot reduce thrash below the 1/N floor. Future approaches must either (a) batch queries per-state at the engine level (changes BFS to per-state batching), (b) cache solver state per-state (multiple Z3 instances — defeats lineage purpose), or (c) detect thrash and disable lineage at runtime. Reverted to commit caa07ebf5 — bench passes again. Bead angr-v5a5 stays IN_PROGRESS. NEXT TIME: do NOT retry vanilla fork-time materialization expecting different perf — the hot-cache prep is verified necessary-but-insufficient.

angr-3ms1 step 1a landed in commit 692063d63 on 2026-05-23 (iter 14). Added bare_z3_push_depth: AtomicUsize to SymContext at native/angr/src/symbolic/context.rs. Increments after solver.push() in scope_savepoint_push None branch (~line 3149); decrements after solver.pop(1) in scope_savepoint_pop None branch (~line 3193); children inherit parent value at fork() (~line 3094-3097). Public reader: pub fn bare_z3_push_depth(&self) -> usize at line ~3114. 3 new Rust unit tests at end of context.rs test mod. Some branch left untouched — counter stays at 0 there. 926/926 Rust lib + 491/491 Python tests pass. The counter is inert (no consumer yet) — slice 1c is the consumer; slice 1b is the opt-in flag that must land first. The increment/decrement is intentionally placed AFTER the Z3 push/pop succeeds, so an underflow can never reach the fetch_sub (z3-rs panics on under-pop first). debug_assert guards against the case anyway.

angr-awqp (v5a5 slice 4c.3 step 2 canary, 2026-05-24 iter 6) MEASURED with use_shared_lineage_solver=True via new --use-shared-lineage-solver flag on tests/benchmarks/run_single.py (commit e02bef6ac). 5-sample medians (baseline -> opt-in): defcon2016quals_baby-re 0.47s -> 3.19s (6.79x SLOWER, mem 283MB->1434MB), defcamp_r100 0.23s -> 0.23s (neutral, mem +7%), ais3_crackme 0.88s -> 0.71s (1.24x FASTER, mem +13%), google2016_unbreakable_0 0.94s -> 1.44s (1.53x slower, mem +25%). VERDICT: per the bead's explicit acceptance criteria ('if baby-re regresses by ANY amount, the design needs revision'), the flag MUST stay default-off. This reproduces the v5a5-slice-4c.3-retry-failed-bfs-thrash-fundamental finding from iter-3: BFS-thrash dominates the lineage cost on baby-re even with the hot-cache prep (caa07ebf5) and the literal slice-1c semantics (per-fork fresh lineage, no Arc-sharing between siblings). NOTABLE: ais3 actually WON 1.24x — the opt-in is workload-dependent rather than uniformly bad. Step 3 (next) should either (a) tie the flag to DFS so workload selection is automatic, or (b) profile why ais3 wins to find the predictor.

v5a5 slice 4c.3 step 3a (angr-1kqf, 2026-05-24 iter 7): profiled ais3_crackme (WIN 1.24x) vs defcon2016quals_baby-re (LOSE 6.79x slower, 4.07x peak mem) with --dump-counters under use_shared_lineage_solver. KEY NUMERIC DIFFERENCES between WIN and LOSE: (1) avoided_count 0 (ais3) vs 13 (baby-re) — baby-re uses 'avoid' stash via solve.py: sm.explore(find=..., avoid=...) which keeps lineage frames alive on dropped states; (2) lineage_pop_count 24 (ais3) vs 0 (baby-re) — baby-re's BFS tree never collapses back to parents; (3) lineage_switch_hot_count/total ratio 44.7% (ais3) vs 30.2% (baby-re) — better hot-cache reuse on ais3; (4) peak mem growth 1.13x (ais3, +49MB) vs 4.07x (baby-re, +1027MB) — 30x ratio in absolute lineage memory overhead; (5) z3_ast_cache_hit 73 (ais3) vs 0 (baby-re) — categorical difference in solver-call repetition. WALL-TIME ACCOUNTING: ais3 saves 224ms in z3_check + 277ms eliminated z3_materialize, costs +251ms in run_loop overhead (net -200ms wall). baby-re saves 200ms in z3_check + 144ms in z3_materialize, costs +125ms in run_loop AND ~2500ms UNACCOUNTED — likely allocator/Z3 backend pressure from the +1GB lineage memory bloat (not charged to z3_check_time_ns). The dominant cost is invisible to current Rust counters. PREDICTOR CANDIDATES: (A) STATIC: 'avoid_addrs > 0' read off SimulationManager at explore() start — strong signal but brittle (many CTF workloads use avoid). (B) RUNTIME: sample lineage_switch_hot_count/lineage_switch_count after N steps and dismantle if <35%, OR sample lineage_pop_count/lineage_push_count and dismantle if <5%. (C) MEMORY: monitor peak_mem growth rate per state; dismantle if growth rate exceeds e.g. 30MB/state. Cleanest single static heuristic = 'avoid_addrs > 0'. Cleanest runtime heuristic = hot-cache-hit-rate threshold. Recommended next: angr-ua1i (DFS coupling step 3b) is the WRONG direction — both benches use default BFS, the win/lose flip is workload-shape not strategy. Should close ua1i and pivot to alt (c) thrash-detection per angr-3ms1.