Pracuję z Python API z Z3, próbując włączyć obsługę tego w narzędziu badawczym, które piszę. Mam pytanie dotyczące wyodrębniania niezadowalającego rdzenia za pomocą interfejsu Pythona.

Mam następujące proste zapytanie:

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

Uruchomienie tego zapytania za pomocą pliku wykonywalnego z3 (dlaZ3 4.1), Otrzymuję oczekiwany wynik:

unsat
(__constraint0)

DlaZ3 4.3, Otrzymuję błąd segmentacji:

unsat
Segmentation fault

To nie jest główne pytanie, chociaż była to intrygująca obserwacja. Następnie zmodyfikowałem zapytanie (wewnątrz pliku) jako

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

Używając programu obsługi plików, przekazałem zawartość tego pliku (w zmiennej `queryStr ') do następującego kodu Pythona:

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()

Otrzymuję pustą listę z funkcji `unsat_core ': []. Czy korzystam z tej funkcji nieprawidłowo? Dokumentacja funkcji sugeruje, że zamiast tego powinienem robić coś podobnego

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

Zastanawiałem się jednak, czy nadal możliwe jest użycie zapytania, ponieważ jest ono zgodne ze standardami SMT-LIB v2.0 (jak sądzę) i czy brakowało mi czegoś oczywistego.