Z3

安装

• python2

  https://pypi.org/project/z3-solver/4.5.1.0/#files(whl文件下载地址)

  sudo pip install z3_solver-4.5.1.0-py2-none-manylinux1_x86_64.whl

• python3

  sudo pip3 install z3-solver

整理解

a1 = IntVector('x', 32)

if s.check() == sat:
    m = s.model()
    res = ""
    for i in range(32):
        res += chr(m[a1[i]].as_long())

    print(res)

更加优雅的写法(python3.6以后支持f-string)

m = s.model()
s = ''
for i in range(10):
    v = m[x[i]].as_long()
    s += f'{v:x}'
print(s)

符号位

在Z3中，有符号数与无符号数使用不同的运算操作。 <,<=,>,>=,/,%,>>运算对应有符号数，相对应的无符号数运算符为ULT,ULE,UGT,UGE,UDiv,URem,LShR

因此在使用上述运算时，需要注意符号位，如果字符型就要BitVec(flag, 9), 或者使用无符号运算