Made eager lemmas an option, enabled for QF_AX
Turning on model based array solver for QF_AX