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

Z3 bug with global-declarations and datatypes #325

Closed
robdockins opened this issue Oct 22, 2019 · 1 comment
Closed

Z3 bug with global-declarations and datatypes #325

robdockins opened this issue Oct 22, 2019 · 1 comment
Labels
what4

Comments

@robdockins
Copy link
Contributor

CF Z3Prover/z3#2647

Released versions of Z3 have a bug that manifests with the combination of push/pop, the global-declarations option and datatype declarations. Z3 HEAD recently got a fix.

If we merge 983ed71, this may cause this bug to manifest for What4 users who use Z3 in online mode and use BaseStructType. It is not immediately clear if it is worth this possibility to fix issue #54.
@robdockins robdockins mentioned this issue Oct 22, 2019
Closed
@robdockins
Copy link
Contributor Author

Ugh, see also cvc5/cvc5#3402

robdockins added a commit that referenced this issue Oct 23, 2019
@robdockins
Merge pull request #330 from GaloisInc/fix/issue324
189d0c1 
Fixes #54. Fixes #324.  Note, however that #325 still applies. However, a bugfix is already applied in HEAD Z3 and the similar CVC4 error has been worked around by changing tuple representations.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
what4
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@robdockins