Z3 incorrect model on QF_NRA formula

Hi,
For this formula,
```
(declare-fun a () Int)
(declare-fun b () Real)
(assert (= b (/ 0 a)))
(assert (> b 0))
(check-sat)
(get-model)
```
z3 gives an incorrect model :
```
(model 
  (define-fun a () Int
    0)
  (define-fun b () Real
    0.0)
)
```
in which b = 0 cannot satisfy b > 0.

OS: Ubuntu 18.04
Revision: 5497022