Incorrect SAT on NRA formula

[muchang]

Hi,
For this formula:

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

z3 reports sat and gives the following model:

  (define-fun n () Real
    (- 1.0))
  (define-fun g () Real
    1.0)
  (define-fun d () Real
    (- 1.0))
  (define-fun f () Real
    (- (/ 1.0 2.0)))
  (define-fun b () Real
    0.0)
  (define-fun o () Real
    1.0)
  (define-fun j () Real
    1.0)
  (define-fun i () Real
    0.0)
  (define-fun k () Real
    1.0)
  (define-fun e () Real
    (- 1.0))
  (define-fun a () Real
    (- 1.0))
  (define-fun c () Real
    (- (/ 1.0 2.0)))
  (define-fun h () Real
    (- 1.0))

If I feed this model to the formula, z3 will report unsat.

z3-4.8.6 also has this bug.
z3-4.8.5 doesn't have this bug.

OS: Ubuntu 18.04
Revision: a424ab9