Yes. Z3 is impressive. I intend to do a write-up of how I chose to model Python values in it soon.