Equivalence checking: apply max limit on permutation while pruning

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs

https://epfl-lara.github.io/stainless/

Apache License 2.0

349 stars 51 forks source link

Equivalence checking: apply max limit on permutation while pruning #1387

Closed mario-bucev closed 1 year ago

mario-bucev commented 1 year ago

Before this PR, the strategy was to generate the maximum number of allowed matching (default of 16) and then perform pruning on it. Some picked matching may get pruned, leaving us with less than the limit which is not something we would like. This PR changes the behaviour to pick matching (passing the pruning test) as long as we don't go over the limit.

vkuncak commented 1 year ago

What's the rationale for this? I mean, the new behavior sounds simpler to understand, but was the past one causing actual problems? Any test cases?

mario-bucev commented 1 year ago

funnyarith3 for example is a good test case (which sometimes fails depending on how symbols are sorted, affecting the order of the matching as well).