Home / Topics / 6

Z3 solver stats & check discipline

17 memories · 10 remembered, 7 forgotten (59% kept).

Label

Written by llm:claude-sonnet-5-5 on 2026-10-15T04:35:22Z. Change it with angr-memories topics label 6 "<label>".

Key prefixes

invariant 7 · z3 4 · v5a5 3 · avoid 2

Nearest the centre

invariant-z3-counters-are-process-wide, invariant-z3-solver-stats-keys, v5a5-step-1a-landed, invariant-z3-ast-cache-counters, avoid-check-assumptions, z3-rlimit-cumulative-not-per-check

Members

• avoid-check-assumptions
• avoid-z3-optimize-for-min-max
• invariant-counter-bump-at-construction-not-entry
• invariant-memo-payoff-is-repeats-not-share
• invariant-saved-check-total-excludes-ast-memo
• invariant-solver-pop-underflow-guard
• invariant-z3-counters-are-process-wide
• invariant-z3-solver-stats-keys
• z3-rlimit-cumulative-not-per-check
• z3-timeout-param-is-not-a-termination-bound
• invariant-z3-ast-cache-counters
• showcase-solver-instrumentation-demo
• v5a5-alt-d-assumptions-measured-negative
• v5a5-bare-z3-push-depth-counter-design
• v5a5-step-1a-landed
• z3-per-site-profiling
• z3-push-pop-is-o-1-just-records