I have a Z3 formula (in Z3py)
i=z3.Int('x')+z3.Int('y')<2
How can I get the variable list x and y?
x
y
I added an example to Z3 to illustrate walking subexpressions in Python. https://github.com/Z3Prover/z3/blob/master/examples/python/visitor.py