SmtEngine::checkModel() now checks that model values are of the correct type (related to bug #569).
Add operator support (resolves bug #563).