For the start, I'd agree, but as soon as you want to do non-trivial things, I don't think that standard compiler IRs (e.g., LLVM) are a good way for binary analysis. (POV: been there, done that.) The time investment in fighting the existing IR quickly becomes larger than just writing a custom IR, which is not _that_ much effort. Running O2 optimizations sounds great in theory, but is often not too helpful in practice.
LLVM is clearly intended to provide a (not too large) set of semantics that can be mapped easily to different architectures. This is great for compilation, but not for the other direction, as even simple things like add-with-carry end up being multiple non-trivial instructions which aren't handled by existing optimization patterns. The same goes for vector instructions, where many patterns are encoded in the back-ends and not in the IR passes. So you end up writing custom passes fairly quickly, but still fight against an IR that doesn't allow you to express the things you'd like to have.
In the long run, a custom IR allows for a much more idiomatic code representation and more flexible analyses; not to mention that LLVM-IR is fairly heavy-weight and not particularly efficient. If I were to write another binary translator (I wrote Instrew/Rellume based on LLVM), I would definitely not choose LLVM.
I completely agree on the SMT part. I experimented with SMT, but standard data flow analysis suffice 90% of the time and are much more efficient and predictable.