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

Error when calling CharFromBv from Python API #7081

Closed
Eladkay opened this issue Jan 4, 2024 · 0 comments
Closed

Error when calling CharFromBv from Python API #7081

Eladkay opened this issue Jan 4, 2024 · 0 comments

Comments

@Eladkay
Copy link

Eladkay commented Jan 4, 2024

Hello,
When calling the CharFromBv function of the Python API, an exception is raised:

  File "/<snip>/venv/lib/python3.12/site-packages/z3/z3.py", line 10858, in CharFromBv
    raise Z3Expression("Bit-vector expression needed")
          ^^^^^^^^^^^^
NameError: name 'Z3Expression' is not defined

I guess "Z3Expression" was supposed to be "Z3Exception".
The bug still exists in the main branch as of right now:

raise Z3Expression("Bit-vector expression needed")

Also, in line 10975, the context used appears to be the context from the expression and not the function's context parameter. Is this behavior intentional? It seems inconsistent with other functions.

Thank you!

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

No branches or pull requests

1 participant