Things like automatic exploit generation[1] and exploit hardening[2] in particular rely on SMT solvers to accomplish their goals. They allow for some truly remarkable things to be done. Expect skynet to utilize them heavily in its distributed automatic exploit generation (global autopwn) tooling!

1. http://security.ece.cmu.edu/aeg/ 2. http://users.ece.cmu.edu/~ejschwar/bib/schwartz_2011_rop-abs...