添加多个约束后 Z3 位向量无法满足

Question

对于 CTF 挑战，我需要根据每个字节的几个约束重建一个字节数组。 然而，在 Z3 中尝试了一下位向量后，我注意到只要添加多个约束，

solver.check()

就会返回 unsat。 这是可重复性的示例代码：

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')

在这种情况下，我希望位向量“x”获得分配的 0 到 128 之间的值。 但是当执行时，这段代码给了我

No solution found

。

我尝试通过一次仅添加一个约束并检查可满足性来调试此问题（例如，通过注释掉

solver.add(x >= 0)

或

solver.add(x <= 128)

）。因此，我发现每个约束本身都按预期工作。然而，两者结合起来不起作用，这对我来说没有任何意义。

我也尝试在互联网上找到任何答案并向ChatGPT寻求帮助，但即使是后者也无法说出为什么它不起作用。

Answer 1

比较运算符默认将

BitVec

视为有符号，即对于这个 8 位二进制补码整数，128 = −128。使用 128 以外的任何值都可以满足要求。

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

与 C、C++、C#、Java 等编程语言相比，作为数字，有符号和无符号位向量之间没有区别。相反，Z3 提供了算术运算的特殊有符号版本，其中位向量被视为有符号还是无符号会有所不同。在 Z3Py 中，运算符

<

、

<=

、

>

、

>=

、

/

、

%

和

>>

对应于签名版本。相应的无符号运算符为

ULT

、

ULE

、

UGT

、

UGE

、

UDiv

、

URem

和

LShR

。

# 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

找到解决方案：x = 128