Skip to content

Error when calling CharFromBv from Python API #7081

Closed
@Eladkay

Description

@Eladkay

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!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions