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

Properties only working on particular Z3 versions #166

Open
2 of 6 tasks
mccleeary-galois opened this issue Oct 31, 2024 · 0 comments
Open
2 of 6 tasks

Properties only working on particular Z3 versions #166

mccleeary-galois opened this issue Oct 31, 2024 · 0 comments
Labels
bug Something isn't working good first issue Good for newcomers

Comments

@mccleeary-galois
Copy link
Contributor

mccleeary-galois commented Oct 31, 2024 •
edited
Loading

Summary

Currently some properties only work with the latest version of Z3 not what is shipped with what4-solvers

https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20240212

This was found during review of #161

Acceptance Criteria

Properties that do not :prove on Z3 4.8.14 have been identified and documented and changed to :check in the docstrings

Do

  • define acceptance criteria
  • add appropriate labels
  • remember to update CHANGES
  • remember to update docs appropriately
  • identified properties that do not :prove on Z3 4.8.14
  • Documented and updated properties to use :check with explanation that it is provable with more recent versions of Z3.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working good first issue Good for newcomers
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@mccleeary-galois