performance on bit vectors

[Heaven2024]

for this case :

(declare-fun n () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(declare-fun z () (_ BitVec 32))
(declare-fun cond () (_ BitVec 32))

(assert (= cond (ite (= (bvadd (_ bv6 32) (bvmul (_ bv6 32) n)) z) (_ bv1 32) (_ bv0 32))))
(assert (let ((cse0 (bvmul (_ bv3 32) (bvmul n n))))
          (and (= (bvadd z y) (bvadd (_ bv7 32) cse0 (bvmul (_ bv9 32) n)))
               (= (bvadd (bvmul (_ bv3 32) n) cse0 (_ bv1 32)) y))))
(assert (not (= (_ bv1 32) cond)))
(check-sat)

timeout 20s  z3 test.smt2
z3 interrupted by SIGTERM. 

For other solvers：

cvc5 test.smt2
unsat
stp test.smt2
unsat