如何在z3py中断言所有变量相等？

from z3 import *

# 定义变量
x = Int('x')
y = Int('y')
z = Int('z')

# 创建z3求解器
solver = Solver()

# 断言所有变量相等
solver.add(z3.And(x == y, y == z))

# 检查是否存在满足断言的解
if solver.check() == sat:
    # 获取解的具体值
    model = solver.model()
    print("x =", model[x])
    print("y =", model[y])
    print("z =", model[z])
else:
    print("No solution")