1.Z3约束器简介：
1.Z3约束器是干啥的？
z3是由微软公司开发的一个优秀的SMT求解器，它能够检查逻辑表达式的可满足性，通俗的来讲我们可以简单理解为它是一个解方程的计算器
使用文档
2.安装：
2.使用教程：
1.声明未知数：
其中BitVec可以是特定大小的数据类型，不一定是8，例如C语言中的int型可以用BitVec('a',32)表示
For Example：
2.常用API：
3.For Example：
对于求解一个方程来说一般可以分为四步：设未知数、列方程、求解方程、得到正解
假设有方程组：
如果用Z3来解的话：
3.z3解决数学问题：
实战例题：
EXEinfo：
64位，无壳，ELF文件
运行一下：
查看主函数：
主函数的逻辑很清晰，scanf接受值，然后if里调用一个函数，根据返回值判断输入Congratulations!或者Wrong。可以看到如果判断成功还会调用一个函数，函数里面是异或并且输出flag。
子函数分析：
函数显示判断输入字符串的长度是否为32,然后与另外三个值进行一些算数运算后看是否等于四个不同的常数，看到这的时候有个疑问，这个判断只用到了输入字符串的前32位，后面的没有用到，这里跟踪到数据段就可以解开异或
s确实只用到了四个字节但这个地址是连续的，而之前判断过输入字串的串长为32位也就是说要想知道输入还需要得到x,z,y,a,b,c,d。(注意排列顺序不是xyz)
- 求解x，z，y：
四个if判断后紧接着就是设置随机数的种子，这里用到了也是之前if判断的三个值和输入的字符串，srand函数是个关键，它决定了后面一大串随机数值的生成，这里需要得出随机数的种子值：(简化一下这四个if判断)
这一看就得构造一个四元一次方程，使用z3模块编写脚本：
输出结果为：
然后计算srand的值：
- 求解a，b，c，d：
上一步我们已经拿到了随机数的种子，那么现在对于我们来说未知数就只有v2，v3，v4，v5了，下面先将v6到v13get。
转到linux系统生成rand函数(在随机数那篇笔记有提到为啥不用Windows):
程序运行结果为：
现在就可以列方程求解四元一次方程了：
运行结果为：
至此输入的字串的值就全到手了，将它排列好：
使用python的
libnum 库将数字串转换成字符串：输入密码可直接获取flag，另外一个函数就是rand函数与已知值进行异或获得flag，随机数种子就是输入的密码，这里就不进行分析了：
flag{th3_Line@r_4lgebra_1s_d1fficult!}