Поддерживает ли Z3 интерполяцию Крейга

Может ли Z3 генерировать интерполянты Крейга (по крайней мере, для логики высказываний?). Я не нашел его в документации Z3.