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

Add inNewFrame2 #218

Open
RyanGlScott opened this issue Sep 8, 2022 · 0 comments
Open

Add inNewFrame2 #218

RyanGlScott opened this issue Sep 8, 2022 · 0 comments
Labels
enhancement New feature or request

Comments

@RyanGlScott
Copy link
Contributor

GaloisInc/crucible#1037 adds an inNewFrame2 combinator that is like what4's inNewFrame, but specifically for frame 2 (used for CVC5 abduction purposes). This combinator would be generally useful, and as such, we should consider upstreaming it to what4.

Note that instead of using the implementation in crucible, we should try to use the exception-safe implementation of inNewFrame as a skeleton for inNewFrame2. In fact, we can likely steal most of the implementation of inNewFrame, so we will need to figure out a reasonable way to share code between inNewFrame and inNewFrame2.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant