Отслеживание SAT-ограничений в Z3

Question

У меня есть некоторые ограничения, касающиеся битвекторов, которые, как я считаю, должны быть sat, хотя Z3 выдает вердикт unsat.Мне удалось сократить их до небольшого примера.

Я попытался отследить решатель, запустив z3 -tr:sat test.smt, но не получил никаких следов (он просто говорит unsat).Есть идеи, почему это не работает, или альтернатива отладке ситуаций такого типа?

Answer 1

Возможно, вы захотите пометить ваши ограничения, а затем попросить ненадлежащее ядро. Это позволит вам увидеть, какой (надеюсь, небольшой) набор ограничений окажется конфликтующим и отладить оттуда. Если вы опубликуете свой пример, мы поможем вам настроить его для производства несфокусированных ресурсов.