-
Notifications
You must be signed in to change notification settings - Fork 104
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
About arrays equal #288
Comments
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
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?
The text was updated successfully, but these errors were encountered: