Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories