Just published a blog post on the PyPy blog:
'Finding Simple Rewrite Rules for the JIT with Z3'
A hands-on post showing how to use the Z3 API to find simple rewrites of integer operations, such as x & 0 -> 0

https://www.pypy.org/posts/2024/07/finding-simple-rewrite-rules-jit-z3.html

Inspired by conversations with @regehr, @sandmouth, @tekknolagi, thanks everyone for your help! In particular to Max for beta reading and feedback. This wasn't the post I was planning to write, second part coming soon, hopefully 😅