Performance regression from smt.arith.sovler=2 to smt.arith.sovler=6 on QF_NIA formula

[rainoftime]

Hi, for the following formula

(set-logic QF_NIA)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(assert (or false (= (div 0 0) (* (+ (abs i4) i1 0 0) (div 0 i0) i5 (abs (+ 728 0 i5 0)) i2)) false))
(assert (or (< 0 (abs i3)) false))
(assert (= i1 i3))
(check-sat)

Z3 (commit f2449df)

time z3 smt.arith.solver=2 zz.smt2
sat
real    0m0.313s
user    0m0.096s
sys     0m0.012s

z3 smt.arith.solver=6 zz.smt2 timeout=10000
unknown

[levnach]

Works in d6ad371934ab24ade0cb99fe6c7e85d2bd51196f