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