[BUG] Inliner fails to inline operators

[konnov]

Somewhat unexpected, the following simple piece of code does not work:

----------------------------- MODULE Callback ----------------------------      
EXTENDS Integers

VARIABLES x

Pick(Cb(_)) ==
    \E i \in 1..10:
        Cb(i)

Init ==
    LET Cb(i) ==
        x = i
    IN
    Pick(Cb)

Next ==
    LET Cb(i) ==
        x' = i
    IN
    Pick(Cb)

Inv ==
    x > 0
==========================================================================

[Kukovec]

While the specification seems to violate FlatLanguagePredicate, it is not an issue with inlining, as the inliner produces the expected output.
We should consider removing (higher-order) operators from the module, once they have been inlined in Init and Next.

[konnov]

Thanks! We should filter out the operators that are not required for the further model checking pass. I will pick this issue.

[konnov]

This is fixed in #301