Я работаю с Python API Z3, пытаясь включить его поддержку в инструмент исследования, который я пишу. У меня есть вопрос относительно извлечения неудовлетворительного ядра с помощью интерфейса Python.

У меня есть следующий простой запрос:

(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)

Выполнение этого запроса через исполняемый файл z3 (дляZ3 4.1), Я получаю ожидаемый результат:

unsat
(__constraint0)

ЗаZ3 4.3Я получаю ошибку сегментации:

unsat
Segmentation fault

Это неГлавный вопрос, хотя это было интригующее наблюдение. Затем я изменил запрос (внутри файла) как

(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)

Используя обработчик файла, я передал содержимое этого файла (в переменную `queryStr ')) к следующему коду Python:

import z3
...
solver = z3.Solver()
solver.reset()
solver.add(z3.parse_smt2_string(queryStr))
querySatResult = solver.check()
if querySatResult == z3.sat:
    ...
elif querySatResult == z3.unsat:
    print solver.unsat_core()

Я получаю пустой список от unsat_core функция: []. Я использую эту функцию неправильно? Строка документа для функции предполагает, что я должен вместо этого делать что-то похожее на

solver.add(z3.Implies(p1, z3.Not(0 == 0)))

Однако мне было интересно, можно ли по-прежнему использовать запрос как есть, так как он соответствует стандартам SMT-LIB v2.0 (я полагаю), и пропустил ли я что-то очевидное.