Unexpected behavior of z3 in parallel mode #7596
Comments
|
Here is a smaller example producing a solution violating the defined constraints: from z3 import *
n = 7
expected_result = 0
for _ in range(n):
expected_result *= 0x1000123
expected_result += ord('a')
expected_result &= 0xffffffff
set_option("parallel.enable", True)
chars = [BitVec(f"c_{i}", 32) for i in range(n)]
s = Solver()
# All characters must be between a-f or 0-9
for c in chars:
s.add(Or(And(c >= ord('a'), c <= ord('f')), And(c >= ord('0'
8000
), c <= ord('9'))))
h = BitVecVal(0, 32)
for i in range(len(chars)):
h *= 0x1000123
h += chars[i]
s.add(h == expected_result)
print(s.check())
m = s.model()
vals = [(x, m[x]) for x in m]
sm = sorted(vals, key=lambda x: str(x[0]))
for name, r in sm:
val = r.as_long()
print(name, hex(val), chr(val) if val < 128 else 'invalid')Output: |
|
it's a tricky one |
NikolajBjorner
added a commit
that referenced
this issue
Apr 28, 2025
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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
Output
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.
The text was updated successfully, but these errors were encountered: