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.
marcoeilers opened this issue · 0 comments
Found by @ArquintL.
The attached program is able to assert false after folding a predicate.