This module implements incremental linearization as described in [25], roughly following [4] and [16]. In addition, it implements an ICP-based axiom instantiation.