Infinite loop/performance regression in Z3 4.15.3

[rod-chapman]

See the attached SMT file.

With Z3 4.12.6, this proves "unsat" in about 15 seconds on my Apple MacBook Pro.

With Z3 4.15.3, it does not terminate in any reasonable time, and consumes approx 30GB RAM.

The SMT file was produced by CBMC 6.7.1.
Can anyone see a way to restore the original performance please?

asg.smt2.gz

[rod-chapman]

Additional info: I tried rewriter.bv_sort_ac=true and Z3 4.5.13 then returns "unsat" after 15 minutes. This is better, but still has a huge impact on our CI and interactive development.