  In this paper, we compare two alternative mechanisms for deciding the
validity of first-order formulas over finite domains supported by the
mathematical model checker RISCAL: first, the original approach of semantic
evaluation (based on an implementation of the denotational semantics of the
RISCAL language) and, second, the later approach of SMT solving (based on
satisfiability preserving translations of RISCAL formulas to SMT-LIB formulas
as inputs for SMT solvers). After a short presentation of the two approaches
and a discussion of their fundamental pros and cons, we quantitatively evaluate
them, both by a set of artificial benchmarks and by a set of benchmarks taken
from real-life applications of RISCAL; for this, we apply the state-of-the-art
SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that
(while SMT solving generally vastly outperforms semantic evaluation), the
various SMT solvers exhibit great performance differences. More important, we
identify classes of formulas where semantic evaluation is able to compete with
(or even outperform) satisfiability solving, outlining some room for
improvements in the translation of RISCAL formulas to SMT-LIB formulas as well
as in the current SMT technology.
