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

[Summer] Call Z3 substitution function when verifying the new-syntax refinement type #41

Closed
EasonZ2022 opened this issue Jul 26, 2022 · 1 comment
Closed

[Summer] Call Z3 substitution function when verifying the new-syntax refinement type #41

EasonZ2022 opened this issue Jul 26, 2022 · 1 comment

Comments

@EasonZ2022
Copy link

EasonZ2022 commented Jul 26, 2022 •
edited
Loading

Since we have parsed the new syntax and carried it to the verifying stage, we should call Z3 substitution function in the correct place to replace the alias variable with the real variable
@EasonZ2022 EasonZ2022 changed the title [Summer] Insert Z3 substitution function when verifying the new-syntax refinement type [Summer] Call Z3 substitution function when verifying the new-syntax refinement type Jul 26, 2022
@jchen-cs
Copy link
Collaborator

Already handled by separate issues for each typing rule in the new syntax

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@EasonZ2022 @jchen-cs