It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things.

I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and either eliminate subtle dead code or generate exploitable invariants (for "free")