I'm new to Z3, so this is likely a silly question. I'm trying to model an execution flow of a program. Doing this through manual z3 calls for now. That said, I end up trying to model something like the following:
x = 1
x += 1
Performing the following commands gives me unsat, and I understand why.
x = z3.Int('x')
s.add(x == 1)
s.add(x == x + 1)
In small scale, it might be reasonable to manually change x == 1 to x == 2. My question is, is there a way to do this in z3 where I don't have to go back and attempt to modify the variables I put into the solver? The equations obviously would get much harrier than just +1, and attempting to work through that logic manually seems error prone and sloppy.
EDIT: After adjusting my program to use SSA as suggested, it works very easily now. I did opt to keep multiple versions of the variable, but that didn't turn into too much extra work.
