Это универсальный феномен, по-видимому: все пытались убедить SMT отдаться, но решали форсом различных степеней брутности и терабайтом рама(тм). Вообще я в процессе получил сносно удовольствия, но по послеконтестному дискурсу начинает казаться, что задачка все-таки была дрянь. Кстати, в одной из статей организаторов, которые гугл любезно выдает сверху на program synthesis, бесцикловые функции сравнимой сложности генерились SMT солвером за ~час.