Efficient Interpolant Generation in Satisfiability Modulo Theories