epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 49 forks source link

Relax fallback condition of `AntiAliasing` handling of `Let` #1495

Closed mario-bucev closed 5 months ago

mario-bucev commented 5 months ago

This relaxation allows the test cases of TargetMutation{7,8} to be accepted. Note that the diff suggests a complete rewrite of the Let case but it is really just replacing varsOfExprDealiased(e, env) with terminalVarsOfExprDealiased(e, env).