fixed bug 502; now the core bv solver only gives the model for variables and shared terms.
Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previously-failing testcase.
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