Reduce execution time for z3

[kangwoosukeq]

Hi. I ran the below example with z3 4.10.2.

(set-logic QF_FPBV)
(declare-fun y () (_ BitVec 32))
(declare-fun x () (_ BitVec 32))
(assert
 (let ((?x14 (bvadd x y)))
 (let ((?x15 ((_ to_fp 11 53) roundNearestTiesToEven ?x14)))
 (let ((?x12 ((_ to_fp 11 53) roundNearestTiesToEven y)))
 (let ((?x11 ((_ to_fp 11 53) roundNearestTiesToEven x)))
 (let ((?x13 (fp.add roundNearestTiesToEven ?x11 ?x12)))
 (let (($x16 (= ?x13 ?x15)))
 (let (($x22 (not $x16)))
 (let (($x27 (=> (and (bvslt x (_ bv0 32)) (bvslt y (_ bv0 32))) (bvslt ?x14 (_ bv0 32)))))
 (let (($x21 (=> (and (bvslt (_ bv0 32) x) (bvslt (_ bv0 32) y)) (bvslt (_ bv0 32) ?x14))))
 (and $x21 $x27 $x22)))))))))))
(check-sat)

❯ ./z3 -smt2 ./test.smt
unsat

It finds if there exists x and y such that (to_fp (bvadd x y)) != (fp.add (to_fp x) (to_fp y) with assuming no overflow and underflow.

Although I used QF_FPBV logic, it takes about 17 minutes.

I wonder why this simple example takes such a long time and if there is any method to speed up this execution.

Thank you.