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.