Skip to content

exprIsDeadEnd: Use isDeadEndAppSig to check if a function appliction is bottoming.

Andreas Klebinger requested to merge wip/andreask/deadend-fix into master 
exprIsDeadEnd: Use isDeadEndAppSig to check if a function appliction is bottoming.

We used to check the divergence and that the number of arguments > arity.
But arity zero represents unknown arity so this was subtly broken for a long time!

We would check if the saturated function diverges, and if we applied >=arity arguments.
But for unknown arity functions any number of arguments is >=idArity.

This fixes #21440.

I also renamed appIsDeadEnd into isDeadEndAppSig so that it's in line with isDeadEndSig.

Merge request reports