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

Expose underlying Z3_context and Z3_sort #298

Merged
merged 1 commit into from
May 29, 2024

Conversation

JakobR
Copy link
Contributor

@JakobR JakobR commented May 29, 2024

This would be useful to use functions from the raw bindings that aren't exposed in the high-level bindings yet. Since the raw bindings are unsafe, it should be fine to give access to the Z3_context and Z3_sort.

Closes #290.

@waywardmonkeys
Copy link
Contributor

Thanks! Per #294, we will try to do a new release soon.

@waywardmonkeys waywardmonkeys merged commit 1252af7 into prove-rs:master May 29, 2024
11 checks passed
@JakobR JakobR deleted the expose-raw-ctx-sort branch May 29, 2024 09:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

No way to access the raw Z3_sort from Sort<'ctx> or Z3_context from Context
2 participants