Performance issue on QF_NIA formula

[rainoftime]

Hi, for the following formula

(set-logic QF_NIA)
(declare-const i3 Int)
(declare-const i19 Int)
(assert (= 538 (* 136 (+ 56 354 0 0 (- i19 18 i3)))))
(check-sat)

yices 5019920

$ time z3 xx.smt2
unsat

real    0m0.011s
user    0m0.004s
sys     0m0.007s
$ time cvc xx.smt2
unsat

real    0m0.005s
user    0m0.003s
sys     0m0.002s
$ yices --timeout=30 xx.smt2                                                                                                                                                    
unknown

[ahmed-irfan]

The example doesn't contain nonlinearity. If you set the logic to QF_LIA, Yices solves this immediately.