Incorrect result NRA formula

[wintered]

Hi,

for this unsatisfiable formula, z3 reports sat. Feeding the model to the formula gives unsat.
We cross-checked with z3-4.8.5 and CVC4. Both give the correct answer - unsat.

(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun o () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun q () Real)
(declare-fun p () Real)
(assert
  (or
    (and
      (not
        (exists
          ((ac Real))
          (=>
            (= c e)
            (=
              (= 0.0 b)
              (= (= (<= ac b) (<= 0 h)) (= o 2.0))
            )
          )
        )
      )
      (not
        (exists
          ((a Real))
          (=>
            (and
              (=>
                (<= l 0)
                (and (<= (* c l) (- d)) (<= l k))
              )
              (= f i)
              (<= 0.0 a)
              (<
                (+ i (/ 0 (* 2.0 g)))
                f
              )
              (<= j d)
              (< 0.0 k)
            )
            (< f 0 (/ 0 0) f)
          )
        )
      )
    )
    (not
      (exists
        ((ae Real))
        (=>
          (and
            (=>
              (<= ae m)
              (>=
                (+ n (* (- 5) (* ae ae)) (* ae q))
                0
              )
            )
            (=
              n
              (+ (* 5 (* p p)) (* q p))
            )
            (>= p 0)
            (<= p (/ 6 5))
          )
          (<= (+ m p) (/ 16 5))
        )
      )
    )
  )
)
(check-sat)

Revision: ffc696e
OS: Ubuntu18.04