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.

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

Use the fixed AFP version of Finite_Map_Extras #47

Open
javierdiaz72 opened this issue Jun 30, 2023 · 0 comments
Open

Use the fixed AFP version of Finite_Map_Extras #47

javierdiaz72 opened this issue Jun 30, 2023 · 0 comments

Comments

@javierdiaz72
Copy link
Contributor

While porting the Praos specification to the Þ-calculus (see #44), we came across an issue in which the GitHub automated build failed due to an abnormal termination of the Z3 prover. The source of this failure is a call to the smt proof method in the AFP's Finite_Map_Extras theory. Although the root cause seems to be related to GitHub Actions (as our code can be successfully built locally), a version of Finite_Map_Extras without such troublesome uses of smt would be the appropriate solution, given that @javierdiaz72 is actually the author of such AFP entry. We shall thus use the fixed AFP version of Finite_Map_Extras once it is available.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant