Kukovec

@shonfeder do you have any idea how complex this would be?

@shonfeder for visibility.

Is there no granularity between "unused imports" and "unused variables" for `-Ywarn-unused`?

We should revisit this when #730 is implemented.

@konnov did this get fixed with the latest changes to `Skolem`?

I think you're mixing `ScopedBuilder` with `Builder` here, this issue is for the old builder, https://github.com/informalsystems/apalache/issues/1912 is for the new one.

As we discussed today, I'm taking over this PR, since Philip's internship is over.

This could also potentially be combined with #1845.

Trace invariants should combine nicely with trace exploration.

View-restricted trace invariants are just a special kind of input for the feature described in #1845