Unknown on NIA formula while z3-4.8.7 gives sat

[muchang]

HI,
For this formula,

(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x 0))
(assert (distinct (div (* x y) y) x))
(check-sat)

z3 nightly build gives unknown while z3-4.8.7 gives sat:

[611] % z3 simple.smt2 
unknown
[612] % z3-4.8.7 simple.smt2 
sat
[613] % cvc4 --quiet simple.smt2 
sat
[614] % cat simple.smt2 
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x 0))
(assert (distinct (div (* x y) y) x))
(check-sat)

If x is replaced by 0, then z3 is able to report sat:

[618] % z3 simple2.smt2 
sat
[619] % cat simple2.smt2 
(declare-fun x () Int)
(declare-fun y () Int)
; (assert (= x 0))
(assert (distinct (div (* 0 y) y) 0))
(check-sat)

OS: Ubuntu 18.04
Revision: 55f62fc