z3
11 remembered, 34 forgotten.
z3-array-bindings-available-in-pinned-version
forgotten
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-c-api-z3-mk-bvadd
forgotten
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.
z3-ast-ptr-design-decision
forgotten
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
forgotten
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-bench-killer
forgotten
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-rc-no-uaf-on-teardown
remembered
clear_worker_local_caches() at worker_thread teardown (exploration/scheduler_pool.rs since the angr-9ke6b.59 split; was scheduler.rs) is eager resource release, NOT a use-after-free guard — the angr-bjk8 / angr-1yge9.9 framing was wrong and was corrected in angr-9ke6b.39. Two independent reasons a cached RustBV cannot dangle: (1) z3-patched Context wraps Rc and every cached AST owns its own Rc clone (struct BV { ctx: Context } in native/z3-patched/src/ast/bv.rs), so ContextInternal::drop -> Z3_del_context only fires when the LAST handle drops, making drop order irrelevant; (2) root Cargo.toml sets panic=abort, so no unwind can skip the call. Generalization: any Z3-lifetime hazard argument written against upstream z3-rs borrow semantics must be re-checked against the Rc-based context redesign (commit d604c1f04) before being trusted.
z3-fast-path-constraint
forgotten
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-ast-refcounting
remembered
Z3 FFI ref-count pitfall: Z3 uses ref-counted ASTs. Calling Z3_mk_fpa_to_fp_bv() and stuffing the raw Z3_ast into a Vec to pass to later FFI calls SEGFAULTs because the intermediate AST may be freed (no one called Z3_inc_ref on it). Fix: wrap each intermediate raw Z3_ast in z3-rs Float/Bool/BV via Ast::wrap (which calls Z3_inc_ref) and HOLD the wrapper alive across every later FFI call. Pattern used in build_fp_z3_ast_cached: convert each operand to a Float wrapper kept in fp_args: Vec, then read .get_z3_ast() inside each FFI call site. See commit 769d1ee54.
z3-fp-build-design
forgotten
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.
z3-fp-conversion-helpers
remembered
Z3 FP conversion design pattern (commit 37983a77b): each conversion kind that has a non-FP or differently-sized operand gets its own build helper, NOT a generalized loop. ConvertItoF takes BV->Float via Z3_mk_fpa_to_fp_signed/unsigned with implicit RNE. ConvertFtoI/Rm takes Float->BV via Z3_mk_fpa_to_sbv/ubv (the dst BV is the final result, NOT routed through Z3_mk_fpa_to_ieee_bv which is only for FP results). ConvertFtoF/Rm uses Z3_mk_fpa_to_fp_float (FP->FP) and DOES need Z3_mk_fpa_to_ieee_bv to extract the dst IEEE bits. Symbolic rm: ITE over 4 concrete-rm results. See build_fp_i_to_f_cached / build_fp_f_to_i_cached / build_fp_f_to_f_cached.
z3-global-param-set-pattern
forgotten
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
forgotten
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-iter-ovqja1
forgotten
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-discipline-li83-audit
forgotten
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-discipline
forgotten
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-is-solver-replay
forgotten
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-mining-round2-sijyb
forgotten
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
forgotten
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-bench-win
forgotten
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-numeral-classifier
remembered
Z3 BV numeral string dispatch (#x hex / #b binary / bare decimal) is centralized in one classifier: symbolic/parse.rs enum Z3Numeral<'a>{Hex,Bin,Dec}::classify. Both bv_codec.rs decoders (extract_bv_value_from_string -> low128, extract_bv_value_wide -> full-width bytes) match on it — do NOT re-open-code strip_prefix("#x"/"#b"). The format!("{bv}") string alloc is inherent (needed to read the numeral); only reached when bv.as_u64() fast path misses (width>64 or non-const). Pure parser tests live in parse_tests.rs (no live Z3). Latent bug angr-ph300.80: parse_decimal_to_bytes mis-right-aligns for width<128 but that path is dead (wide decoder only for >128 bits).
z3-param-survey-bimodal-negative
forgotten
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-param-survey-negative-result
forgotten
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.
z3-patched-api-from-string
forgotten
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.
z3-per-site-profiling
forgotten
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
forgotten
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.
z3-qfbv-tactic-bench-impact
forgotten
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-rlimit-cumulative-not-per-check
remembered
Z3 rlimit (pinned via pin_rlimit in symbolic/context_tests/solver.rs) is a CUMULATIVE per-solver resource budget, not per-check: once one check exhausts it (e.g. a hard-factoring probe), every LATER check on the same solver also returns Unknown. Consequence for min/max timeout tests: a hard sign probe that times out poisons the fall-through bsearch too, so both pre- and post-fix return None. This makes the fabricated-Some(0) failure mode of angr-n0irt.1 (sign probe collapsing Unknown->has_negative=false) UNREACHABLE in-process via the deterministic rlimit path — isolating it would need the wall-clock-only timeout, deliberately avoided because its timer is flaky under parallel cargo test (see HARD_FACTORING_RLIMIT doc). So the n0irt.1 fix is defensive correctness-alignment, and signed timeout tests can only pin the None-on-timeout contract, not discriminate the fix.
z3-roundtrip-test-pattern-for-rewrites
forgotten
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-019-wrap-incref-behavior
forgotten
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-rounding-mode-names
forgotten
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
forgotten
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
forgotten
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.
z3-source-mining-ovqja
forgotten
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-spec-replay-test-template
forgotten
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-build-script-ordering
remembered
z3-sys's build.rs runs FIRST as a dependency, then our crate's build.rs. So 'cargo:rustc-env=Z3_SYS_Z3_HEADER=...' from our build.rs cannot fix z3-sys (it has already finished). The only effective places to set Z3_SYS_Z3_HEADER are: (1) .cargo/config.toml [env] block, (2) shell env before invoking cargo. From our build.rs we can only emit cargo:rustc-link-search/link-arg directives, which DO take effect during our crate's link step. Implication: any 'fix detection in build.rs' approach for the header is structurally impossible — the fix must be removing the bad value from config.toml so z3-sys's own pkg-config probe + wrapper.h fallback can work.
z3-sys-pkg-config-fallback
forgotten
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
forgotten
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-timeout-param-is-not-a-termination-bound
remembered
Z3's timeout solver param is NOT a reliable termination bound in tests: it is enforced by a background scoped_timer thread that flips the context cancel flag, and under a heavily parallel cargo test --release run that timer has been observed not to fire — a gdb backtrace on a wedged run showed the thread genuinely grinding inside Z3_solver_check -> smt::context::search -> bounded_search -> propagate for 20.5h under a 1ms budget (angr-zdakq/angr-x8ocv). The reliable bound is the rlimit solver param: a deterministic resource budget polled by the search loop itself (reslimit::inc), no thread involved. PATTERN (see pin_rlimit + HARD_FACTORING_RLIMIT in symbolic/context_tests/solver.rs): any test that deliberately drives Z3 to Unknown on a hard instance must set BOTH — timeout for the behavior under test, rlimit (100_000 works; sub-second worst case) so a missed timer degrades to a fast Unknown instead of a hang. Apply it AFTER asserting the constraints, via ctx.with_z3_solver(|s| s.set_params(&build_solver_params(ctx.timeout_ms()) + rlimit)) — set_params replaces the param set, so rebuild from build_solver_params or you drop the timeout. VERIFIED: with with_timeout(u32::MAX) the branch-feasibility test still finishes in 0.10s and still sees Unknown, i.e. rlimit alone is what bounds it. Guarded permanently by test_pin_rlimit_reaches_the_solver, which probes rlimit=1 on an EASY query (10<x<20) so a silently-ignored param fails fast rather than hanging.
z3-timeout-test-pattern
remembered
Z3 timeout tests: the lenient SymContext::is_sat (and its Python passthrough RustSolverContext::satisfiable) still collapses Unknown->false, so don't assert on THAT boolean. Since angr-03vl4.62 there IS a decided-only form to assert on: SymContext::is_sat_checked() -> Option (Rust) / RustSolverContext::satisfiable_checked() (Python: bool|None) / RustSimState::satisfiable_checked(), which returns None on Unknown and never writes sat_cache. Three rigs: (a) deterministic in-Rust -- assume an EASY set (10<x<20) then pin the solver rlimit to 1, so the very first check aborts Unknown and restoring rlimit=0 afterwards decides it instantly, no hang either way; see test_is_sat_checked_reports_timeout_as_undecided (context_tests/solver_queries.rs) and state/tests/solver_gate.rs. The rig lives on the context as SymContext::pin_rlimit_for_test (cfg(test), in solving_ops.rs) so tests OUTSIDE symbolic/ can use it -- the solver_build module that owns build_solver_params is private to symbolic/ and cannot be widened to pub(crate) without tripping private_interfaces on timed_check's pub(super) CheckSite arg. (b) from Python -- tight timeout (50ms via RustSolverContext.set_timeout) + 128-bit semiprime factoring with 60+-bit factors, and assert only on WALL CLOCK (returns under ~5s), per TestErrorRecovery::test_z3_solver_timeout_does_not_hang. (c) PARTWAY-undecided enumeration (angr-fs8kb.84): rig (a) starves EVERY check, so an Enumeration can only ever give up on its first one -- it yields undecided with an EMPTY values vec and can never reach a branch that needs a non-empty undecided prefix, or one sitting behind an already-decided query (e.g. AddressConcretizer::concretize_internal's enumeration.undecided arm, which is only reached after a decided range_seeded). For those use symbolic::stop_enumeration_after_for_test(n) (solver_build.rs, cfg(test), re-exported from symbolic/mod.rs): a thread-local allowance consulted by timed_check that forces Unknown at CheckSite::EvalUpto ONLY, after n real checks there -- so the min/max bisection and plain satisfiability checks stay honest and a test can have a decided range alongside an undecided enumeration. Returns an EnumerationFault scope guard: --test-threads=1 shares one thread across tests, so a leaked arming would corrupt the next test. Check-count budgeting: enumerate_distinct/eval_upto_ascending spend exactly one EvalUpto check per solution produced, so allowance == the count the first enumeration asks for lands the fault on the second one (allow +-1 for the warm-model-cache seed, which supplies one value with no check). Prefer (a) when the assertion is about the verdict rather than about not hanging.
z3-universality-parity-test-template
remembered
Z3-universality test patterns for VEX ops (consolidated). FOUR variants used in #[cfg(feature='vex-engine-z3')] tests in native/angr/src/vex/ops/tests_.rs and the symbolic/value__tests.rs family:
(1) Python-parity template: when angr/engines/vex/claripy/irop.py defines an explicit reference (_op_Iop_X — e.g. _op_Iop_Reverse32sIn64_x2), reconstruct the same Concat pattern using RustBV extract + concat_le_elements. Push() -> add_constraint(got._eq(&py).not()) -> assert(!is_sat()) -> pop(). Claripy bit-index convention: arg[127:96] = high 32 bits maps to RustBV.extract(127, 96, &ctx) with same indices; concat_le_elements indexes 0 -> LSB so slices pushed LSB->MSB order. Confirmed for VReverse (Iop_Reverse32sIn64_x2) and VQAdd (Iop_QAdd8Sx8). Examples: test_vec_reverse_32in64_x2_symbolic_matches_python_ref in ops/tests_vec_permute_mul.rs.
(2) Spec-replay template (angr-tukg.8): for VEX ops with NO claripy reference (no _op_generic_X). Build a 'spec-replay' reference using the SAME RustBV primitives as the helper but inlined in the test. Catches structural encoding errors (wrong cap, swapped then/else, off-by-one extract, sign-bit confusion) as SAT counter-example. WEAKER than full parity — bugs in the spec itself are not caught. Examples: test_vqshl_16x4_symbolic_universal_unsigned, test_vqsal_16x4_symbolic_universal_signed.
(2b) Opposite-numbering ISA replay (angr-sqfj8.143): strengthens (2) when the op is specified by a vendor ISA manual whose bit/byte numbering DIFFERS from the implementation's. Write the reference straight from the manual's pseudocode in the manual's own numbering (PPC/IBM: byte 0 = MSB, bit 0 = MSB) while the helper uses little-endian numbering. The two derivations then share no index arithmetic, so it is a genuinely independent check, not an inlined copy — it catches exactly the byte/bit-order confusion that (2) is blind to. Example: vgbbd_be_reference in ops/tests_vec_permute_mul.rs vs VEXOps::vec_bit_mtx_xpose. Companion trick: before agonizing over which index direction a permutation op uses, check whether the permutation is an INVOLUTION — a transpose (and any full reversal) is fixed under simultaneous reversal of both index orders, so the numbering choice provably cannot change the result and the 'silently wrong direction' hazard evaporates.
(2c) Sibling-op identity (angr-0jh0j.61): the other way to escape (2)'s inlined-copy weakness, and PREFER IT over (2)/(2b) whenever the new op is algebraically related to ops already covered. Instead of re-deriving the new op's own lane arithmetic in the test, assert an identity that ties it to two or more PRE-EXISTING dispatch arms, so the reference shares no index arithmetic with the code under test. Canonical example: VMulHi (high half of the widening multiply) is proved by VMull_lane == concat(VMulHi_lane, VMul_lane) over fully symbolic operands — VMull and VMul predate it and derive their lanes separately, so a wrong shift amount, flipped sign/zero extension, or reversed lane order in vec_mulhi breaks the identity. See test_vec_mulhi_symbolic_matches_mull_split in ops/tests_vec_permute_mul.rs. Look for hi/lo splits, widen-then-narrow round trips, and add/sub inverses. ALWAYS mutation-check the identity test (temporarily break the op, confirm the test reds) — an identity that happens to hold for the buggy version too is silently vacuous.
(3) Roundtrip template (angr-p8cz commit 2870a3429): for IR rewrite rules in symbolic::value, must pin every symbolic with concrete values via constraint, then call ctx.eval() — purely structural assertions about RustBV tree miss semantic bugs (e.g. wrong byte order). Use a raw_extract_node helper bypassing extract_into to verify the Z3-emission hook independently of the construction-time hook. Right pattern for any rewrite with dual hook points. Examples: test_pre_z3_extract_, test_extract_over_reverse_ at value_simplify_tests.rs.
When evaluating a new VEX op: (a) check irop.py for op_Iop* or op_generic* — if present use template (1); (b) else, if the op is algebraically expressible in terms of already-covered ops, use (2c); (c) else use template (2), upgraded to (2b) when a vendor ISA manual specifies it; (d) for rewrites with both construction-time and Z3-emit hooks, use template (3).
z3-universality-vs-python-parity
forgotten
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.
z3-upstream-wishlist
remembered
Upstream Z3 wishlist (2026-07-26, grounded in external/z3 tag z3-4.13.0 source reading across angr-ovqja + angr-sijyb mining rounds). NOT actionable beads for this repo -- these require changing Z3 itself, not our usage of it. Reference doc for if/when a future session decides to actually patch and upstream something to Z3Prover/z3 (we have a full local git clone at external/z3, so prototyping is feasible without waiting on upstream). One entry per idea:
(1) HIGHEST VALUE: cheap same-context Solver duplication that shares preprocessed/bit-blasted state. Pain point (angr-2yyao, ovqja): sibling forks in the exploration tree each pay a full re-assert of an identical shared assertion prefix (~3ms/fork measured on ekopartyctf2016_rev250 z3_materialize_time_ns=386ms/124 forks, google2016_unbreakable_1 254ms/102 forks) because Z3's only same-context incrementality primitive is a SINGLE sequential push/pop stack shared by one live Solver object, and Solver::translate (the actual clone primitive) is cross-context-only and re-preprocesses from scratch (confirmed: no cheap same-context clone exists at all in z3-4.13.0). A real angr-side solver-POOL redesign was scoped as a much bigger effort than the payoff justified (angr-mawkv spike) precisely because Z3 doesn't give you the primitive to make it cheap. Proposed Z3-side change: a Solver::fork()-style API that COW-shares the internal preprocessed/bit-blasted assertion-prefix state (something like Z3's own use of persistent/immutable AST sharing extended to solver-internal CNF state) and returns a new Solver whose push/pop stack starts empty on top of that shared base -- i.e. exactly the multi-live-child structure angr's stash model needs (many simultaneous siblings, not one sequential stack). Sketch lands somewhere in src/solver/solver.cpp + whatever backs the incremental SAT state (src/sat/sat_solver.cpp's internal clause database) -- NOT a param flip, a genuine new capability; likely the single biggest engineering lift on this list but also the highest measured payoff since it's the SAME wall multiple independent investigations hit.
(2) Incremental tactic-based solving (tactic2solver). Pain point (angr-ovqja.5): under QfbvSmart, every check() re-bit-blasts the ENTIRE formula from scratch (tactic2solver.cpp::check_sat_core2, confirmed z3-4.13.0) -- push/pop only grow/shrink the assertion vector, no clause reuse across calls, so eval_upto/min/max push/pop loops pay a full re-blast per iteration. Currently low-value for us since qfbv_smart is opt-in-only (ANGR_Z3_TACTIC), but the underlying gap -- tactics don't support incremental re-use the way the plain smt Solver does -- is a general Z3 architecture limitation, not angr-specific. Proposed change: tactic2solver tracking which assertions/subgoal state survived the last run and re-running only the tactic passes affected by the delta, rather than cleanup()+full-rerun. Lands in src/solver/tactic2solver.cpp.
(3) Stable Unknown reason-code enum. Pain point (sijyb thread 3): Z3_solver_get_reason_unknown already exists and IS queryable, but only as a free-text string with an undocumented prefix contract (parallel_tactical.cpp::giveup() itself parses '(incomplete'/'(sat.giveup' by string match) -- conflates permanent giveups (incomplete theory support) with resource exhaustion (timeout/memory/conflict-budget) that might succeed with more budget. Minor, general-purpose gap, not specific to parallel solving -- applies to any solve with a timeout. Proposed change: a stable Z3_UNKNOWN_* enum (INCOMPLETE_THEORY / RESOURCE_TIMEOUT / RESOURCE_MEMORY / RESOURCE_CONFLICTS / ...) alongside the existing string. Small, low-risk API addition; lands in src/api plus wherever reason_unknown() is set across tactics/solvers.
(4) LOWER CONFIDENCE, not clearly worth it: native BV Reverse/byte-swap AST operator. Z3 has zero native support (only OP_RE_REVERSE, a regex op) -- Reverse is always caller-lowered to Concat-of-byte-Extracts before Z3 sees it. A native op would need a new theory-adjacent rewriter rule PLUS bit-blaster support, which is real engineering, and thread-1 mining explicitly noted bit-blasting cost is dominated by flattened CNF regardless of AST sugar -- so this might not even move the needle on solve time, only on term-graph size/readability. Include for completeness, but do not prioritize without first measuring whether term COUNT (not just AST 'unnaturalness') is actually the bottleneck on a real affected bench.
z3-with_z3_context-test-pattern
remembered
When writing a Rust unit test that needs to operate inside a freshly-allocated Z3 context, use with_z3_context(&new_ctx, || { ... }). Pitfall: the closure type is bound by Send + Sync to prevent smuggling Z3 ASTs across context boundaries (Z3_ast/Z3_context are NonNull<Z3*> which are !Send). Workaround: cast pointers to usize BEFORE the closure if you need them for sanity-check assertions (e.g., 'confirm the new context is actually a different pointer'); return usize from the closure for the inside-the-closure values. Don't pass raw Z3 pointers into or out of the closure. Pattern is used in native/angr/src/symbolic/context.rs::test_smtlib2_cross_context_round_trip.