Performance regression on stratified EPR formula

[kenmcmil]

thing2.zip

The attached example is in the stratified EPR fragment. Z3 version 4.7.1 handles this and similar examples in a fraction of a second, while version 4.12.2 seems to diverge or take an extremely long time. I've run into numerous other cases where 4.12.2 seems to diverge or run very slowly on such formulas, while 4.7.1 is almost instantaneous.

Thanks for any help -- Ken