Kukovec

I just tried sketching out what it would take to add a simple `UniqueNameGenerator` to `OppApplTranslator::translateLocalOperator`. Since basically none of the classes in the parser pass are injection-managed, you'd need...

> > We have a systematic approach, it's called "using the scoped builder". > > I don't see how this is related. Local operators are substituted in the importer. Yes,...

Sure, you should be able to pass all of the parameters that are currently only set inside `apalache.cfg` via flags when you call `check`, including the option to just point...

No, this is an extension of #1036

Are we talking about `main` or the temporal branch?

No, if it was there would have been a PR about it.

Adding to the above, caches will also be an issue in follow-ups to #2547, since arena/SMT splitting would require us to reevaluate the caches, as the cached values are cells...

Well, first we need to have a discussion regarding what we consider to be a metric for performance. But ultimately, probably.

I'd like to see others weigh in on this too, but the tests you have proposed are not equivalent. - The following case is never addressed: ```scala ( builder.name("x", tt),...

The issue is not with `Unroller` but with `INSTANCE`-imported recursive operators not being marked recursive (i.e. having `.isRecursive = false`). See attached minimal example.