Can Z3 generate Craig interpolators (at least for propositional logic?). I did not find it in the Z3 documentation.
No, Z3 does not support Craig interpolation, but generates evidence. Interpolations can be extracted from the evidence. Ken Mcmillan is developing an interpolator generator on top of the Z3 using this approach.