Unexpected behavior of z3 in parallel mode #7596
Description
Running the example below produces incorrect/unexpected results. All flag characters are constrained to be within the [a-fA-F0-9] range. However, the generated solution clearly violates that constraint. Switching the parallel mode off fixes the problem.
Python reproduction
from z3 import *
FLAG = [BitVec(f"flag_{i:x}", 32) for i in range(16)]
set_option("parallel.enable", True)
s = Solver()
# All characters must be between a-f or 0-9
for flag_char in FLAG:
s.add(Or(And(flag_char >= ord('a'), flag_char <= ord('f')), And(flag_char >= ord('0'), flag_char <= ord('9'))))
HASH = BitVecVal(0x811C9DC5, 32)
for i in range(16):
HASH *= 0x1000193
HASH ^= FLAG[i]
s.add(HASH == 0x7586CBD1)
MEM_0x10 = BitVecVal(0x811C9DC5, 32)
for i in range(3):
MEM_0x10 *= 0x1000193
MEM_0x10 ^= FLAG[i + 5]
MEM_0x10 &= 0xFF
s.add(MEM_0x10 == 0x51)
MEM_0x11 = BitVecVal(0x811C9DC5, 32)
for i in range(3):
MEM_0x11 *= 0x1000193
MEM_0x11 ^= FLAG[(i * 2) + 0xA]
MEM_0x11 &= 0xFF
s.add(MEM_0x11 == 0x53)
s.add(FLAG[4] == 0x30) # 0x12
MEM_0x13 = BitVecVal(0, 32)
for i in range(4):
MEM_0x13 += FLAG[i] * (0xD3**i)
MEM_0x13 -= 0x74D
MEM_0x13 &= 0xFF
MEM_0x13 ^= 0xC0
s.add(MEM_0x13 == 0xD1)
R0 = BitVecVal(0, 32)
R0 += FLAG[0xB]
R0 = R0 >> 13 | ((R0 & 0xFFFF) << (32 - 13))
R0 += FLAG[0xD]
R0 = R0 >> 13 | ((R0 & 0xFFFF) << (32 - 13))
R0 += FLAG[0xF]
R0 = R0 >> 13 | ((R0 & 0xFFFF) << (32 - 13))
R0 &= 0xFF
s.add(R0 == 0x40)
s.add(FLAG[9] == 0x61)
s.add(FLAG[8] == 0x32)
print(s.check())
m = s.model()
vals = [(x, m[x]) for x in m]
sm = sorted(vals, key=lambda x: str(x[0]))
for x in sm:
print(x[0], hex(x[1].as_long()), chr(x[1].as_long()) if x[1].as_long() < 1000 else '???')Output
sat
flag_0 0x61 a
flag_1 0xf00039 ???
flag_2 0x30 0
flag_3 0x36 6
flag_4 0x30 0
flag_5 0x62 b
flag_6 0x36 6
flag_7 0x32 2
flag_8 0x32 2
flag_9 0x61 a
flag_a 0x36 6
flag_b 0x6c l
flag_c 0x39 9
flag_d 0x3d =
flag_e 0x65 e
flag_f 0x43040432 ???
In case this is intended behaviour, and I'm using z3 incorrectly, a warning message or even a crash would be appreciated since presenting an incorrect result is quite unintuitive.