всё, как в тех лекциях (http://www.cs.berkeley.edu/~bodik/cs294fa12) : генерили дерево решения с дырками + функции для заполнения дырок + список ограничений в виде равенств (x, lambda(x))и скармливали Z3, а оно возвращало, есть ли у него решение и если есть - что поставило в дырки.
эээ ... ну, я код там практически не писал, только с SMT2 для Z2 разобрался (он оказался не так уж и сложный. только рекурсию его не удалось заставить генерить) и немного примеров - как это решается на ём. А там уже народ писал код.
Код, похоже, (насколько я разбираюсь в гите) в непубличном репозитории. Но там ИМХО достаточно тривиально : получаем задание - перерабатываем в задачу для z3 и выдаем решение.
Самое смешное - что запустили решатель ~ за три часа до конца конкурса. И поэтому нарешали всего 550+ решений %)