The satisfiability modulo theories (SMT) problem refers
to the problem of determining whether a formula in predicate logic is satisfiable
with respect to some theory. A theory fixes the interpretation/meaning of certain
predicate and function symbols. Checking whether a formula in predicate logic is
satisfiable with respect to a theory means that we are not interested in arbitrary
models but in models that interpret the functions and predicates contained in
the theory as defined by the axioms in the theory.