search

cvc5 / cvc5-projects

1 stars 0 forks source link

Performance regression on QF_NRA formula #238

Open muchang opened 3 years ago

muchang commented 3 years ago

Hi, For this formula, cvc4-1.7 can report sat while cvc4-1.8 and nightly build report unknown:

[563] % cvc4-1.7 -q small.smt2
sat
[564] % cvc4-1.8 -q small.smt2
unknown
[565] % cvc4 -q small.smt2
unknown
[566] % 
[566] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (< a b))
(assert (or (< b 0) (= (/ 3 b) 1)))
(check-sat)
[567] %

OS: Ubuntu 18.04 Commit: 56f2e6d

ajreynol commented 3 years ago

Note this benchmark times out with: --nl-ext-tplanes --nl-rlv=always (best configuration for "sat"). However, it is solved sat by --decision=internal. I'm marking this issue as "performance". The performance issue is likely caused by a different in SAT decisions.

ajreynol commented 3 years ago

FYI, this is QF_NRA since there is a non-constant division.