-
Notifications
You must be signed in to change notification settings - Fork 104
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
Symbol::as_z3_symbol can return Null Pointer #235
Comments
In doing some more digging, I see that Z3 tries to warn the user about this but in #92 we disabled the error handler and don't otherwise try to detect this situation. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
It seem like the integer conversion for Symbol does not check that the integer is within the valid bounds that
Z3_mk_int_symbol
expects(0 <= 2^30 -1). If you try to create a symbol withu32::MAX
for example then any of the functions that use a symbol viaas_z3_symbol
will be using a null pointer.I'm not sure what bad things can happen because of this, I think some of the usual cases do get caught or just have other operations return null as well.
The text was updated successfully, but these errors were encountered: