I used it to do some tax optimization around ISOs at a newly public company (https://gitlab.com/mbryant/taxoptimizer/-/blob/master/amt.py). It gets pretty slow when you try to look more than a few years out, so I'm guessing writing some optimization logic by hand would've made more sense. Using Z3 here definitely beat me trying to do this on paper like I've seen other people do!