Debug branch: Wrong model on QF_NIA formula

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