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.