search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
371 stars 47 forks source link

Performance issue on QF_NIA formula #307

Open rainoftime opened 4 years ago

rainoftime commented 4 years ago

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 commented 1 year ago

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