QF_UFBV unexpected slowdown for large model versus z3

[aep]

in average yices2 is alot faster than z3, but it apparantly becomes slower than z3 for large models.

the attached smt runs in 2 seconds with z3 and 16.2 seconds with yices2 on a Ryzen 3950X

::carrier::endpoint::poll.smt2.txt

is there any tuning i can do to prevent the slowdown for large models?

[aep]

here's a specific case that solves in 0.4 seconds in z3 but does not return after 3 hours in yices2

ab.smt2.txt