do simple ite rewriting within quantifiers
Disabling eager array index splitting for QF_AUFLIA
Minor changes to model-based array solver
changed option to run inequality solver by default
work on bug 491