Been trying out Souper, which uses Z3 underneath. It is pretty spectacular, what it is able to do.

I struggled to find it on my phone, so here is a link. Souper is a LLVM optimizer; https://github.com/google/souper