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
Fix get-authors script to not extract email addresses, canonicalize names, add .mailmap
Remove old README file from rewrite-rules left over from new-theory script long ago
Regenerated copyrights: canonicalized names, no emails
Making arithmetic model reversion on unsat checks an option.
abort quantifiers check if master equality engine is inconsistent.
updated NEWS to include inequality solver
Some final minor changes before cutting 1.1.

* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression