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

goal_eval_unint doesn't work with at #1591

Closed
brianhuffman opened this issue Feb 17, 2022 · 0 comments
Closed

goal_eval_unint doesn't work with at #1591

brianhuffman opened this issue Feb 17, 2022 · 0 comments

Comments

@brianhuffman
Copy link
Contributor

brianhuffman commented Feb 17, 2022 •
edited
Loading

When I try to make at uninterpreted, it produces the following error message:

Cannot create uninterpreted function "at_180_256_Vec_32_Bool" with argument bvToNat 8 (<<bitvector>>)
brianhuffman pushed a commit that referenced this issue Feb 17, 2022
Support bvToNat in uninterpreted functions.
aa9afcd 
This lets `goal_eval_unint` and `w4_unint` work with
functions like `at`.

Fixes #1591.
@mergify mergify bot closed this as completed in 60e5a48 Feb 21, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@brianhuffman