SMT solvers are built on top of them which can do useful things like crack license keys or do cryptanalysis.

https://zeta-two.com/assets/other/nixucon18-slides.pdf https://github.com/TechSecCTF/z3_splash_class