如何为z3py序列中的所有元素设置约束？

from z3 import *

solver = Solver()

sequence = Ints('x', n)

for i in range(n):
    # 设置约束条件
    constraint = And(sequence[i] >= lower_bound, sequence[i] <= upper_bound)
    # 添加约束条件到求解器
    solver.add(constraint)

if solver.check() == sat:
    print("Constraints are satisfiable.")
else:
    print("Constraints are unsatisfiable.")

from z3 import *

# 创建求解器
solver = Solver()

# 定义序列变量
n = 5
sequence = Ints('x', n)

# 设置约束条件
lower_bound = 0
upper_bound = 10
for i in range(n):
    constraint = And(sequence[i] >= lower_bound, sequence[i] <= upper_bound)
    solver.add(constraint)

# 检查约束是否可满足
if solver.check() == sat:
    print("Constraints are satisfiable.")
else:
    print("Constraints are unsatisfiable.")