Separate model_eval and eval, use model_eval in Z3Model.eval