Closed
Description
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:
Line 10974 in 239d68e
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!
Metadata
Metadata
Assignees
Labels
No labels