Finding simple rewrite rules for the JIT with z3

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

CF Bolz-Tereick demonstrates how they used the z3 constraint solver to prove many of the rewrite rules in pypy, and found a few that they had not yet included.