viperproject/silicon

Unsoundness when using let-expressions inside quantifiers.

marcoeilers opened this issue · 0 comments

marcoeilers commented

Found by @ArquintL.
The attached program is able to assert false after folding a predicate.

test.gobra.txt