search

cvc5 / cvc5-projects

1 stars 0 forks source link

(check-model) Performance issue on QF_NRA formula #233

Closed muchang closed 4 years ago

muchang commented 4 years ago

Hi, for this formula, CVC4 can report sat quickly without arguments. If we enable check-model, CVC4 gives unknown.

[632] % cvc4 small.smt2
sat
[633] % cvc4 --check-models small.smt2
unknown
[634] % 
[634] % cat small.smt2
(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (not (< a 1 (/ 1 c))))
(assert (= (+ c (/ 0 b)) (+ (* 2 c) (* 4 a)) 1))
(check-sat)
[635] %

OS: Ubuntu 18.04 Commit: b52dc97

ajreynol commented 4 years ago

This is non-linear problem due to the use of non-linear division.

The behavior sat -> unknown is to be expected, since this problem involves non-linear, and check-models changes the internal heuristics.

Marking "performance".

ajreynol commented 4 years ago

Appears to be fixed in current master.