Implements solving for nonlinear integer arithmetic using incremental linearization. This module was implemented in [26] based on [1].