  We present a new procedure to infer size bounds for integer programs
automatically. Size bounds are important for the deduction of bounds on the
runtime complexity or in general, for the resource analysis of programs. We
show that our technique is complete (i.e., it always computes finite size
bounds) for a subclass of loops, possibly with non-linear arithmetic. Moreover,
we present a novel approach to combine and integrate this complete technique
into an incomplete approach to infer size and runtime bounds of general integer
programs. We prove completeness of our integration for an important subclass of
integer programs. We implemented our new algorithm in the automated complexity
analysis tool KoAT to evaluate its power, in particular on programs with
non-linear arithmetic.
