Может ли Z3 проверить выполнимость рекурсивных функций на ограниченных структурах данных?

Я знаю, что Z3 не может проверять выполнимость формул, содержащих рекурсивные функции . Но мне интересно, может ли Z3 обрабатывать такие формулы для ограниченных структур данных. Например, я определил список длиной не более двух в моей программе Z3 и функцию с именем last , чтобы вернуть последний элемент списка. Однако Z3 не завершает работу, когда его просят проверить выполнимость формулы, содержащей last .

Есть ли способ использовать рекурсивные функции над ограниченными списками в Z3?