TheoryEngineModelBuilder::buildModel() is only called once with fullModel=true, withi...

TheoryEngineModelBuilder::buildModel() is only called once with fullModel=true, within a SAT context.  This fixes some outstanding model bugs.

Committing also a Clark-provided assertion the Model code to ensure the call is only done once per context.

(this commit was certified error- and warning-free by the test-and-commit script.)