I want to extract Craig's interpolants from a formula which includes String literals too. There are versions of Z3 which support extracting interpolants like McMillan's extension and SMTInterpol and iZ3 which support arithmetic and arrays but none support string. What is the best option for the formulas which have string operations too?
Z3 dropped support for interpolants recently, and it's unlikely they'll add it back anytime soon.
MathSAT supports interpolants, but I don't think it supports strings.
I don't think there's any SMT solver out there right now that supports both strings and interpolants.