Нет; SMTLib - это, по сути, теория первого порядка; функции более высокого порядка просто не поддерживаются.
Однако
Z3 позволяет отображать функции на массивы с расширением (_ map f). См. https://rise4fun.com/Z3/tutorial/guide, для поиска «Функции отображения на массивах». Это не дает вам произвольных функций высшего порядка, но может использоваться для имитации тех, которые работают с массивами SMTLib.
Если вы намереваетесь рассуждать о функциях более высокого порядка, то SMTLib, возможно, является для вас неправильной логикой. Использование более традиционного средства доказательства теорем, такого как HOL / Isabelle, или современных воплощений в Agda / Coq было бы более подходящим. Вы также можете взглянуть на Lean, который имеет хороший компромисс между функциями и автоматизацией.