z3 - Z3 の get-answer はサポートされていません

Question

Z3 の固定小数点エンジンを使用して、いくつかのユニバーサル ホーン式をエンコードしています。クエリは unsat であることが判明しました。Z3Py では、get_answer() を使用すると、評価が解釈されていない関係に返されます。ただし、SMTLIB2 形式では、get-answer は を返しますunsupported。これが私のプログラムです：

(declare-var x Int)
(declare-var y Int)

(declare-rel I (Int) interval_relation)
(declare-rel I1 (Int) interval_relation)
(declare-rel err (Int) interval_relation)

(rule (=> (= x 0) (I x) ))
(rule (=> (and (= y (+ x 1)) (I x) ) (I1 y) ))
(rule (=> (and (> y 2) (I1 y)) (err y) ))

(query (err y)
    :engine pdr
:use-farkas true
:print-answer true
)
(get-answer)

Z3 を使用して取得している出力version 4.3.2は次のとおりです。

unsat
unsupported
; get-answer

Z3Py では、固定小数点コンテキストを作成してfp=Fixedpoint()から実行するprint fp.get_answer()と、評価がI、I1およびに返されerrます。SMTLIB2 形式で同じものを取得する方法はありますか? ありがとう。