z3 creates two int vectors with the same elements but in different order

The easiest way to do this would be to convert your lists to bags and check that they’re equal to each other. (A bag is essentially an array that stores the multiplicity of each element you store in it.)

Based on this idea, here’s an example implementation:

from z3 import *

s = Solver()

# Working on 10 elements
SIZE = 10

# a is the original arary, sortedA will be the sorted version of it
a       = IntVector('A', SIZE)
sortedA = IntVector('S', SIZE)

# Assert that sortedA is indeed sorted
for i in range(SIZE-1):
    s.add(sortedA[i] <= sortedA[i+1])

# convert them to bags:
bagA = K(IntSort(), 0)
bagS = K(IntSort(), 0)
for i in range(SIZE):
    bagA = Store(bagA, a[i],       1 + Select(bagA, a[i]))
    bagS = Store(bagS, sortedA[i], 1 + Select(bagS, sortedA[i]))

# assert that the bags are the same
s.add(bagA == bagS)

# a few constraints to make output interesting. obviously you'll
# have actual constraints, so these won't be needed
s.add(a[3] == 5)    # a fixed element
s.add(a[3] > a[9])  # out-of order

# get and print the model
r = s.check()
if r == sat:
    m = s.model()
    finalA = []
    finalS = []
    for i in range(SIZE):
        finalA.append(m.evaluate(a[i],       model_completion=True))
        finalS.append(m.evaluate(sortedA[i], model_completion=True))
    print("A = %s" % finalA)
    print("S = %s" % finalS)
else:
    print("Solver said: %s" % r)

I commented the code so it should be easy to follow, but feel free to ask if there’s anything unclear.

When I run this program, I get:

A = [4, 4, 4, 5, 3, 5, 3, -2, 3, -2]
S = [-2, -2, 3, 3, 3, 4, 4, 4, 5, 5]

You can verify that S is indeed the sorted version of A. (Depending on your version of z3, random seed, etc., you might of course get a different answer. But S should still be the sorted version of A.)