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

z3 reports unsat, while CVC4 reports sat.
If I feed this model to the formula, z3 reports sat:

(define-fun a () Real (/ 1 12))
(define-fun b () Real 0.0)
(define-fun c () Real 0.0)
(define-fun d () Real (/ (- 13) 12))
(define-fun e () Real (/ (- 1) 12))
(define-fun f () Real 0.0)
(define-fun g () Real (/ 7 6))
(define-fun h () Real 0.0)
(define-fun i () Real 0.0)
(define-fun j () Real (/ (- 7) 6))
(define-fun m () Real 0.0)
(define-fun n () Real 0.0)
(define-fun aa () Real (/ 1 12))

z3-4.8.6 also has this bug.

OS: Ubuntu 18.04
Revision: a424ab9