We introduce a calculus for handling integer arithmetic in first-order
logic. The method is tailored to \Java\ program verification and meant
to be used both as a supporting procedure and simplifier during
interactive verification and as an automated tool for discharging
(ground) proof obligations. There are four main components: a complete
procedure for linear equations, a complete procedure for linear
inequalities, an incomplete procedure for nonlinear (polynomial)
equations, and an incomplete procedure for nonlinear inequalities. The
calculus is complete for the generation of counterexamples for invalid
ground formula in integer arithmetic. All parts described here have
been implemented as part of the KeY verification system.