search

viperproject / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78 stars 40 forks source link

Avoiding folds in the encoding of unfolding expressions #773

Closed marcoeilers closed 6 months ago

marcoeilers commented 6 months ago

This avoids having to prove that the predicate can be folded, which is not needed (but can still sometimes fail e.g. if wildcard multiplications lead to non-linear terms, like in an example that @jcp19 found).

jcp19 commented 6 months ago

I'm surprised that we are still running into non-linear terms here, considering that I am using the silicon branch with the wildcard multiplication optimization

marcoeilers commented 6 months ago

That's probably because I'm an idiot and forgot some cases there (added them now)

jcp19 commented 6 months ago

I would be happy to merge this as soon as the release is out (assuming the tests are passing)