Posted on 2026-01-04:: reverse

简介

Z3 solver 是由微软开发的 可满足性模理论求解器（Satisfiability Modulo Theory solver，即 SMT solver），用于检查逻辑表达式的可满足性，并可以找到一组约束中的其中一个可行解（无法找出所有的可行解）。

安装

$ uv add z3-solver

基础

先用一个简单的例子开头

from z3 import *

x = Int('x')
y = Int('y')
solve(2 < x, x < 100, x + 2*y == 7)

首先定义2个整数变量x, y, 再使用solve()求解约束条件

条件就是满足 $$ 2 < x < 100,x + 2y = 7,(x,y \in \mathbb{Z}) $$

这里可以看出, $x + 2y = 7$ 本身有无穷组整数解, 但是限定了 $x$ 的范围后变成了有限组解(49个解)

接下来使用更普遍的方法去做求解

import z3

# 创建求解器
s = z3.Solver()

# 创建变量
x = z3.Int("x")
y = z3.Int("y")

# 添加约束
s.add(x + y == 35)
s.add(2 * x + 4 * y == 94)

# 检查是否有解
if s.check() == z3.sat:
    m = s.model()
    print("鸡的数量:", m[x].as_long())
    print("兔的数量:", m[y].as_long())

使用z3求解鸡兔同笼的问题, 需要注意的是, 可以使用创建的变量作为键从model里取值, 但是其类型为ModelRef, 如果想用其参与python里的数学运算, 需要使用.as_long()方法变为int类型

解题

先看一道SECCON 2025的z3, 总共30个, 这里取一个

{
  "day": 1,
  "eqExprs": [
    "((((((((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) ^ 2936264725)) ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262))) + 88) - (((7784302 ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262)))) + 88))) | (-(((((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) ^ 2936264725)) ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262))) + 88) - (((7784302 ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262)))) + 88))))) >>> 31) ^ 1) === 1",
    "(((((((((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)) + 2936264725) - ((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 2936264725) << 1))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224))) + 89) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224)))) + 89))) | (-((((((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)) + 2936264725) - ((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 2936264725) << 1))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224))) + 89) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224)))) + 89))))) >>> 31) ^ 1) === 1",
    "(((((((((((~((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)))) & 2936264725) | (((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & (~2936264725)))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156))) + 128) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156)))) + 128))) | (-((((((((~((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)))) & 2936264725) | (((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & (~2936264725)))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156))) + 128) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156)))) + 128))))) >>> 31) ^ 1) === 1"
  ],
  "maskExprs": [
    "((((((((((x >>> 0)) ^ 1660657782) & 2634309513) ^ 42307)) - ((470042113 ^ 42307))) | (-(((((((x >>> 0)) ^ 1660657782) & 2634309513) ^ 42307)) - ((470042113 ^ 42307))))) >>> 31) ^ 1) === 1",
    "((((((((~((~((x >>> 0))) | 1660657782))) ^ 58922)) - ((470042113 ^ 58922))) | (-(((((~((~((x >>> 0))) | 1660657782))) ^ 58922)) - ((470042113 ^ 58922))))) >>> 31) ^ 1) === 1",
    "(((((((((x >>> 0)) & 2634309513) ^ 0 ^ 36529)) - ((470042113 ^ 36529))) | (-((((((x >>> 0)) & 2634309513) ^ 0 ^ 36529)) - ((470042113 ^ 36529))))) >>> 31) ^ 1) === 1"
  ]
}

eqExprs和maskExprs作为约束条件求解x, $x\in [0,4294967295]$, x正好是一个32位无符号整数

import z3

s = z3.Solver()

expr = {
    "day": 1,
    "eqExprs": [
        "((((((((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) ^ 2936264725)) ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262))) + 88) - (((7784302 ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262)))) + 88))) | (-(((((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) ^ 2936264725)) ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262))) + 88) - (((7784302 ^ ((((((((x >>> 0)) | 1384569162) + ((((x >>> 0)) & 1384569162) << 0))) & 61) ^ 58262)))) + 88))))) >>> 31) ^ 1) === 1",
        "(((((((((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)) + 2936264725) - ((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 2936264725) << 1))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224))) + 89) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224)))) + 89))) | (-((((((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)) + 2936264725) - ((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 2936264725) << 1))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224))) + 89) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 75) ^ 64224)))) + 89))))) >>> 31) ^ 1) === 1",
        "(((((((((((~((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)))) & 2936264725) | (((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & (~2936264725)))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156))) + 128) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156)))) + 128))) | (-((((((((~((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162)))) & 2936264725) | (((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & (~2936264725)))) ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156))) + 128) - (((7784302 ^ (((((((x >>> 0) | 1384569162) + ((x >>> 0) & 1384569162))) & 205) ^ 17156)))) + 128))))) >>> 31) ^ 1) === 1",
    ],
    "maskExprs": [
        "((((((((((x >>> 0)) ^ 1660657782) & 2634309513) ^ 42307)) - ((470042113 ^ 42307))) | (-(((((((x >>> 0)) ^ 1660657782) & 2634309513) ^ 42307)) - ((470042113 ^ 42307))))) >>> 31) ^ 1) === 1",
        "((((((((~((~((x >>> 0))) | 1660657782))) ^ 58922)) - ((470042113 ^ 58922))) | (-(((((~((~((x >>> 0))) | 1660657782))) ^ 58922)) - ((470042113 ^ 58922))))) >>> 31) ^ 1) === 1",
        "(((((((((x >>> 0)) & 2634309513) ^ 0 ^ 36529)) - ((470042113 ^ 36529))) | (-((((((x >>> 0)) & 2634309513) ^ 0 ^ 36529)) - ((470042113 ^ 36529))))) >>> 31) ^ 1) === 1",
    ],
}

x = z3.BitVec("x", 32)

for e in expr["eqExprs"]:
    s.add(eval(e.replace("===", "==").replace(">>>", ">>")))
for e in expr["maskExprs"]:
    s.add(eval(e.replace("===", "==").replace(">>>", ">>")))
if s.check() == z3.sat:
    m = s.model()
    print("solve:", m[x])

这里使用BitVec作为变量类型, 是因为Int不能参与位运算, 也不会溢出.

多解问题

对于约束条件 $$ 2 < x < 100,x + 2y = 7,(x,y \in \mathbb{Z}) $$

显然是有多解的, 解题中我们也会碰到多解的问题, 这时候就需要再往求解器添加约束条件, 我们可以使用生成器来方便地做这件事

import z3
from z3 import And, Not

def s():
    s = z3.Solver()
    x = z3.Int("x")
    y = z3.Int("y")

    s.add((x * x) + (y * y) == 16)
    while True:
        if s.check() == z3.sat:
            m = s.model()
            s.add(Not(And([m[i] == i for i in [x, y]])))
            yield m[x].as_long(), m[y].as_long()
        else:
            return

gen = s()

for i in range(100):
    try:
        v = next(gen)
        print(f"{i + 1}解: {v}")
    except:
        print("Done.")
        break

这里用Not(And([m[i] == i for i in [x, y]]))这个表达式来排除这一组特定的解

接下来以moectf 2025的一道z3题示例

__int64 __fastcall check(__int64 a1)
{
  int i; // [rsp+1Ch] [rbp-4h]

  for ( i = 0; i <= 33; ++i )
  {
    check(std::string)::b[i] = 47806 * (*(char *)std::string::operator[](a1, i) + i);
    if ( i )
      check(std::string)::b[i] ^= check(std::string)::b[i - 1] ^ 0x114514;
    check(std::string)::b[i] %= 51966;
    if ( check(std::string)::b[i] != a[i] )
      return 0;
  }
  return 1;
}

先初始化b[0], 之后的b[i]会多一步异或b[i-1] ^ 0x114514

import z3
from z3 import And, Not

target = [
    0x0B1B0, 0x5678, 0x7FF2, 0x0A332, 0x0A0E8, 0x364C, 0x2BD4, 0x0C8FE, 0x4A7C, 0x18, 0x2BE4, 0x4144, 0x3BA6, 0x0BE8C, 0x8F7E,
    0x35F8, 0x61AA, 0x2B4A, 0x6828, 0x0B39E, 0x0B542, 0x33EC, 0x0C7D8, 0x448C, 0x9310, 0x8808, 0x0ADD4, 0x3CC2, 0x796, 0x0C940, 0x4E32, 0x4E2E, 0x924A, 0x5B5C,
]

def s():
    flag = [z3.BitVec("flag[" + str(i) + "]", 32) for i in range(34)]
    s = z3.Solver()
    s.add((47806 * flag[0]) % 51966 == target[0])

    b = 47806 * flag[0] % 51966

    for i in range(34):
        s.add(32 <= flag[i], flag[i] <= 176)

    for i in range(1, 34):
        s.add(((47806 * (flag[i] + i)) ^ 0x114514 ^ b) % 51966 == target[i])
        b = ((47806 * (flag[i] + i)) ^ 0x114514 ^ b) % 51966

    while True:
        if s.check() == z3.sat:
            m = s.model()
            s.add(Not(And([m[i] == i for i in flag])))
            yield [m[i].as_long() for i in flag]
        else:
            return

gen = s()

for i in range(100):
    try:
        v = bytes(next(gen)).decode("utf-8")
        print(f"{i + 1}解: {v}")
    except:
        print("Done.")
        break

这样就成功拿到全部4个解