- Z3 solver <0.01% of wall time (74 queries, ~0ms) - Real bottleneck: AST walkers + CFG traversal (~85%) - Top optimization: TU pre-filter (skip files with no security ops) - Bitwuzla multi-solver would not help — SMT queries are already fast
