z3 Solver results affected on the order in which unrelated contraints are added

test-z3.py

import z3
import sys

def solve(msg, lvar, xvar, s):
  global status

  s.set("timeout", 60000)
  res = s.check()

  if(z3.unknown == res):
    print("::unk")

  if(z3.sat == res):
      print("::sat")
  elif(z3.unsat == res):
    print("::unsat")

### GPRs
VX_RAX = z3.BitVec('VX_RAX',1)
VL_RAX = z3.BitVec('VL_RAX',1)

### YMM Registers
VX_YMM1 = z3.BitVec('VX_YMM1', 256)
VX_YMM2 = z3.BitVec('VX_YMM2', 256)

VL_YMM1_0 = z3.BitVec('VL_YMM1_0', 64)
VL_YMM1_1 = z3.BitVec('VL_YMM1_1', 64)
VL_YMM1_2 = z3.BitVec('VL_YMM1_2', 64)
VL_YMM1_3 = z3.BitVec('VL_YMM1_3', 64)

VL_YMM2_0 = z3.BitVec('VL_YMM2_0', 64)
VL_YMM2_1 = z3.BitVec('VL_YMM2_1', 64)
VL_YMM2_2 = z3.BitVec('VL_YMM2_2', 64)
VL_YMM2_3 = z3.BitVec('VL_YMM2_3', 64)

##############################
## Proof variables ###########
##############################
s = z3.Solver()
#z3.set_param("verbose", 5)

#s.add(VX_RAX == VL_RAX)
s.add(z3.Concat(VL_YMM1_3, VL_YMM1_2, VL_YMM1_1, VL_YMM1_0) == VX_YMM1)
s.add(z3.Concat(VL_YMM2_3, VL_YMM2_2, VL_YMM2_1, VL_YMM2_0) == VX_YMM2)
s.add(VX_RAX == VL_RAX)


V_R = z3.BitVec('V_R',64)
V_Y = z3.BitVec('V_Y',256)

## =******= YMM1 =******=
print(s)
s.push()
lvar = (V_Y == z3.Concat(z3.Extract(63, 56, VL_YMM1_3), z3.Extract(55, 48, VL_YMM1_3), z3.Extract(47, 40, VL_YMM1_3), z3.Extract(39, 32, VL_YMM1_3), z3.Extract(31, 24, VL_YMM1_3), z3.Extract(23, 16, VL_YMM1_3), z3.Extract(15, 8, VL_YMM1_3), z3.Extract(7, 0, VL_YMM1_3), z3.Extract(63, 56, VL_YMM1_2), z3.Extract(55, 48, VL_YMM1_2), z3.Extract(47, 40, VL_YMM1_2), z3.Extract(39, 32, VL_YMM1_2), z3.Extract(31, 24, VL_YMM1_2), z3.Extract(23, 16, VL_YMM1_2), z3.Extract(15, 8, VL_YMM1_2), z3.Extract(7, 0, VL_YMM1_2), z3.Extract(7, 0, ((((z3.LShR(VL_YMM2_1, z3.BitVecVal(56, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + (z3.LShR(VL_YMM1_1, z3.BitVecVal(56, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64))) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_1 & z3.BitVecVal(71776119061217280, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_1) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(48, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_1 & z3.BitVecVal(280375465082880, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_1) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(40, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_1 & z3.BitVecVal(1095216660480, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_1) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(32, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_1 & z3.BitVecVal(4278190080, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_1) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(24, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_1 & z3.BitVecVal(16711680, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_1) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(16, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_1 & z3.BitVecVal(65280, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_1) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(8, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, (((VL_YMM2_1 + VL_YMM1_1) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((((z3.LShR(VL_YMM2_0, z3.BitVecVal(56, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + (z3.LShR(VL_YMM1_0, z3.BitVecVal(56, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64))) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_0 & z3.BitVecVal(71776119061217280, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_0) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(48, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_0 & z3.BitVecVal(280375465082880, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_0) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(40, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_0 & z3.BitVecVal(1095216660480, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_0) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(32, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_0 & z3.BitVecVal(4278190080, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_0) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(24, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_0 & z3.BitVecVal(16711680, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_0) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(16, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, ((z3.LShR(((((VL_YMM2_0 & z3.BitVecVal(65280, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) + VL_YMM1_0) & z3.BitVecVal(18446744073709551616 - 1, 64)), z3.BitVecVal(8, 64)) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64))), z3.Extract(7, 0, (((VL_YMM2_0 + VL_YMM1_0) & z3.BitVecVal(18446744073709551616 - 1, 64)) & z3.BitVecVal(256 - 1, 64)))))

xvar = (V_Y == z3.Concat(z3.Extract(255, 128, VX_YMM1), z3.Concat((z3.Extract(127, 120, VX_YMM1) + z3.Extract(127, 120, VX_YMM2)), z3.Concat((z3.Extract(119, 112, VX_YMM1) + z3.Extract(119, 112, VX_YMM2)), z3.Concat((z3.Extract(111, 104, VX_YMM1) + z3.Extract(111, 104, VX_YMM2)), z3.Concat((z3.Extract(103, 96, VX_YMM1) + z3.Extract(103, 96, VX_YMM2)), z3.Concat((z3.Extract(95, 88, VX_YMM1) + z3.Extract(95, 88, VX_YMM2)), z3.Concat((z3.Extract(87, 80, VX_YMM1) + z3.Extract(87, 80, VX_YMM2)), z3.Concat((z3.Extract(79, 72, VX_YMM1) + z3.Extract(79, 72, VX_YMM2)), z3.Concat((z3.Extract(71, 64, VX_YMM1) + z3.Extract(71, 64, VX_YMM2)), z3.Concat((z3.Extract(63, 56, VX_YMM1) + z3.Extract(63, 56, VX_YMM2)), z3.Concat((z3.Extract(55, 48, VX_YMM1) + z3.Extract(55, 48, VX_YMM2)), z3.Concat((z3.Extract(47, 40, VX_YMM1) + z3.Extract(47, 40, VX_YMM2)), z3.Concat((z3.Extract(39, 32, VX_YMM1) + z3.Extract(39, 32, VX_YMM2)), z3.Concat((z3.Extract(31, 24, VX_YMM1) + z3.Extract(31, 24, VX_YMM2)), z3.Concat((z3.Extract(23, 16, VX_YMM1) + z3.Extract(23, 16, VX_YMM2)), z3.Concat((z3.Extract(15, 8, VX_YMM1) + z3.Extract(15, 8, VX_YMM2)), (z3.Extract(7, 0, VX_YMM1) + z3.Extract(7, 0, VX_YMM2)))))))))))))))))))

s.add(lvar != xvar)
solve("YMM1", lvar, xvar, s)

s.pop()