About arrays equal

[carbonium14]

Hello, I found that array contains the _eq method when looking at the documentation, but I don't know how it is compared. What I want is to determine whether two arrays are equal, which means to determine whether the values of elements at the same position in the two arrays are equal.

Since my device is not equipped with z3-rust, I used z3python to test and find out whether two arrays are equal. I found that when the prefixes of two arrays are not equal, the deep elements will no longer be compared.

from z3 import *
# The result we want is that the two arrays are equal, but the result is unsat.
i, v = Ints('i v')
a = Array('a', IntSort(), IntSort())
a = Store(a, i, v)
b = Array('b', IntSort(), IntSort())
b = Store(b, i, v)

x = Solver()
x.add(a.eq(b))
print(x.check())

My question is, does the same rule follow in z3-rust?

update: I found the z3 documentation, which said "Z3 also enforces that if two arrays agree on all reads, then the arrays are equal.", so my question is, when z3 compares two arrays, it needs to traverse all the elements. And compare in turn whether they are equal?

[Pat-Lafon]

I think your python code might use the wrong equality?

from z3 import *

# The result we want is that the two arrays are equal, but the result is unsat.
i, v = Ints("i v")
a = Array("a", IntSort(), IntSort())
a = Store(a, i, v)
b = Array("b", IntSort(), IntSort())
b = Store(b, i, v)

x = Solver()
x.add(a == b)
print(x.check())

Returns sat as expected