This module contains the UF theory solver for the CEGAR loop. It detects model conflicts with function congruence and inserts new congruence lemmas as required (dynamic Ackermannization).
Equations
- One or more equations did not get rendered due to their size.