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

Test functions over booleans #36

Open
makaimann opened this issue Feb 12, 2020 · 6 comments
Open

Test functions over booleans #36

makaimann opened this issue Feb 12, 2020 · 6 comments
Assignees
@makaimann
Labels
bug Something isn't working

Comments

@makaimann
Copy link
Collaborator

Saw unexpected behaviour once (using MathSAT).
@makaimann makaimann added the bug Something isn't working label Feb 12, 2020
@makaimann makaimann self-assigned this Feb 12, 2020
@ahmed-irfan
Copy link
Collaborator

you mean f(b), where f is a UF and b is a boolean?

@makaimann
Copy link
Collaborator Author

Yep, exactly! Is that expected?

@ahmed-irfan
Copy link
Collaborator

iirc, mathsat does not allow that. Another example is Array of booleans, which is also not allowed by mathsat.

@makaimann
Copy link
Collaborator Author

MathSAT doesn't support UF over booleans. Handled partially with 898e019, however querying the function sort will give bit-vector operators (because that's what we're using under-the-hood) even though at the smt-switch level they should be booleans.

@makaimann
Copy link
Collaborator Author

Looks like there is a "allow_bool_function_args" option. Should try using that.

@ahmed-irfan
Copy link
Collaborator

yeah, we should try that. I think it is a new option

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@makaimann makaimann

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@makaimann @ahmed-irfan