Напомним, что модели, возвращаемые Z3, можно рассматривать как простые функциональные программы.Ваша формула находится во фрагменте UFBV.Z3 использует несколько модулей для определения этого фрагмента.Каждый модуль преобразует формулу F в «более простую» формулу F' и создает процедуру, которая преобразует модель для F' в модель для F.Мы называем эти процедуры: «модель преобразователей».Преобразователи моделей, например, исключают интерпретации для вспомогательных функций и констант, введенных в преобразовании F в F'.Некоторые вспомогательные определения не могут быть удалены, кажется, они используются для толкования других определений.Мы должны рассматривать их как «вспомогательные функции».Они также создают интерпретацию для символов, которые были исключены ..
В вашем примере происходит следующее: последний модуль создает модель, содержащую символы trans!... и k!....Эта модель для формулы, которая даже не содержит trans.Функция trans была исключена.Поскольку мы применяем конвертеры моделей, интерпретация для trans строится на основе интерпретации всех trans!....На этом этапе символы trans!... и k!... все еще используются, поскольку интерпретация trans имеет ссылку на все символы trans!..., а интерпретация функций trans!... имеет ссылки на символы функции k!....,На этом этапе в модели нет ненужных символов.Однако на более позднем этапе интерпретация trans упрощается путем развертывания определений trans!... и k!....Итак, после этого шага упрощения trans!... и k!... по сути являются «мертвым кодом».
При этом модель, возвращаемая Z3, верна, то есть модель для вашей формулы.Я признаю, что эти дополнительные символы являются раздражающими и ненужными.Чтобы устранить их, мы применили эквивалент шага устранения «мертвого кода».Мы действительно близки к следующему релизу.Таким образом, эта функция не будет доступна в следующем выпуске, но я добавлю ее для следующего выпуска.