--mcsat --trace mcsat::model::check