Z3: regression in BV theory with bitvector rotation

[kfriedberger]

In #497, we noticed a performance issue of Z3 in the test BitvectorFormulaManagerTest::bvRotateByBV.

@daniel-raffler could you analyse the issue and report to the Z3 developers? thanks.

[daniel-raffler]

I've opened a Z3 issue here:
Z3Prover/z3#7750

[daniel-raffler]

They've added some rewrite rules for this special case and it should work again in the next release. We can either wait for that release or just disable the test for now

[baierd]

Thanks for reporting!
I guess we can keep the current solution until it is fixed. We should however add a TODO so that we don't forget which version had the regression and when to look at it again. Also, we should leave this ticket open and set the milestone to our release after 6.0.0.

[daniel-raffler]

A new version of Z3 has been released a few days ago. The new version includes e3139d4, which should fix our performance issues in the test