  We present a generic tree-interpolation algorithm in the SMT context with
quantifiers. The algorithm takes a proof of unsatisfiability using resolution
and quantifier instantiation and computes interpolants (which may contain
quantifiers). Arbitrary SMT theories are supported, as long as each theory
itself supports tree interpolation for its lemmas. In particular, we show this
for the theory combination of equality with uninterpreted functions and linear
arithmetic. The interpolants can be tweaked by virtually assigning each literal
in the proof to interpolation partitions (colouring the literals) in arbitrary
ways. The algorithm is implemented in SMTInterpol.
