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

[FEATURE] Update and use KeraLanguagePred #1127

Closed
konnov opened this issue Dec 1, 2021 · 0 comments · Fixed by #1128
Closed

[FEATURE] Update and use KeraLanguagePred #1127

konnov opened this issue Dec 1, 2021 · 0 comments · Fixed by #1128
Assignees
@konnov
Labels
refactoring

Comments

@konnov
Copy link
Collaborator

konnov commented Dec 1, 2021

KeraLanguagePred was supposed to guard our preprocessing passes from producing expressions outside of KerA+. Since we have updated KerA+ since then, we have to update this predicate and include it as a watchdog in preprocessing.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@konnov konnov

Labels
refactoring
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Use KeraLanguagePred to complain about unsupported operators apalache-mc/apalache
1 participant
@konnov