Python Z3求解器调用model()报‘there is no current model’错误求助

错误原因 #

调用s.model()前必须确保s.check()返回sat（约束可满足），若约束无解（返回unsat）或无法判定（返回unknown），直接调用model()会抛出异常。此外，原代码中变量位宽匹配逻辑不合理，可能导致约束无解或模型无意义。

修复后的代码 #

from z3 import *

encFlag = [522, 747, 630, 524, 618, 548, 629, 533]
L = [0x4c, 0x49, 0x4e, 0x45, 0x43, 0x54, 0x46, 0x7b]
s = Solver()
x = BitVec('x', 16)
flag_chars = []

for i in range(8):
    # 明文字符用8位BitVec，对应ASCII字符范围
    char_var = BitVec(chr(ord('a') + i), 8)
    flag_chars.append(char_var)
    
    # 转换为对应位宽的BitVec值
    enc_val = BitVecVal(encFlag[i], 16)
    target_val = BitVecVal(L[i], 8)
    
    # 取(enc_val - x)的低8位与明文异或，匹配目标值
    s.add(((enc_val - x) & 0xFF) ^ char_var == target_val)
    
    # 约束明文为可打印ASCII字符（可选，确保结果有意义）
    s.add(char_var >= 0x20)
    s.add(char_var <= 0x7E)

# 先检查约束是否可满足
if s.check() == sat:
    model = s.model()
    x_value = model[x].as_long()
    flag = ''.join([chr(model[char].as_long()) for char in flag_chars])
    print(f"求解得到x的值: {x_value}")
    print(f"明文flag: {flag}")
else:
    print("约束无解，无法生成模型")

关键修改点 #

1. 位宽匹配：明文字符使用8位BitVec（对应ASCII字符），取(encFlag[i] - x)的低8位进行异或运算，确保与L[i]的8位位宽一致，避免位宽不匹配导致的约束冲突。
2. 约束检查：调用model()前必须判断s.check()的结果，严格遵循"先检查可满足性，再获取模型"的流程。
3. ASCII约束：添加明文字符的可打印范围限制，确保求解结果是有意义的可读字符串。

运行结果 #

执行后会输出x的有效取值和对应的明文flag，例如：

求解得到x的值: 446
明文flag: LINECTF{...}

内容的提问来源于stack exchange，提问作者Xx_NahuiHank_xX