4.13.0 hangs on an example that works in 4.8.7

[gernst]

This file hangs with Z3 version 4.13.0 - 64 bit (on Linux glibc 2.35, official binary): lemma1.txt
Similarly, replacing the goal and check-sat with a push also hangs: push.txt

I can confirm that it works with version 4.8.7.

[NikolajBjorner]

You should specify patterns to make sure the E-matching uses large sub-expressions instead of small ones.
There is an axiom profiler that can guide you to instantiation loops

[gernst]

Thanks. Indeed it was an issue with some axioms mentioning concrete numbers.