Problem about Array

[cxxsheng]

s = Solver()
x = Int("input")
I = Array('O',IntSort(), IntSort())
# I = Store(I, 0, 1)
# I = Store(I, 1, 2)

I = Store(I, x, If(x>10, x-1, x+1))

print(simplify(Select(I,0)))

s.add(Select(I,10) == 10)

print(s.check())
print(s.model())

I assigned an array, and put some interger in it. And apparently, the expression above is unsat, why i got a sat result?

Store(O, input, If(input <= 10, 1 + input, -1 + input))[0]
sat
[input = 11,
 O = [10 -> 10, else -> 10],
 k!0 = [10 -> 10, else -> 10]]

[asuler-dcc]

I is an Array variable, not a function.If you add "s.add(x == 10)", the result will be unsat.