Home / Topics / 3

RustBV rewrites & Z3 emission

24 memories · 9 remembered, 15 forgotten (38% kept).

Label

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

Key prefixes

invariant 8 · z3 6 · expression 2 · extract 2

Nearest the centre

invariant-prefer-z3-native-bv-ops, z3-has-no-native-bitvector-reverse-operation-both, z3-ast-construction-c-api-z3-mk-bvadd, value-z3-native-primitives-no-handrolled-ext, behq-root-cause, invariant-z3-construction-canonicalization

Members

• emit-extract-z3-recursion-hazard
• invariant-cmp-pair-zext-direction
• invariant-commutative-canonicalization-active
• invariant-prefer-z3-native-bv-ops
• invariant-reverse-z3-roundtrip-tests
• invariant-signext-extend-bits
• invariant-zext-fold
• value-z3-native-primitives-no-handrolled-ext
• zext-fold-property-test
• behq-root-cause
• expression-canonicalization
• expression-simplification-rules
• extract-driver-unified
• extract-over-reverse-multibyte-rewrite-fix
• invariant-rustbv-rewrite-second-hook
• invariant-z3-construction-canonicalization
• kkpr-canonicalization-scope
• reverse-leaf-emission-root-cause
• z3-ast-construction-c-api-z3-mk-bvadd
• z3-bit-blasting-ite-cost-ite-cond-bv
• z3-has-no-native-bitvector-reverse-operation-both
• z3-roundtrip-test-pattern-for-rewrites
• z3-solver-params-for-bv-optimization-1-bv
• z3-th-rewriter-invoked-during-solver-preprocessing-on