This module is meant to be used for solving nonlinear integer arithmetic problems by encoding them into bitvector arithmetic formulas (as done in smtrat::IntBlastModule), as described in [20] and [19], both (heavily) inspired by [10]. This approach heavily benefits from knowing bounds on individual variables, both in terms of its ability to find infeasibility and its performance in general.

In this module, we use smtrat::ICPModule to infer new bounds and call the backend incrementally with growing bounds until the computed upper bounds are met.