Z3 bitvector unsatisfiable after adding more than one constraint

October 4, 2024

For a CTF challenge, I need to reconstruct a byte array based on several constraints for each byte.
However, after playing around a bit with bit vectors in Z3, I noticed that solver.check() returns unsat as soon as I add more than one constraint.
Here is an example code for reproducibility:

from z3 import *

# Create solver
solver = Solver()

# Declare a BitVector of 8 bit
x = BitVec('x', 8)

# Add multiple constraints
solver.add(x >= 0)      # x should be greater or equal than 0
solver.add(x <= 128)    # x should be less or equal than 128

# Check whether constraints are satisfiable
if solver.check() == sat:
    model = solver.model()
    print(f'Found solution: x = {model[x]}')
else:
    print('No solution found')

In this case, I would expect that the bit vector "x" gets a value between 0 and 128 assigned.
But when being executed, this code gives me No solution found.

I tried to debug this issue by only adding one constraint at a time and checking the satisfiability (e.g. by commenting out either solver.add(x >= 0) or solver.add(x <= 128)). Thereby, I found out that each constraint on its own works as expected. However, both in combination don’t work which doesn’t make any sense to me.

I also tried to find any answers on the internet and ask ChatGPT for help, but even the latter one couldn’t tell why it doesn’t work.

Update:

I found out, that it works if I use 127 as upper limit.
So if I use the following 2 constraints, I’m getting x = 0 as solution although I still don’t know why it only works under these conditions (if I’m not completely mistaken, 8 bits should be sufficient to represent values up to 255):

solver.add(x >= 0)
solver.add(x <= 127)

>Solution :

Comparison operators treat the BitVec as signed by default, i.e. 128 = −128 for this 8-bit two’s complement integer. (Using any value less than 128 will make the existing signed integer constraints satisfiable.)

https://ericpony.github.io/z3py-tutorial/guide-examples.htm#:~:text=Machine%20Arithmetic

In contrast to programming languages, such as C, C++, C#, Java, there is no distinction between signed and unsigned bit-vectors as numbers. Instead, Z3 provides special signed versions of arithmetical operations where it makes a difference whether the bit-vector is treated as signed or unsigned. In Z3Py, the operators <, <=, >, >=, /, % and >> correspond to the signed versions. The corresponding unsigned operators are ULT, ULE, UGT, UGE, UDiv, URem and LShR.

Use unsigned ≥/≤ constraints:

# Add multiple constraints
solver.add(UGE(x, 0))      # x should be greater or equal than 0
solver.add(ULE(x, 128))    # x should be less or equal than 128