how to get constraint of variable in Fixedpoint using z3?

I wish to get the constraint of the element in the fixedpoint phi like d>=0.0, how to realize it in Z3?

(set-option :produce-models true)
(set-option :dl_engine 1)
(set-option :dl_pdr_use_farkas true)
(declare-var c Real)
(declare-var d Real)
(declare-var lambda Real)
(declare-rel phi(Real))
(rule 
   (=>
      (and
        (>= lambda 0.0)
        (phi c)
      )
      (phi (+ c lambda))
   )
)
(rule 
    (=>
       (= c 0.0)
       (phi c)
    )
)
(rule
     (=>
        (phi c)
        (phi d)
     )
 )
(query (phi d))

There are two main options for getting information back from the fixedpoint engine. :print-answer true will cause the engine to display one or more instances that satisfy the query (depending on the engine). :print-certificate true will cause the engine to print a trail to explain the answer. If the query cannot be satisfied, it the PDR engine will print a certificate that the query is empty (if it converges, of course).

Currently the dl-engine prints answers (when the query is satisfied)
as a conjunction of the predicates along the trace that satisfy the query. So:

(query (phi d) 
  :print-answer true)

will return:

sat
(and (query!0 0.0) (phi 0.0))

meaning that the value 0.0 can be derived. I am planning to change this format in future releases as the format is not really consistent, but I hope this will work for you at this point.

You can also call it with:

(query (phi d) 
  :print-certificate true)

and it returns a similar conjunction (but with a pretty-printer that omits the decimal notation).