Performance issue on QF_NIRA formula

muchang commented 4 years ago

This formula causes cvc4 to hang (while cvc4-1.7 answers sat quickly and cvc4-1.8 returns unknown) :

[756] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun c () Real)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (<= 4 c))
(assert
 (or (<= (- a) (div (to_int c) (to_int a)))
 (<=
  (div (to_int b)
  (mod 4
   (to_int (/ a (* c (div (- 3) (to_int (* c c))))))))
  0)))
(assert (> a b))
(assert (> a c))
(check-sat)
[757] % time cvc4-1.7 small.smt2
sat
real  0m0.144s
user  0m0.051s
sys   0m0.004s
[758] % 
[758] % time cvc4-1.8 small.smt2
unknown
real  0m16.886s
user  0m12.282s
sys   0m0.020s
[759] % 
[759] % timeout -s 9 30 cvc4 small.smt2
Killed
[760] %

OS: Ubuntu 18.04 Commit: 8802500

ajreynol commented 3 years ago

Fixed in latest master, will add regression.

ajreynol commented 2 years ago

cvc5 solves this in 1.5 seconds in production now.

cvc5 / cvc5-projects

Performance issue on QF_NIRA formula #263