The inference of program invariants over machine arithmetic,
  commonly called bit-vector arithmetic, is an important problem in
  verification. Techniques that have been successful for unbounded
  arithmetic, in particular Craig interpolation, have turned out to be
  difficult to generalise to machine arithmetic: existing bit-vector
  interpolation approaches are based either on eager translation from
  bit-vectors to unbounded arithmetic, resulting in complicated
  constraints that are hard to solve and interpolate, or on
  bit-blasting to propositional logic, in the process losing all
  arithmetic structure. We present a new approach to bit-vector
  interpolation, as well as bit-vector quantifier elimination (QE),
  that works by lazy translation of bit-vector constraints to
  unbounded arithmetic. Laziness enables us to fully utilise the
  information available during proof search (implied by decisions and
  propagation) in the encoding, and this way produce constraints that
  can be handled relatively easily by existing interpolation and QE
  procedures for Presburger arithmetic. The lazy encoding is
  complemented with a set of native proof rules for bit-vector
  equations and non-linear (polynomial) constraints, this way
  minimising the number of cases a solver has to consider.