Performance regression on QF_NIA

[merlinsun]

Hi,
For this following instance, z3 c18a42c cannot solve it in 5 minutes, while z3-4.8.1 return sat quickly.

$ cat small.smt2 
(set-logic QF_NIA)
(declare-fun R () Int)
(declare-fun e () Int)
(assert (distinct (mod e R) (mod e (- R))))
(check-sat)
$ time z3-4.8.1.016872a5e0f6-x64-ubuntu-16.04/bin/z3 small.smt2 
sat

real	0m2.029s
user	0m2.025s
sys	0m0.004s
$ timeout 5m z3 small.smt2 

[NikolajBjorner]

this kind of regression would be a bit arbitrary given that reasoning about non-linear mod is highly incomplete. Hard to keep track of such issues as stand-alone. What would be the criteria for knowing when such are adequately addressed?