Performance problem of NodeEliminator on some LIA-lin CHC-Comp 2024 benchmarks

[BritikovKI]

Golem parser seems to struggle with some benchmarks from chc-comp 2024. Specifically when being run on a bunch chc-comp24-LIA-Lin-226.smt2 - chc-comp24-LIA-Lin-262.smt2 golem with 300s timeout never even starts solving the instance.

Supposed bug.

[blishko]

The parser has no problem with these benchmarks, the problem is in preprocessor that is applied before some engines (e.g., TPA). Namely, NodeEliminator.

Note that Spacer engine gets to the solving pretty quickly.
However, these benchmarks seem to be quite hard in general. Also Z3 is struggling with solving them.

[blishko]

The problem is with NonLoopEliminator that aggressively tries to eliminate non-looping nodes.
However, if both the number of incoming and outgoing edges is large, this will simply blow up, because, it needs to merge every pair of incoming and outgoing edge.

Interestingly, NonLoopEliminator is used only in the pipeline from towardsTransitionSystems(), which is used only for kind, pdkind and tpa engines.
We should consider dropping NonLoopEliminator and instead try to run SimpleNodeEliminator in combination with pruning until fixedpoint.