Fix bug in mbqi=fmc handling theory symbols.  Fix mbqi=fmc models (Bug 557).  Improve datatypes rewrite, make option for previous dt semantics.