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
fixed bug 502; now the core bv solver only gives the model for variables and shared terms.
fixed TheoryBool rewriter bug
Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previously-failing testcase.
Fix for iff terms over equalities between the same term and differing constants.
Merging some cleanup work:

* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed
Adding tests for the previous commit.
Adding demand restart.
Adding a restart test strategy to integers.
Cleaning up the demand restart code.
Fixes for two bugs:

* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models

Test cases enabled/added for both.
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)
Adjust release Makefile rules, new run script
update copyrights
One final fix to "make submission" rule