Craig interpolation has become a key ingredient in many symbolic model
checkers, serving as an approximative replacement for expensive
quantifier elimination. In this paper, we focus on an interpolating
decision procedure for the full quantifier-free fragment of Presburger
Arithmetic, i.e., linear arithmetic over the integers, a theory which
is a good fit for the analysis of software systems. In contrast to
earlier procedures based on quantifier elimination and the Omega test,
our approach uses integer linear programming techniques: relaxation of
interpolation problems to the rationals, and a complete
branch-and-bound rule tailored to efficient interpolation. Equations
are handled via a dedicated polynomial-time sub-procedure. We have
fully implemented our procedure on top of the SMT-solver OpenSMT and
present an extensive experimental evaluation.