Same. I’d been circling SMT solvers for a while but a recent HN post on knuckledragger[1] (built on Z3) made me finally take a closer look at Z3 itself. It kind of feels like stealing fire.

[1] https://news.ycombinator.com/item?id=41161455