Equivalence checking: split 'erroneous' into 'unequivalent' and 'unsafe'

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs

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

Apache License 2.0

349 stars 50 forks source link

Equivalence checking: split 'erroneous' into 'unequivalent' and 'unsafe' #1435

Closed mario-bucev closed 1 year ago

mario-bucev commented 1 year ago

We now distinguish between a candidate function being incorrect due to unsafety (e.g. division by zero) or due to not being equivalent. Previously, these two kinds of incorrectness were merged into one category.