Получение «хорошего» ненадежного ядра с помощью z3 (логика QF_BV)

Я использую решатель Z3 SMT для решения проблемы, которую я выразил в логике QF_BV, используя язык SMTLIB 2.

Модель неудовлетворительна, и я пытаюсь заставить решатель производить неподходящее ядро.

Моя модель состоит из нескольких «обязательных» ограничений, которые я определяю с помощью операторов assert .

Утверждения, которые я хочу учитывать при генерации неподатливых ядер, были определены с помощью конструкции (assert (! (EXPR): named NAME)) .

Z3 дает мне unsat , как и ожидалось. Однако Z3 всегда, кажется, сбрасывает «тривиальное» unsat-ядро, состоящее из ВСЕХ названных утверждений.

Я знаю, что существует подмножество моих названных утверждений, которое является неподтвержденным ядром. Я нашел это ядро ​​с помощью решателя Yices SMT, который часто дает мне относительно меньшие ядра без согласования. Модель Yices такая же, как и модель Z3 (в значительной степени построчный перевод из SMT2 на язык ввода Yices).

Является ли создание "хороших" ядер ненадежного типа функцией конкретного решателя, или есть какие-то общие предложения / изменения, которые я мог бы внести, чтобы помочь Z3 улучшить ядро?