New model-based array procedure
Updates to model-based array solver
Minor fixes to bv and theory_engine
Added assertion
Fixed bug in arrays
Fixed a warning, made eager-index default to true (better for QF_AUFBV)
some Java bindings fixes (fixes Debian build problems)
fix memory corruption in arrays destructor
removing cryptominisat since we're not using it
Merge branch 'master' of github.com:CVC4/CVC4
make Boolean term conversion partially non-recursive (resolves bug 501)
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.