Performance issue on QF_LIRA formula

[rainoftime]

Hi, for the following fomula

(set-logic QF_LIRA)
(declare-const i1 Int)
(declare-const r2 Real)
(declare-const i13 Int)
(assert (is_int (- 0.0 0.0 0.0 r2 (to_real (abs i1)))))
(assert (< (to_real (to_int (to_real i13))) (- r2) 0.0 (to_real 60)))
(check-sat)

cvc4 63e7c6bb6d

$ time ./z3 yy.smt2 
sat
real    0m0.029s
user    0m0.028s
sys     0m0.000s

$ time ./yices_smt2 yy.smt2 
sat
real    0m0.004s
user    0m0.002s
sys     0m0.001s

$ /cvc4 --tlimit=60000 yy.smt2                                                                                              
CVC4 interrupted by timeout.
Aborted

The results are similar after changing (set-logic QF_LIRA) to (set-logic ALL)

[nafur]

So we could implement a preprocessing that does the following:

   (is_int i1)
=> (is_int (abs i1))
=> (is_int (to_real (abs i1)))
   (is_int (- 0.0 0.0 0.0 r2 (to_real (abs i1)))))
=> (is_int (+ 0.0 0.0 0.0 r2 (to_real (abs i1)))))
=> (is_int r2)

With this, the example is solved pretty much instantly.