Skip to content

Z3 python plugin API's decide method broken #7451

New issue
Jump to bottom
New issue
Jump to bottom
Closed
#7452
Closed
Z3 python plugin API's decide method broken#7451
#7452
@linusheck

Description

@linusheck
linusheck
opened on Nov 13, 2024

I found some issues in the Python plugin API. The decide method uses the undefined variable t_ref:

z3/src/api/python/z3/z3.py

Line 11668 in c0e748a

t = _to_expr_ref(to_Ast(t_ref), prop.ctx())

Also, registering a decide refers to the undefined property self.decide:

z3/src/api/python/z3/z3.py

Line 11787 in c0e748a

def add_decide(self, decide):

which should have been declared here:

z3/src/api/python/z3/z3.py

Line 11728 in c0e748a

self.created = None

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