Oh and there's one other ridiculously cool feature that would go nicely with this blog post about "thinking like a compiler" and that's BitVec
Some info here https://www.josephkirwin.com/2017/11/16/constraint-solver-ti...
Essentially though, you can model fixed width integers signed/unsigned using that and make assertions on things like integer overflow or change in signed-ness.
Uwaterloo did some work to abstract Strings ontop of BitVec so you can include them in your solver state too, worth a look to people that like this content https://z3string.github.io/
Alive/Alive2 [1] is one of the most famous frameworks for compiler transformation verification using BitVec logic