Soundness issue on NRA formula

[wintered]

Hi,

on the following unsatisfiable formula Z3 reports sat. We fed the model to the formula and got unsat.

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () 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 o () Real)
(assert
 (not
  (exists ((n Real))
   (=> (> d i) (= (<= 0 k) (not (=> (<= 0 n k) (and (= (+ (* b n) h) c) (= n (- d i))))))))))
(assert
 (not
  (exists ((m Real))
   (= (or (< (* l i i) 0 g) (< (+ j o) 0)) (or (< 0 a) (>= (+ (* 6 e) (/ i (* 2 l))) f))))))
(check-sat)

OS: Ubuntu 18.04
Revision: e818b8d