Debug branch: Wrong model on QF_NIA formula

[wintered]

Z3 returns a wrong model for this formula

(declare-fun a () Int)
(declare-fun b () Int)
(assert (= (div a (- 2 b)) 2))
(check-sat)
(get-model)

sat
(model 
  (define-fun b () Int
    0)
  (define-fun a () Int
    2)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    2)
)

OS: Ubuntu 18.04
Revision: e0411c1