Knowing how to use z3 for stuff like this is a superpower that not a lot of people have, but is definitely worth knowing if you work with code that needs to be optimized at this level. I have an mcp script that interfaces with z3, and this comment is a reminder to myself to find some time to expand it in the future for this specific flow.
It’s also worth calling out angr as an interface between capstone and z3, which can take this to another level.