Disabling eager array index splitting for QF_AX
Made eager lemmas an option, enabled for QF_AX
Turning on model based array solver for QF_AX
Fix regression error by turning off model-based solver when models are on
(ironic, yes, but model-based solver doesn't yet produce models)
spelling
update copyrights
minor adjustments to documentation / interface / #includes; these from Tim's fcsimplex branch, thanks Tim