Int(name, ctx=None)，创建一个整数变量，name是名字
Ints (names, ctx=None)，创建多个整数变量，names是空格分隔名字
IntVal (val, ctx=None)，创建一个整数常量，有初始值，没名字。
对于实数类型的API与整数类型一致，向量(BitVec)则稍有区别：
Bitvec(name,bv,ctx=None)，创建一个位向量，name是他的名字，bv表示大小
BitVecs(name,bv,ctx=None)，创建一个有多变量的位向量，name是名字，bv表示大小
BitVecVal(val,bv,ctx=None)，创建一个位向量，有初始值，没名字。
常用函数：
- s=solver()，创建一个解的对象。
- s.add(条件)，为解增加一个限制条件
- s.check()，检查解是否存在，如果存在，会返回"sat"
- modul()，输出解得结果
solver.assertions()查看求解器已经添加的约束和约束的个数：
简单使用：
解一个二元一次方程：
x - y = 10
x+ y = 0
from z3 import *
x,y = Reals('x y')
solve(x-y==10,x+y==0)
例题：
[GDOUCTF 2023]Check_Your_Luck：
题目代码：
#include <iostream>
using namespace std;void flag_checker(int v, int w,int x,int y,int z); int main(){int v,w,x,y,z;cout << "Input 5 random number and check your luck ;)" << endl;cout << "Num1: ";cin >> v;cout << "Num2: ";cin >> w;cout << "Num3: ";cin >> x;cout << "Num4: ";cin >> y;cout << "Num5: ";cin >> z;cout << endl;flag_checker(v,w,x,y,z);
}void flag_checker(int v,int w, int x, int y, int z){if ((v * 23 + w * -32 + x * 98 + y * 55 + z * 90 == 333322) &&(v * 123 + w * -322 + x * 68 + y * 67 + z * 32 == 707724) &&(v * 266 + w * -34 + x * 43 + y * 8 + z * 32 == 1272529) &&(v * 343 + w * -352 + x * 58 + y * 65 + z * 5 == 1672457) &&(v * 231 + w * -321 + x * 938 + y * 555 + z * 970 == 3372367)){cout << "Congratulations, Here is your flag:\n";cout << "flag{" << v << "_" << w << "_" << x << "_" << y << "_" << z << "}" << endl;}else{cout << "\nSeems your luck is not in favor right now!\nBetter luck next time!" << endl;}}WP：
from z3 import *
v,w,x,y,z = Ints('v w x y z')
s = Solver()
s.add(v * 23 + w * -32 + x * 98 + y * 55 + z * 90 == 333322)
s.add(v * 123 + w * -322 + x * 68 + y * 67 + z * 32 == 707724)
s.add(v * 266 + w * -34 + x * 43 + y * 8 + z * 32 == 1272529)
s.add(v * 343 + w * -352 + x * 58 + y * 65 + z * 5 == 1672457)
s.add(v * 231 + w * -321 + x * 938 + y * 555 + z * 970 == 3372367)
s.check()
print(s.model())
