z3 - floor をステートメントではなく式として実装する

Question

発言ではなく、表現として使えるように床を表現することはできますか？Yices では、次のようなことができsatます(= fooInt 5)。

(define floor::(-> x::real (subtype (y::int) (and (<= y x) (< x (+ y 1)))))) 
(define fooReal::real 11/2)
(define fooInt::int)
(assert (= fooInt (floor fooReal))

Z3 で取得できる最も近いものは次のとおりです (Z3 は依存型をサポートしていないためだと思います)。

(declare-const fooInt Int)
(define-fun fooReal () Real 5.5)
(assert (and (>= fooReal fooInt)(< fooReal (+ fooInt 1))))

式としての Floor は、Z3 入力を生成している AST とより厳密に一致するため、理想的です。明らかな解決策を見逃していたら、申し訳ありません。