epfl-lara / leon

The Leon system for verification, synthesis, repair
Other
162 stars 49 forks source link

Improve verification of some pattern matching #307

Closed mantognini closed 7 years ago

mantognini commented 7 years ago

This patch addresses issues with array access with side effect in the index selection, while being scrutinee of a pattern match. Side effect in guards and pattern is not supported, as it was the case previously.