how to get model interpretation without arithmetic operators?

[2paperstar]

when I use simplifiable condition in ITE, then I can get concrete value.

s = Solver()
i = Int('i')
s.add(1 + If(1 == 1, 1, 2) == i)
if s.check() == sat:
    print(s.model())  # [i = 2]
    print(s.model().eval(i))  # 2

however, if condition isn't simplifiable, then I cannot get concrete value in model.

s = Solver()
i = Int('i')
arr1 = K(IntSort(), 0)
arr2 = Store(arr1, 0, 1)
s.add(1 + If(arr1 == arr2, 1, 2) == i)
print(simplify(arr1 == arr2))  # K(Int, 0) == Store(K(Int, 0), 0, 1)
if s.check() == sat:
    print(s.model())  # [i = 1 + If(K(Int, 0) == Store(K(Int, 0), 0, 1), 1, 2)]
    print(s.model().eval(i))  # 3

even though I could get concrete value with eval, but it's not sufficient with lambda.

s = Solver()
i = Int('i')
arr = Array('arr', IntSort(), IntSort())
s.add(Lambda([i], 1+If(i == 0, 0, 1)) == arr)
if s.check() == sat:
    print(s.model())  # [arr = Lambda(i, 1 + If(i == 0, 0, 1))]
    print(s.model().eval(arr))  # Lambda(i, 1 + If(i == 0, 0, 1))

At least, I want to get result [arr = Lambda(i, If(i == 0, 1, 2))] from [arr = Lambda(i, If(i == 0, 0+1, 1+1))]
is there a way to get model interpretation without arithmetic operators?