Suppose I assign to a sym as follows:
Define f in terms of z
Now assign a value to z
But f is still expressed in terms of z and it doesn't seem to substitute the value for z
But assigning to a new expression in terms of z works as expected.
How do I get the SMT to realize that f = 2i?