Z3 reports incorrect sat on unsat NRA formula without /

[muchang]

Hi,
For this formula:

(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 j () Real) 
(declare-fun k () Real) 
(assert (or
    (not                  ;false
        (=>               
            (and            
                (= k 1.0)
                (= k 0.0) 
                (<= 1.0 f)) 
            (<= a (+ g b)))) 
    (and                    ;false
        (forall ((?d Real)) ;false
            (and                      
                (or                  
                    (<= 0.0 (+ (- b) ?d)) 
                    (= (- b f) 0.0))      
                (and 
                    (not (= d 0)) 
                    (not (= d 1.0)))))
        (and 
            (exists ((?h Real)) 
                (forall ((?d Real)) 
                    (exists ((?e Real)) 
                        (and 
                            (or 
                                (= j 0) 
                                (not (= (+ (- ?h) (- b f)) 0.0))) 
                            (or 
                                (and (< 0.0 ?h) (= ?e 0)) 
                                (or (<= (- b f) 0.0) (= (- b f) 0))) 
                            (and 
                                (<= 0.0 (+ ?e (* 2.0 ?d) (* (- 2.0) ?h))) 
                                (<= (+ ?d (* (- 2.0) ?h)) 0.00))))))
            (exists ((?h Real))
                (or 
                    (forall ((?e Real))
                        (or 
                            (<= ?h 0.0) 
                            (= (+ ?e f) 0.0)))
                    (and 
                        (or 
                            (not (= (+ (* (- 1.0) ?h) (* 2.0 j)) (- 1.0)))
                            (not (= (+ (* (- 2.0) ?h) (* (- 2.0) j)) 2.0)))
                        (forall ((?d Real)) 
                            (=  (* 2.0 ?d) ?h)))))))))
(assert (= b (+ j f)))  
(assert (= c (* e g)))  

(check-sat)
(get-model)

Z3 will report sat on this unsat formula and with the invalid model, while cvc4 reports unsat:

(model
  (define-fun g () Real
    (- 1.0))
  (define-fun e () Real
    (- (/ 1.0 8.0)))
  (define-fun c () Real
    (/ 1.0 8.0))
  (define-fun f () Real
    (/ 2.0 3.0))
  (define-fun j () Real
    (- (/ 2.0 3.0)))
  (define-fun b () Real
    0.0)
  (define-fun d () Real
    (/ 1.0 2.0))
  (define-fun a () Real
    0.0)
  (define-fun k () Real
    2.0)
)

If I feed this model to the formula, z3 will report unsat. z3-4.8.5 also reports unsat.

OS: Ubuntu 18.04
Revision: e1fd167