要在Z3模型中以十进制格式获取数组的值，可以使用以下代码示例：

from z3 import *

# 创建一个数组变量
array = Array('array', IntSort(), IntSort())

# 创建一个Z3求解器
solver = Solver()

# 假设数组array中的某些元素已知
solver.add(array[0] == 10)
solver.add(array[1] == 20)
solver.add(array[2] == 30)

# 获取数组的值
value_0 = solver.model()[array[0]].as_long()  # 获取索引为0的元素值
value_1 = solver.model()[array[1]].as_long()  # 获取索引为1的元素值
value_2 = solver.model()[array[2]].as_long()  # 获取索引为2的元素值

# 打印数组的值
print(f"array[0] = {value_0}")
print(f"array[1] = {value_1}")
print(f"array[2] = {value_2}")

这段代码创建了一个名为array的数组变量，并使用solver.add()函数添加了一些已知的数组元素。然后，通过solver.model()函数获取到求解器的模型，并使用as_long()方法将获取到的值转换为十进制格式。

最后，使用print()函数打印出数组的值。输出结果将会是：

array[0] = 10
array[1] = 20
array[2] = 30

请注意，这只是一个简单的示例，实际使用时可能需要根据具体情况进行适当修改。