Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

expect_failure pollutes SMT #1956

Closed
mtzguido opened this issue Mar 22, 2020 · 1 comment
Closed

expect_failure pollutes SMT #1956

mtzguido opened this issue Mar 22, 2020 · 1 comment
Assignees
@mtzguido
Labels
component/smtencoding component/typechecker

Comments

@mtzguido
Copy link
Member

I have a fix incoming. This wrongly succeeds:

[@expect_failure]
let xx : squash False = ()

let _ = assert False
@mtzguido mtzguido self-assigned this Mar 22, 2020
mtzguido added a commit that referenced this issue Mar 22, 2020
@mtzguido
mark #1956 fixed
ebb8826
@mtzguido
Copy link
Member Author

Ha, sorry, this is on a branch of mine only where I'm messing with expect_failure. Nothing wrong in master. I'll check this file in as a regression test in that branch.

mtzguido added a commit that referenced this issue Mar 23, 2020
@mtzguido
examples: add several regression tests for pattern matching
d263e24 
For issues #1121, #1903 and #1954. Issue #829 is also relevant.
The PatternMatch.fst file also constains some various examples. While at
it, also add a check for #1956 (even if it never manifested).
mtzguido added a commit that referenced this issue Mar 24, 2020
@mtzguido
examples: add several regression tests for pattern matching
921445f 
For issues #829, #1121, #1228, #1903 and #1954. The PatternMatch.fst
file also constains some various examples. While at it, also add a check
for #1956 (even if it never manifested).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mtzguido mtzguido

Labels
component/smtencoding component/typechecker
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@mtzguido