It is vital to optimize floating-point arithmetic because it is ubiqui- tous, costly, and used in compute-heavy workloads. Implementing precise optimizations correctly, however, is difficult, since devel- opers must account for all the esoteric properties of floating-point arithmetic to ensure that their transformations do not alter the out- put of a program. Manual reasoning is error prone and stifles incor- poration of new optimizations. In this paper, we present an approach to automate reasoning about floating-point optimizations using satisfiability modulo the- ories (SMT) solvers. We implement the approach in LifeJacket, a system for automatically verifying precise floating-point optimiza- tions for the LLVM assembly language. We have used LifeJacket to verify 43 correct optimizations and to discover eight incorrect ones, including three previously unreported problems. LifeJacket is an open source extension of the Alive system for optimization verification