Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories