По совету Петра Георгиевича после z3 решил попробовать солвер cvc5.

У него есть API, который почти полностью повторяет синтаксис z3 — надо просто заменить импорт на from cvc5.pythonic import * и убрать z3.. (Ну или в стиле злодеев сделать import cvc5.pythonic as z3). Однако данные из модели выковыриваются немного по-другому: вместо

model.eval(el).as_long()

надо писать

model[el].ast.getIntegerValue()

С получением результатов еще связан один очень дебильный баг (и это не только у меня руки кривые).

Несмотря на то, что cvc5 побеждает на конкурсах, на моей машине работал он ощутимо медленнее. Если z3 решил судоку за 100мс примерно (и это с учетом запуска интерпретатора), то cvc5 пыхтел аж 9,5 секунд. Решение для магического квадрата 5x5 он не нашел. А для рюкзака нет аналога Optimization из z3.

За разумное время последние две проблемы я решить не смог. Вообще cvc5 показался существенно менее дружелюбным к пользователю с точки зрения документации и настройки по сравнению с z3. С учетом ниши, которую я описывал ранее, z3 выглядит более адекватно.