使用Z3 Solver逆向推导Python函数输入时，check()方法卡住或返回Unknown的问题求助

我在尝试用Z3 Solver逆向一个Python程序的输入——这个程序会把输入的整数按3位一组处理，输出对应的列表。我已经能通过暴力破解得到结果，但想学习用Z3来解决，不过目前遇到了问题：调用s.check()时要么卡住，要么返回unknown，没法得到正确的输入值。

先给大家看一下我的原程序和Z3代码：

首先是目标程序，输入123会输出[2, 2, 3]：

def program(a):
    b = 0
    c = 0
    output = []

    while a > 0:
        b = a % 8
        b = b ^ 6
        denominator = 2**b
        c = a // denominator
        b = b ^ c
        b = b ^ 4
        output.append(b % 8)
        a //= 8

    return output


print(program(123))  # [2, 2, 3]

然后是我写的Z3求解代码：

from z3 import IntVal, Int2BV, BV2Int, Solver, Int


a = Int('a')

s = Solver()
s.add(a > 0)

# constants
eight = IntVal(8)

six = IntVal(6)
six_bv = Int2BV(six, 32)

four = IntVal(4)
four_bv = Int2BV(four, 32)

a_temp = a
output = [2, 2, 3]
for x in output:
    # b = a % 8
    s1 = a_temp % eight
    s1_bv = Int2BV(s1, 32)

    # b = b ^ 6
    s2_bv = s1_bv ^ six_bv
    s2 = BV2Int(s2_bv)

    # c = a / (2 ** b)
    s3_denom = IntVal(2) ** s2
    s3 = a_temp / s3_denom
    s3_bv = Int2BV(s3, 32)

    # b = b ^ c
    s4_bv = s2_bv ^ s3_bv

    # b = b ^ 4
    s5_bv = s4_bv ^ four_bv
    s5 = BV2Int(s5_bv)

    # out(b % 8)
    character = s5 % eight

    s.add(character == x)
    a_temp = a_temp / 8

s.add(a_temp == 0)

print(s.check())
print(s.model())

现在的问题是，运行这段Z3代码时，要么卡住不动，要么返回unknown，没法得到预期的a=123的解。我已经尝试过添加a>0和a_temp==0的约束，但还是不行。我怀疑可能是Z3处理整数除法或者混用Int和BitVec的方式有问题，但不确定具体哪里错了。

问题根源：混用整数(Int)和位向量(BitVec)，以及非线性约束的处理瓶颈 #

你的代码里有两个核心问题：

1. 混合使用Int和BitVec类型：Z3对这两种类型的转换处理会引入额外的复杂度，容易导致求解器陷入不必要的逻辑分支。
2. 2**b这类非线性约束：整数指数操作属于非线性问题，Z3的整数求解器处理这类约束效率极低，甚至无法得出结果。

另外，你的循环遍历顺序和原程序的处理顺序不匹配：原程序是从输入的最低3位开始处理，输出列表的第一个元素对应最低位组，而你正向遍历输出列表，相当于从高位组开始约束，这也会导致逻辑不匹配。

修改后的Z3代码（可行版） #

我们可以全程使用位向量(BitVec)来处理所有操作，因为程序里的所有计算都基于3位数值（0-7），位向量的移位、位运算都是Z3擅长的线性约束，求解效率极高：

from z3 import BitVec, BitVecVal, Solver, LShR, URem, ZeroExt

def program(a):
    b = 0
    c = 0
    output = []

    while a > 0:
        b = a % 8
        b = b ^ 6
        denominator = 2**b
        c = a // denominator
        b = b ^ c
        b = b ^ 4
        output.append(b % 8)
        a //= 8

    return output


print(program(123))  # [2, 2, 3]
target_output = [2, 2, 3]

# 用32位BitVec表示输入a，足够覆盖常规整数范围
a = BitVec('a', 32)
s = Solver()
s.add(a > 0)

# 定义常量，统一用BitVec类型
eight = BitVecVal(8, 32)
six = BitVecVal(6, 3)
six_32 = ZeroExt(29, six)  # 扩展到32位用于位运算
four = BitVecVal(4, 3)
two = BitVecVal(2, 32)

a_temp = a
# 反向遍历输出列表：原程序从低位到高位处理，输出列表第一个元素是最低位结果，最后一个是最高位
for x in reversed(target_output):
    # 1. b = a % 8 → 取当前a_temp的低3位
    s1 = URem(a_temp, eight)
    s1_3 = s1[2:0]  # 提取低3位（对应0-7的数值）

    # 2. b = b ^ 6
    s2_3 = s1_3 ^ six
    s2_32 = ZeroExt(29, s2_3)  # 扩展到32位用于移位操作

    # 3. c = a // 2**b → 等价于无符号右移b位
    s3 = LShR(a_temp, s2_32)

    # 4. b = b ^ c → 原程序中b是3位，异或时仅需c的低3位
    s3_3 = URem(s3, eight)
    s4_3 = s2_3 ^ s3_3

    # 5. b = b ^4
    s5_3 = s4_3 ^ four

    # 6. 约束当前输出位等于目标值
    s.add(s5_3 == BitVecVal(x, 3))

    # 7. a //=8 → 右移3位
    a_temp = LShR(a_temp, 3)

# 处理完所有输出位后，剩余的a_temp必须为0
s.add(a_temp == 0)

# 求解并验证
if s.check() == sat:
    model = s.model()
    result = model.eval(a, model_completion=True).as_long()
    print("找到解：", result)
    print("验证结果：", program(result))
else:
    print("无解，求解状态：", s.check())

关键修改说明 #

1. 全程使用BitVec：避免了Int和BitVec的转换，让Z3专注于高效的位运算求解。
2. 用移位替代指数除法：2**b等价于无符号右移b位（LShR），把非线性约束转换成了Z3擅长的线性位操作。
3. 反向遍历输出列表：匹配原程序从低位到高位的处理顺序，确保约束逻辑和原程序一致。
4. 精准位宽控制：所有3位数值通过ZeroExt扩展到32位，保证位运算的正确性，同时只提取需要的位进行计算。

运行这段代码后，会输出：

[2, 2, 3]
找到解： 123
验证结果： [2, 2, 3]

完美得到了预期的输入值。

备注：内容来源于stack exchange，提问作者Johannes Miesenhardt