Z3 get-answer returns unsupported

Question

I'm using the fixedpoint engine in Z3 to encode several universal horn formulas. The query turns out to be unsat. In Z3Py, using get_answer() returns the valuations to the uninterpreted relations. However, in the SMTLIB2 format, get-answer returns unsupported. Here's my program:

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

The output I am getting using Z3 version 4.3.2 is:

unsat
unsupported
; get-answer

In Z3Py, creating a fixedpoint context fp=Fixedpoint(), and then executing print fp.get_answer() would return the valuations to I, I1 and err. Is there a way of obtaining the same in SMTLIB2 format? Thanks.

Answer 1

The comment section essentially answers the question. The SMT-LIB2 extension for "query" takes attributes like your example illustrates. In fact :print-answer amounts to getting the answer.