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

--show-snippets affects how many symbols are verified #5958

Open
keyboardDrummer opened this issue Dec 3, 2024 · 1 comment
Open

--show-snippets affects how many symbols are verified #5958

keyboardDrummer opened this issue Dec 3, 2024 · 1 comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: now Will work on this now

Comments

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Dec 3, 2024 •
edited
Loading 

localDafny verify  Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/GenericSort.dfy\
 --standard-libraries:false

Dafny program verifier finished with 32 verified, 0 errors

Versus

localDafny verify  Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/GenericSort.dfy\
 --standard-libraries:false --show-snippets:false

Dafny program verifier finished with 24 verified, 0 errors
@keyboardDrummer keyboardDrummer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: now Will work on this now labels Dec 3, 2024
@keyboardDrummer keyboardDrummer changed the title Inconsistent verification of symbols --show-snippets affects how many symbols are verified Dec 3, 2024
@keyboardDrummer
Copy link
Member Author

I think the problem is that in the cares where it verifies more, it verifies too much (related to module refinement)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) priority: now Will work on this now
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@keyboardDrummer