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

Avoid generating ghost state declarations for quantifiers unless quantifiers are used #95

Open
wuestholz opened this issue Oct 12, 2021 · 2 comments
Open

Avoid generating ghost state declarations for quantifiers unless quantifiers are used #95

wuestholz opened this issue Oct 12, 2021 · 2 comments
Assignees
@cd1m0
Labels
enhancement New feature or request

Comments

@wuestholz
Copy link

Currently, ghost state declarations (e.g., for tracking map keys) are generated regardless of whether there is a quantifier that quantifies over the corresponding map. It would be great to only generate the declarations on demand.
@wuestholz wuestholz added the enhancement New feature or request label Oct 12, 2021
@cd1m0
Copy link
Collaborator

cd1m0 commented Oct 28, 2021

Is this in the case where there is a sum operator over the map, but no forall?

@cd1m0 cd1m0 self-assigned this Oct 28, 2021
@wuestholz
Copy link
Author

Yeah, I think that was the case.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@cd1m0 cd1m0

Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@wuestholz @cd1m0