PV3 ⊧ MSATIC3a dedicated property checker for infinite domains

Solver in nuXmv for infinite domains.

Internals

It is used as a back-end solver of nuXmv alongside MathSAT. The IC3 most likely refers to an incremental model checking algorithm for invariance properties.