小提示：此文章为原翻车鱼博客文章，仅存档
z3 是微软开发的的高性能约束求解工具。
z3 也是 angr 和 triton 底层的约束求解器。其强大的数学求解能力在CTF解题中被广泛使用，
本文记录/摘录一些常用的z3 Python API，以期能较为充分的运用z3的强大能力。
数据类型
$1, $2 表示第1，2个参数。以此类推
数学类型
函数名 | 说明 | 例 |
Int | 定义一个整数，这里的整数是数学意义上的整数，不是C中int | x = Int('x') |
Ints | 定义几个整数 | x, y = Ints('x y') |
IntVector | 以$1为前缀定义，定义$2个Int | x = IntVector('x', 12) |
IntVal | 定义值为$1的一个Int，$1可以是string或整数 | a = IntVal(1); b=IntVal('123') |
Real | 定义一个实数 | x = Real('x') |
Reals | 同Ints | x = Reals('x y') |
RealVector | 同IntVector | x = RealVector('x', 12) |
RealVal | 同IntVal | x = RealVal('2.718') |
Q | 定义一个有理分数$1/$2 | x = Q(5, 8) |
RatVal | 与Q一样，定义一个有理分数$1 / $2，实际Q是调用的RatVal | x = RatVal(5, 8) |
Bool | 定义一个布尔类型 | p = Bool('p') |
Bools | 同Ints | p, q, r = Bools('p q r') |
BoolVector | 同IntVector | P = BoolVector('p', 5) |
BoolVal | 同IntVal | BoolVal(True) |
有限类型
函数名 | 说明 | 例 |
BitVec | 定义一个名为$1长度为$2 bit的位向量，如 BitVal(‘x’, 32)表示C语言中的int | x = BitVec('x', 16) |
BitVecs | 同 Ints | x, y, z = BitVecs('x y z', 16) |
BitVecVal | 定义值为$1，长度为$2 bit的位向量 | v = BitVecVal(10, 32) |
FPSort | 按照$1 bit指数位， $2 bit有效位定义一个浮点类型，如 FPSort(8, 24)表示C语言中float，FPSort(11, 53)表示C语言中double，当然z3已经内置了这几种类型：Float16()Float32(), Float64(), float128() | Single = FPSort(8, 24); Double = Float64() |
FP | 定义一个名为$1，类型为$2 的浮点数 | x = FP('x', FPSort(8, 24)) |
FPs | 同 Ints | x, y, z = FPs('x y z', FPSort(8, 24)) |
FPVal | 定义值为$1，类型为$2的浮点数 | v = FPVal(12.25, FPSort(8, 24)) |
String | 定义一个名为$1 的字符串 | x = String('x') |
Strings | 同 Ints | x, y, z = Strings('x y z') |
StringVal | 定义一个值为$1 的字符串 | x = StringVal('x') |
类
数学类型
Int
成员函数
函数名 | 返回类型 | 说明 | 例 |
as_long | python int | 把z3的Int转换成python的int | IntVal(888).as_long() |
as_string | python string | 把z3的Int转换成python的string | IntVal(888).as_string() |
运算
以下int除非特殊说明，均可使用python类型
函数名 | 返回类型 | 说明 | 例 |
add | Int | 两个Int相加 | Int('x') + Int('y'); Int('x') + 10 |
sub | Int | 两个Int相减 | Int('x') - Int('y'); Int('x') - 10 |
mul | Int | 两个Int相乘 | Int('x') * Int('y'); Int('x') * 10 |
div | Int | 两个Int相除 | Int('x') / Int('y'); Int('x') / 10 |
mod | Int | 取模运算 | Int('x') % Int('y'); Int('x') % 10 |
neg | Int | 取相反数 | -Int('x') |
pow | Int | 指数运算 | Int('x') ** Int('y'); Int('x') ** 10 |
eq | Bool | 得到相等的约束 | Int('a') == Int('b') |
ne | Bool | 得到不等的约束 | Int('a') != Int('b') |
lt | Bool | 得到小于的约束 | Int('a') < Int('b') |
le | Bool | 得到小于等于的约束 | Int('a') <= Int('b') |
gt | Bool | 得到大于的约束 | Int('a') > Int('b') |
ge | Bool | 得到大于等于的约束 | Int('a') >= Int('b') |
ToReal | Real | 转换成Real类型 | ToReal(Int('x')) |
Int2BV | BitVec | 把1 转换成长2 bit的BitVec | Int2BV(Int('x'), 32) |
Real
成员函数
函数名 | 返回类型 | 说明 | 例 |
numerator | Int | 返回该数分数形式的分子 | Q(3,5).numerator() |
numerator_as_long | python int | 返回该数分数形式的分子 | Q(3,5).numerator() |
denominator | Int | 返回该数分数形式的分母 | RealVal(12.25).denominator() |
denominator_as_long | python int | 返回该数分数形式的分母 | RealVal("1/77").denominator_as_long() |
as_fraction | python Fraction | 得到该数的python Fraction对象 | RealVal("1/12").as_fraction() |
as_decimal | python string | 得到该数的小数形式并保留$1位小数 | RealVal("1/33").as_decimal(3) |
as_long | python int | 得到该数的python整数形式，如果该数不为整数则抛异常 | 同Int |
as_string | pyhton string | 同Int | 同Int |
运算
Int有的Real都有，同时Real特有
函数名 | 返回类型 | 说明 | 例 |
Cbrt | Real | 开三次方 | Cbrt(Real('x')) |
Sqrt | Real | 开平方 | Sqrt(Real('x')) |
ToInt | Int | 转换成Int类型 | ToInt(Real('x')) |
Bool
成员函数
无
运算
函数名 | 返回类型 | 说明 | 例 |
Xor | Bool | 异或表达式 | Xor(Bool('p'), Bool('q')) |
Not | Bool | 取非表达式 | Not(Bool('p')) |
And | Bool | 取与表达式 | And(Bool('p'), Bool('q'), Bool('w')) |
Or | Bool | 取或表达式 | Or(Bool('p'), Bool('q'), Bool('w')) |
Implies | Bool | 蕴含表达式 | Implies(Bool('p'), Bool('q')) |
有限类型
BitVec
成员函数
函数名 | 返回类型 | 说明 | 例 |
size | python int | 得到BitVec的长度 | len = BitVec('x', 12).size() |
运算
Int有的BitVec都有，长度不同的BitVec不能运算，且均为有符号运算、无符号运算见下。
函数名 | 返回类型 | 说明 | 例 |
BV2Int | Int | 把$1 转换成Int，$2 表示这个BitVec是否有符号 | BV2Int(BitVec('x', 32), is_signed=True) |
Concat | BitVec | 把参数中的Bitvec连接到一起 | Concat(BitVec('x', 16),BitVec('y', 16)) |
Extract | BitVec | 截取$3 从$2 到 $1，长度为$1 - $2 + 1bit的BitVec | Extract(6, 2, BitVec('x', 8)) |
RotateLeft | BitVec | 把$1 循环左移 $2位， RotateLeft(BitVec('x', 16),4)等价于Concat(Extract(11, 0, x), Extract(15, 12, x)) | RotateLeft(BitVec('x', 16),4) |
RotateRight | BitVec | 把$1 循环右移 $2位 | RotateRight(BitVec('x', 16),4) |
RepeatBitVec | BitVec | 重复$2，$1 次 RepeatBitVec(2, a)等价于Concat(a, a) | RepeatBitVec(4, BitVec('x', 8)) |
SignExt | BitVec | 得到一个带有$1 位前缀并填充 1的BitVec，SignExt(8, BitVec('x', 16)等价于Concat(RepeatBitVec(8, BitVecVal(1, 1)), BitVec('x', 16)) | SignExt(8, BitVec('x', 16)) |
ZeroExt | BitVec | 得到一个带有$1 位前缀并填充 0的BitVec | ZeroExt(8, BitVec('x', 16)) |
有符号与无符号运算表
运算 | 有符号 | 无符号 |
加法 | + | + |
减法 | - | - |
乘法 | * | * |
除法 | / | UDiv |
取模 | % | URem |
小于等于 | <= | ULE |
小于 | < | ULT |
大于等于 | >= | UGE |
大于 | > | UGT |
右移运算 | >> | LShR |
左移运算 | << | << |
FP
成员函数
函数名 | 返回类型 | 说明 | 例 |
ebits | python int | 得到浮点数的指数位长度 | ㅤ |
sbits | python int | 得到浮点数的有效位长度 | ㅤ |
运算
在看运算前，先看看浮点数的舍入规则，在z3中定义了5种IEEE舍入规则:
- RoundNearestTiesToEven
- RoundNearestTiesToAway
- RoundTowardPositive
- RoundTowardNegative
- RoundTowardZero
在IEEE 754-2019 27页中，我们找到了这五种舍入规则的定义。
函数名 | 别名 | 说明 |
RoundNearestTiesToEven | RNE | 向偶数舍入 |
RoundNearestTiesToAway | RNA | 最近舍入 |
RoundTowardPositive | RTP | 向+∞舍入 |
RoundTowardNegative | RTN | 向-∞舍入 |
RoundTowardZero | RTZ | 向0舍入 |
在C语言中默认的是RNE
函数名 | 返回类型 | 说明 | 例 |
fpNaN | FP | 创建一个值为NaN的FP | fpNaN(FPSort(8, 24)) |
fpPlusInfinit | FP | 创建一个值为+∞的FP | fpPlusInfinity(FPSort(8, 24)) |
fpMinusInfinity | FP | 创建一个值为-∞的FP | fpMinusInfinity(FPSort(8, 24)) |
fpInfinity | FP | 创建一个值为+∞ 或 -∞的FP | fpInfinity(FPSort(8, 24), False) |
fpPlusZero | FP | 创建一个值为+0.0的FP | fpPlusZero(FPSort(8, 24)) |
fpMinusZero | FP | 创建一个值为-0.0的FP | fpMinusZero(FPSort(8, 24)) |
fpZero | FP | 创建一个值为+0.0 或 -0.0的FP | fpZero(FPSort(8, 24), False) |
fpAbs | FP | 取绝对值 | fpAbs(x) |
fpNeg | FP | 取相反数 | fpAbs(Neg) |
fpAdd | FP | $2 和 $3按照$1舍入规则相加 | fpAdd(RNE(), x, y) |
fpSub | FP | $2 和 $3按照$1舍入规则相减 | fpSub(RNE(), x, y) |
fpMul | FP | $2 和 $3按照$1舍入规则相乘 | fpMul(RNE(), x, y) |
fpDiv | FP | $2 和 $3按照$1舍入规则相除 | fpDiv(RNE(), x, y) |
fpRem | FP | $2 和 $3按照$1舍入规则取模 | fpRem(RNE(), x, y) |
fpMin | FP | 取出$1与$2较小的一个 | fpMin(x, y) |
fpMax | FP | 取出$1与$2较大的一个 | fpMax(x, y) |
fpFMA | FP | 按照$1舍入规则计算$2 * 3 + $4，但整个过程只进行一次舍入 | fpFMA(RNE(), x, y, z) |
fpSqrt | FP | 按照$1 舍入规则进行开方 | fpSqrt(RNE(), x) |
fpRoundToIntegral | Int | 按照$1舍入规则，把$2取整 | fpRoundToIntegral(RNE(), a) |
fpIsNaN | Bool | 判断$1是否是NaN | fpIsNaN(x) |
fpIsInf | Bool | 判断$1是否是Inf | fpIsInf(x) |
fpIsZero | Bool | 判断$1是否是0 | fpIsZero(x) |
fpIsNormal | Bool | 但fpIsNaN、fpIsInf、fpIsZero都不成立时此表达式为True | fpIsNormal(x) |
fpIsNegative | Bool | 判断$1是否为负 | fpIsNegative(x) |
fpIsPositive | Bool | 判断$1是否为正 | fpIsPositive(x) |
fpLT | Bool | $1 < $2 | fpLT(a,b) |
fpLEQ | Bool | $1 <= $2 | fpLEQ(a,b) |
fpGT | Bool | $1 > $2 | fpGT(a,b) |
fpGEQ | Bool | $1 >= $2 | fpGEQ(a,b) |
fpEQ | Bool | $1 == $2 | fpEQ(a,b) |
fpNEQ | Bool | $1 != $2 | fpNEQ(a,b) |
fpBVToFP | FP | 把$1 按照IEEE编码转换成$2类型的浮点数 | fpBVToFP(BitVecVal(0x41440000, 32), Float32()) |
fpSignedToFP | FP | $2 按照$1 舍入规则转换成$3 类型 | fpSignedToFP(RNE(), BitVecVal(-5, 32), Float32()) |
fpUnsignedToFP | FP | $2 按照$1 舍入规则转换成$3 类型 | fpUnsignedToFP(RNE(), BitVecVal(-5, 32), Float32()) |
fpFPToFP | FP | $2 按照$1 舍入规则转换成$3 类型 | fpFPToFP(RNE(), FPVal(1.0, Float32()), Float64()) |
fpRealToFP | FP | $2 按照$1 舍入规则转换成$3 类型 | fpRealToFP(RNE(), RealVal(1.5), Float32()) |
fpToIEEEBV | BitVec | 把$1 按照IEEE编码转换成BitVec类型 | fpToIEEEBV(FP('x', FPSort(8, 24))) |
fpToSBV | BitVec | 把$2 按照$1舍入规则转换成有符号BitVec类型 | fpToSBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32))) |
fpToUBV | BitVec | 把$2 按照$1舍入规则转换成无符号BitVec类型 | fpToUBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32))) |
fpToReal | Real | 把$1 转换成Real类型 | fpToReal(x) |
String
成员函数
函数名 | 返回类型 | 说明 | 例 |
at | String | 取出第$1个位置的值 | StringVal('who am i').at(2) |
add | String | Concat($1, $2) | String('a') + String('b') |
运算
函数名 | 返回类型 | 说明 | 例 |
SubSeq | String | 从$2 偏移处在$1 中取出长度$3的子串 | SubSeq(s,0,4) |
PrefixOf | Bool | 判断$1 是否是$2 的前缀 | PrefixOf("ab", "abc") |
SuffixOf | Bool | 判断$1 是否是$2 的后缀 | SuffixOf("bc", "abc") |
Contains | Bool | 判断$1 是否包含$2 | Contains("abc", "bc") |
Replace | String | 把$1 中的第一个$2 字符替换成$3 | Replace("aaa", "a", "b") |
IndexOf | Int | 从$3 偏移开始在$1 中检索子串$2，$3默认为0 | IndexOf("abcabc", "bc") |
LastIndexOf | Int | 在$1 中检索子串$2 最后一个位置 | LastIndexOf("abcdc","dc") |
Length | Int | 取长度 | Length(StringVal('aaa')) |
StrToInt | Int | String转Int | StrToInt("1") |
IntToStr | String | Int转String | IntToStr(IntVal(31)) |
求解
一般情况下，用
Solver创建一个求解器，利用成员函数add添加约束，最后使用成员函数check进行求解，成员函数model()得到求解结果。
例如：a, b = Reals('a b') sol = Solver() sol.add(a + b == 128) sol.add(a - b == 64) assert sol.check() == sat rol = sol.model() print(f"a = {rol[a]}") print(f"b = {rol[b]}")
还有一个函数
solve则是直接在参数中添加约束。例如：
a = Int('a') solve(a > 0, a < 2)
z3 解Base64
from z3 import * from functools import reduce enc = "zPYeyPYqVUJtyf4=" table = StringVal("ZYXABCDEFGHIJKLMNOPQRSTUVWzyxabcdefghijklmnopqrstuvw0123456789+/") s = reduce(Concat, [Int2BV(If(i == '=', 0, IndexOf(table, i, 0)), 6) for i in enc]) st = reversed([chr(simplify(Extract(8 * (i + 1) - 1, 8 * i, s)).as_long()) for i in range(s.size() // 8)]) print(''.join(st))
实例
2021 ZJCTF初赛 Triple Language
import z3 checkBox = [194, 195, 215, 196, 218, 165, 160, 0xBE] checkBox2 = list(int.to_bytes(0x3EBB0EFAF301FC, length=8, byteorder="little")) raw2 = [z3.BitVec(f"a{str(i)}", 8) for i in range(8)] raw3 = [z3.BitVec(f"b{str(i)}", 8) for i in range(8)] slo = z3.Solver() for i in range(8): slo.add(raw2[i] + raw3[i] == checkBox[i]) slo.add(raw2[i] - raw3[i] == checkBox2[i]) assert slo.check() == z3.sat rlt = slo.model() flag2 = "".join([chr(rlt.eval(i).as_long()) for i in raw2]) flag3 = "".join([chr(rlt.eval(i).as_long()) for i in raw3])
# Part2 import z3 dword_1400034B0 = [0x00000000, 0xF26B8303, 0xE13B70F7, 0x1350F3F4, 0xC79A971F, 0x35F1141C, 0x26A1E7E8, 0xD4CA64EB, 0x8AD958CF, 0x78B2DBCC, 0x6BE22838, 0x9989AB3B, 0x4D43CFD0, 0xBF284CD3, 0xAC78BF27, 0x5E133C24, 0x105EC76F, 0xE235446C, 0xF165B798, 0x030E349B, 0xD7C45070, 0x25AFD373, 0x36FF2087, 0xC494A384, 0x9A879FA0, 0x68EC1CA3, 0x7BBCEF57, 0x89D76C54, 0x5D1D08BF, 0xAF768BBC, 0xBC267848, 0x4E4DFB4B, 0x20BD8EDE, 0xD2D60DDD, 0xC186FE29, 0x33ED7D2A, 0xE72719C1, 0x154C9AC2, 0x061C6936, 0xF477EA35, 0xAA64D611, 0x580F5512, 0x4B5FA6E6, 0xB93425E5, 0x6DFE410E, 0x9F95C20D, 0x8CC531F9, 0x7EAEB2FA, 0x30E349B1, 0xC288CAB2, 0xD1D83946, 0x23B3BA45, 0xF779DEAE, 0x05125DAD, 0x1642AE59, 0xE4292D5A, 0xBA3A117E, 0x4851927D, 0x5B016189, 0xA96AE28A, 0x7DA08661, 0x8FCB0562, 0x9C9BF696, 0x6EF07595, 0x417B1DBC, 0xB3109EBF, 0xA0406D4B, 0x522BEE48, 0x86E18AA3, 0x748A09A0, 0x67DAFA54, 0x95B17957, 0xCBA24573, 0x39C9C670, 0x2A993584, 0xD8F2B687, 0x0C38D26C, 0xFE53516F, 0xED03A29B, 0x1F682198, 0x5125DAD3, 0xA34E59D0, 0xB01EAA24, 0x42752927, 0x96BF4DCC, 0x64D4CECF, 0x77843D3B, 0x85EFBE38, 0xDBFC821C, 0x2997011F, 0x3AC7F2EB, 0xC8AC71E8, 0x1C661503, 0xEE0D9600, 0xFD5D65F4, 0x0F36E6F7, 0x61C69362, 0x93AD1061, 0x80FDE395, 0x72966096, 0xA65C047D, 0x5437877E, 0x4767748A, 0xB50CF789, 0xEB1FCBAD, 0x197448AE, 0x0A24BB5A, 0xF84F3859, 0x2C855CB2, 0xDEEEDFB1, 0xCDBE2C45, 0x3FD5AF46, 0x7198540D, 0x83F3D70E, 0x90A324FA, 0x62C8A7F9, 0xB602C312, 0x44694011, 0x5739B3E5, 0xA55230E6, 0xFB410CC2, 0x092A8FC1, 0x1A7A7C35, 0xE811FF36, 0x3CDB9BDD, 0xCEB018DE, 0xDDE0EB2A, 0x2F8B6829, 0x82F63B78, 0x709DB87B, 0x63CD4B8F, 0x91A6C88C, 0x456CAC67, 0xB7072F64, 0xA457DC90, 0x563C5F93, 0x082F63B7, 0xFA44E0B4, 0xE9141340, 0x1B7F9043, 0xCFB5F4A8, 0x3DDE77AB, 0x2E8E845F, 0xDCE5075C, 0x92A8FC17, 0x60C37F14, 0x73938CE0, 0x81F80FE3, 0x55326B08, 0xA759E80B, 0xB4091BFF, 0x466298FC, 0x1871A4D8, 0xEA1A27DB, 0xF94AD42F, 0x0B21572C, 0xDFEB33C7, 0x2D80B0C4, 0x3ED04330, 0xCCBBC033, 0xA24BB5A6, 0x502036A5, 0x4370C551, 0xB11B4652, 0x65D122B9, 0x97BAA1BA, 0x84EA524E, 0x7681D14D, 0x2892ED69, 0xDAF96E6A, 0xC9A99D9E, 0x3BC21E9D, 0xEF087A76, 0x1D63F975, 0x0E330A81, 0xFC588982, 0xB21572C9, 0x407EF1CA, 0x532E023E, 0xA145813D, 0x758FE5D6, 0x87E466D5, 0x94B49521, 0x66DF1622, 0x38CC2A06, 0xCAA7A905, 0xD9F75AF1, 0x2B9CD9F2, 0xFF56BD19, 0x0D3D3E1A, 0x1E6DCDEE, 0xEC064EED, 0xC38D26C4, 0x31E6A5C7, 0x22B65633, 0xD0DDD530, 0x0417B1DB, 0xF67C32D8, 0xE52CC12C, 0x1747422F, 0x49547E0B, 0xBB3FFD08, 0xA86F0EFC, 0x5A048DFF, 0x8ECEE914, 0x7CA56A17, 0x6FF599E3, 0x9D9E1AE0, 0xD3D3E1AB, 0x21B862A8, 0x32E8915C, 0xC083125F, 0x144976B4, 0xE622F5B7, 0xF5720643, 0x07198540, 0x590AB964, 0xAB613A67, 0xB831C993, 0x4A5A4A90, 0x9E902E7B, 0x6CFBAD78, 0x7FAB5E8C, 0x8DC0DD8F, 0xE330A81A, 0x115B2B19, 0x020BD8ED, 0xF0605BEE, 0x24AA3F05, 0xD6C1BC06, 0xC5914FF2, 0x37FACCF1, 0x69E9F0D5, 0x9B8273D6, 0x88D28022, 0x7AB90321, 0xAE7367CA, 0x5C18E4C9, 0x4F48173D, 0xBD23943E, 0xF36E6F75, 0x0105EC76, 0x12551F82, 0xE03E9C81, 0x34F4F86A, 0xC69F7B69, 0xD5CF889D, 0x27A40B9E, 0x79B737BA, 0x8BDCB4B9, 0x988C474D, 0x6AE7C44E, 0xBE2DA0A5, 0x4C4623A6, 0x5F16D052, 0xAD7D5351, 0xD76AA478] sol = z3.Solver() flag4 = [z3.BitVec(f"a{str(i)}", 8) for i in range(4)] mapping = z3.Array("mapping", z3.BitVecSort(32), z3.BitVecSort(32)) for i in range(len(dword_1400034B0)): sol.add(mapping[i] == dword_1400034B0[i]) # 太慢 # for i, v in enumerate(dword_1400034B0): # mapping = z3.Store(mapping, i, v) v1 = z3.BitVecVal(0xFFFFFFFF, 32) for i in range(4): idx = (z3.ZeroExt(24, flag4[i]) ^ v1) & 0xff v1 = z3.LShR(v1, 8) ^ mapping[idx] sol.add(~v1 & 0xffffffff == 0xCAFABCBC) assert sol.check() == z3.sat ros = sol.model() flag4 = "".join([chr(ros.eval(j).as_long()) for j in flag4]) print(flag4)
# Part3 import z3 key3 = list(b")8FP>6^B=G6@>X*P<G=B)1 ") key3[0] += 15 key3[1] ^= 0x6f key3[2] -= 12 key3[3] ^= 0x12 key3[4] -= 5 key3[5] += 33 key3[6] -= 12 key3[7] ^= 0xd key3[8] -= 3 key3[9] += 15 key3[10] ^= 0x68 key3[11] ^= 0xa key3[12] -= 5 key3[13] -= 33 key3[14] += 48 key3[15] ^= 0x18 key3[16] += 2 key3[17] -= 16 key3[18] ^= 0x1b key3[19] += 6 key3[20] ^= 0x13 flag5 = "" for i in range(0, len(key3), 4): sol = z3.Solver() if i < 5 * 4: raw4 = [z3.BitVec(f"a{str(j)}", 8) for j in range(3)] sol.add(((raw4[0] >> 2) + 33) == key3[i]) sol.add(((16 * raw4[0]) & 0x30 | (raw4[1] >> 4) & 0xff) + 33 == key3[i + 1]) sol.add(((4 * raw4[1]) & 0x3C | (raw4[2] >> 6) & 0xff) + 33 == key3[i + 2]) sol.add((raw4[2] & 0x3F) + 33 == key3[i + 3]) else: raw4 = [z3.BitVec(f"a{str(j)}", 8) for j in range(1)] sol.add((raw4[0] >> 2) + 33 == key3[i]) sol.add(((16 * raw4[0]) & 0x30) + 33 == key3[i+1]) assert sol.check() == z3.sat ros = sol.model() flag5 += "".join([chr(ros.eval(j).as_long()) for j in raw4 if isinstance(j, z3.BitVecRef)]) # print(flag5)