Better check-models output for some kinds of problems; add anassertion that the master equality engine is consistent when it needs to be.

This is intended to help root out some recent model-generation bugs.