如何从z3中给定的一组可能的整数中获取整数列表？

from z3 import *

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

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

# 添加约束条件
solver.add(x >= 0, x <= 10)
solver.add(y >= 0, y <= 10)
solver.add(z >= 0, z <= 10)
solver.add(x + y + z == 10)

# 检查约束条件是否可满足
if solver.check() == sat:
    # 获取满足条件的模型
    model = solver.model()

    # 从模型中提取整数变量的取值，生成整数列表
    integer_list = [model.eval(var).as_long() for var in [x, y, z]]
    print(integer_list)
else:
    print("No solution found.")