Soundness bug QF_NIA, (distinct (mod 

Consider the following formula:

```
(declare-fun m () Int) 
(declare-fun y () Int) 
(declare-fun x () Int) 
(assert (= (- (- x y) m) 0)) 
(assert (distinct (mod x m) (mod y m)))  
(assert (> y 0)) (assert (<= m 0)) 
(check-sat)
```
Z3 reports `sat` on this unsatisfiable formula. Feeding Z3's model yields `unsat`.

OS: Ubuntu 18.04
Revision: 1fff7bb