Hi @NikolajBjorner , @agurfinkel!

In SolCMC, we have observed some regressions on our test suite when attempting to upgrade Z3 from 4.12.1 to 4.13.0.
I have prepared a simplified example here.
When running z3 with the option fp.xform.inline_eager=false, version 4.13.0 hangs, while version 4.12.1 solves it immediately.
Note that both fp.xform.inline_eager=false and (set-option :produce-proofs true) in the file are required for 4.13.0 to hang.

Let me know, if I should try to minimize the example even further. I could spend more time on this, if the cause is not anything obvious.