Simplifies Viper programs (useful for simplifying generated code).
Aims to only perform sound simplifications: it should not introduce new verification errors, or cause previously code to verify when it shouldn't.
However there are likely many bugs, so use at your own risk.