Dolmen provides tools to parse, type, and validate input files used in automated deduction, and in particular problems from the SMT-LIB. We present here an extension of Dolmen which makes it capable of verifying ground models for quantifier-free SMT-LIB problems. While most of the extension was a straightforward implementation of an evaluator for ground expressions, there were some challenges, related to corner cases of the semantics (division by zero, partial functions, . . . ), as well as order of evaluation of statements, most of which could be solved by improvements to the SMT-LIB standard for models.