Supongo que tengo una lista de 10 variables

v = [Real('v_%s' % (i+1)) for i in range(10)]

y quiero agregar una restricción simple como esta

s = Solver()
for i in range(10):
    s.add(v[i] == i)
if s.check() == sat:
    print(s.model())

Así que un modelo satisfactorio esv_1 = 0, v_2 = 1 .... v_10 = 9. Sin embargo, la salida deprint(s.model()) está totalmente desordenado, lo que me confunde cuando tengo muchas variables en un modelo más grande. Para este ejemplo, la salida de mi computadora esv_5, v_7, v_4, v_2, v_1, v_3, v_6, v_8, v_9, v_10, pero quiero superar las variables de este modelo en orden comov_1, v_2, ..., v_10. ¿Alguien puede decirme si z3Py tiene este tipo de función o no? ¡Gracias