Мой опыт работы с такими случаями: все зависит! Это может быть простой вопрос эффективности или что-то более фундаментальное. Возможно, ваша собственная кодировка довольно неэффективна, или, возможно, в z3 отсутствует регистр heuristi c, который отправляет его по неверному пути. (Я нахожу, что смешивание Int с Bool обычно нормально, если вы не пытаетесь закодировать логические логики c с какой-то прикольной арифметикой c.)
Поскольку вы ничего не рассказали нам о своей конкретной проблеме, невозможно догадаться. Но если вы подгоняете его к чему-то достаточно маленькому, чтобы выявить проблему, вы должны подать заявку на https://github.com/Z3Prover/z3/issues и, по крайней мере, разработчики должны взглянуть и высказать одно мнение или Другой. Чем меньше ваш пример, тем лучше. Вы также можете опубликовать это здесь, конечно.