Satisfiability Modulo Theories for Finite Domains