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

Struct declaration fixes #324

Closed
robdockins opened this issue Oct 22, 2019 · 0 comments · Fixed by #330
Closed

Struct declaration fixes #324

robdockins opened this issue Oct 22, 2019 · 0 comments · Fixed by #330
Labels
what4

Comments

@robdockins
Copy link
Contributor

What4 has code for automatically declaring tuple datatypes in solvers that speak SMTLib2 as necessary to interpret the BaseStruct type. Currently, this code apparently assumes the Z3 syntax for declaring datatypes, which does not match the SMTLib 2.6 syntax (CF http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf).

As a result, the necessary tuple declarations fail on SMTLib 2.6 compliant solvers (e.g. CVC4). We should refactor the tuple declaration code to work correctly on as many solvers as possible.
@robdockins robdockins mentioned this issue Oct 23, 2019
Merged
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

Successfully merging a pull request may close this issue.

Fix/issue324 GaloisInc/crucible
1 participant
@robdockins