Question about a method to change AST in z3py

[hagozaebii]

Hello, I am a novice in z3py. Recently, I've tried to change a part of AST into another AST.
For example, if we have a formula 1 == 2, I wanna change 1 into 3. I tried some codes as below.

p = IntVal(1) == IntVal(2)

p = IntVal(1) == IntVal(2)
q = IntVal(3)
p.children()[0] = q
p
1 == 2

After I checked z3py implementation, I noticed why my code won't work. Is there any method to change AST?
Thanks for your time!

[NikolajBjorner]

expressions are immutable objects in z3. You have to build new expressions if you want to have a variant.