压缩包中共有四个文件
run.sh是启动程序的shell脚本从这个脚本中我们可以知道babyunic是可执行程序，放入IDA分析下
查看main函数，我们大概可以得知程序的主要逻辑是把用户输入的flag给sub_CBA这个函数，进行一顿运算赋值给s1，然后拿s1的值和&unk202020程序硬编码的数据进行比较。
分析一下sub_CBA这个函数的三个参数，v4是用户输入的字符串，s1是一个指针，迪桑参数是运行程序时命令行跟的参数func，参数分析完毕，进入sub_CBA函数。
看到这几个uc_开头的函数，让我想到了unicorn-engine，Unicorn是一个轻量级, 多平台, 多架构的CPU模拟器框架。分析这个函数得知这个函数的大概逻辑就是读取func文件然后使用unicorn-engine模拟执行，可以通过uc_open这个函数的参数得到字节码文件func的系统架构，参数的具体意思需要去github上看unicorn-engine源代码的注释。
这里只需要分析第一个和第二个参数就可以了
uc_open(3LL, 0x40000004LL, &uc_engine);
uc_open的定义：
UNICORN_EXPORT uc_err uc_open(uc_arch arch, uc_mode mode, uc_engine **uc); /* Close a Unicorn engine instance. NOTE: this must be called only when there is no longer any usage of @uc. This API releases some of @uc's cached memory, thus any use of the Unicorn API with @uc after it has been closed may crash your application. After this, @uc is invalid, and is no longer usable. @uc: pointer to a handle returned by uc_open() @return UC_ERR_OK on success, or other value on failure (refer to uc_err enum for detailed error). */
uc_arch的定义：
得知这个字节码是MIPS架构的程序
uc_mode的定义：
得知这个字节码是MIPS架构32bit的大端序的程序
// Architecture typetypedef enum uc_arch {
UC_ARCH_ARM = 1, // ARM architecture (including Thumb, Thumb-2)
UC_ARCH_ARM64, // ARM-64, also called AArch64
UC_ARCH_MIPS, // Mips architecture
UC_ARCH_X86, // X86 architecture (including x86 & x86-64)
UC_ARCH_PPC, // PowerPC architecture (currently unsupported)
UC_ARCH_SPARC, // Sparc architecture
UC_ARCH_M68K, // M68K architecture
UC_ARCH_MAX,
} uc_arch;// Mode typetypedef enum uc_mode {
UC_MODE_LITTLE_ENDIAN = 0, // little-endian mode (default mode)
UC_MODE_BIG_ENDIAN = 1 << 30, // big-endian mode
// arm / arm64
UC_MODE_ARM = 0, // ARM mode
UC_MODE_THUMB = 1 << 4, // THUMB mode (including Thumb-2)
UC_MODE_MCLASS = 1 << 5, // ARM's Cortex-M series (currently unsupported)
UC_MODE_V8 = 1 << 6, // ARMv8 A32 encodings for ARM (currently unsupported)
// mips
UC_MODE_MICRO = 1 << 4, // MicroMips mode (currently unsupported)
UC_MODE_MIPS3 = 1 << 5, // Mips III ISA (currently unsupported)
UC_MODE_MIPS32R6 = 1 << 6, // Mips32r6 ISA (currently unsupported)
UC_MODE_MIPS32 = 1 << 2, // Mips32 ISA
UC_MODE_MIPS64 = 1 << 3, // Mips64 ISA
// x86 / x64
UC_MODE_16 = 1 << 1, // 16-bit mode
UC_MODE_32 = 1 << 2, // 32-bit mode
UC_MODE_64 = 1 << 3, // 64-bit mode
// ppc
UC_MODE_PPC32 = 1 << 2, // 32-bit mode (currently unsupported)
UC_MODE_PPC64 = 1 << 3, // 64-bit mode (currently unsupported)
UC_MODE_QPX = 1 << 4, // Quad Processing eXtensions mode (currently unsupported)
// sparc
UC_MODE_SPARC32 = 1 << 2, // 32-bit mode
UC_MODE_SPARC64 = 1 << 3, // 64-bit mode
UC_MODE_V9 = 1 << 4, // SparcV9 mode (currently unsupported)
// m68k} uc_mode;根据分析得知func这段字节码是MIPS架构32bit的大端序的程序
由于IDA正常不转插件的情况下MIPS没办法看伪代码，所以我们上另一个神器Ghidra，这个程序可以分析MIPS架构的伪代码。
新建一个项目，然后导入func文件，接着选择架构
打开后默认应该是这样
在a区域按d会反汇编成汇编代码，然后单击b按钮，会出现c区域的伪代码，接着就可以愉快的分析伪代码了。
这两个参数就是func这个函数的参数，a1是用户输入，a2就相当于返回的值
然后上一层函数使用a2和程序硬编码数据做比较
func这个函数逻辑还是比较清楚的，只是这个42元的方程有点烦，看这一串括号都瘆得慌。这里就要用z3这个解方程神器了。
写有一个IDAPython脚本把程序中硬编码的数据dump出来，这里有一点需要注意，func函数是大端序，ida分析的硬编码数据如果以dword形式显示，是小端序，所以要注意处理这部分的数据，所以我的IDAPython脚本使用get_bytes按顺序取数据。
import binascii start = 0x202020 tmp = [] for i in range(42): tmp.append(binascii.hexlify(get_bytes(start,4))) start += 4 print tmp
['ffffff94', 'ffffff38', '00000126', 'ffffff28', 'fffffc10', '00000294', 'fffffc9e', '000006ea', '000000dc', '00000006', 'ffffff0c', 'fffffdf6', 'fffffa82', 'fffffcd0', '00000182', '000003de', '0000014e', '000002b2', 'fffff8d8', '00000174', 'fffffaa6', 'fffff9d4', '000001c2', 'fffff97c', '0000035a', '00000146', 'ffffff3c', 'fffffa14', '000001ce', '000007dc', 'fffffd48', '00000098', '0000085e', 'fffffdb0', 'ffffffbc', '0000036e', 'ffffff4e', 'fffff836', '000005c0', '000006ae', '00000694', '00000022']1
由func函数得知&unk_202020的数据应该是32位大端序的int类型数据，这里由于是有符号整型，我们如果需要用Python进行操作，就需要先转换类型
import ctypes tmp = ['ffffff94', 'ffffff38', '00000126', 'ffffff28', 'fffffc10', '00000294', 'fffffc9e', '000006ea', '000000dc', '00000006', 'ffffff0c', 'fffffdf6', 'fffffa82', 'fffffcd0', '00000182', '000003de', '0000014e', '000002b2', 'fffff8d8', '00000174', 'fffffaa6', 'fffff9d4', '000001c2', 'fffff97c', '0000035a', '00000146', 'ffffff3c', 'fffffa14', '000001ce', '000007dc', 'fffffd48', '00000098', '0000085e', 'fffffdb0', 'ffffffbc', '0000036e', 'ffffff4e', 'fffff836', '000005c0', '000006ae', '00000694', '00000022'] piParm2 = list(map(lambda x:z3.IntVal(ctypes.c_int32(int(x,16)).value),tmp))
这里解密代码，程序中有注释
from z3 import *
e = [0xFFFFFF94, 0xFFFFFF38, 0x00000126, 0xFFFFFF28, 0xFFFFFC10, 0x00000294, 0xFFFFFC9E, 0x000006EA, 0x000000DC,
0x00000006, 0xFFFFFF0C, 0xFFFFFDF6, 0xFFFFFA82, 0xFFFFFCD0, 0x00000182, 0x000003DE, 0x0000014E, 0x000002B2,
0xFFFFF8D8, 0x00000174, 0xFFFFFAA6, 0xFFFFF9D4, 0x000001C2, 0xFFFFF97C, 0x0000035A, 0x00000146, 0xFFFFFF3C,
0xFFFFFA14, 0x000001CE, 0x000007DC, 0xFFFFFD48, 0x00000098, 0x0000085E, 0xFFFFFDB0, 0xFFFFFFBC, 0x0000036E,
0xFFFFFF4E, 0xFFFFF836, 0x000005C0, 0x000006AE, 0x00000694, 0x00000022]
en = map(lambda x: ctypes.c_int32(x).value, e)
arr = [IntVal(i) for i in en]
param_2 = arr
param_1 = [Int('c%d' % i) for i in range(0x2a)]
solver = z3.Solver()
# for v in param_1:
# solver.add(v >= 0x0)
# solver.add(v <= 0xff)
solver.add(param_2[0] == (((((((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2]) -
param_1[3]) + param_1[4]) - param_1[5])
- param_1[6]) - param_1[7]) - param_1[8]) +
param_1[9] + param_1[10]) - param_1[0xb]) +
param_1[0xc]) - param_1[0xd]) - param_1[0xe]) +
param_1[0xf]) - param_1[0x10]) - param_1[0x11]) +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) +
param_1[0x15] + param_1[0x16] + param_1[0x17] +
param_1[0x18]) - param_1[0x19]) + param_1[0x1a]) -
param_1[0x1b]) + param_1[0x1c] + param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) + param_1[0x20]) -
param_1[0x21]) + param_1[0x22] + param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) + param_1[0x26]) -
param_1[0x27]) + param_1[0x28] + param_1[0x29])
solver.add(param_2[1] == ((((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) +
param_1[2]) - param_1[3]) -
param_1[4]) + param_1[5]) -
param_1[6]) - param_1[7]) - param_1[8])
- param_1[9]) + param_1[10]) -
param_1[0xb]) + param_1[0xc]) - param_1[0xd]
) - param_1[0xe]) + param_1[0xf]) -
param_1[0x10]) - param_1[0x11]) + param_1[0x12])
- param_1[0x13]) + param_1[0x14] + param_1[0x15]) -
param_1[0x16]) - param_1[0x17]) - param_1[0x18]) +
param_1[0x19]) - param_1[0x1a]) + param_1[0x1b]) -
param_1[0x1c]) - param_1[0x1d]) + param_1[0x1e] +
param_1[0x1f] + param_1[0x20] + param_1[0x21] +
param_1[0x22] + param_1[0x23]) - param_1[0x24]) -
param_1[0x25]) - param_1[0x26]) - param_1[0x27]) -
param_1[0x28]) + param_1[0x29])
solver.add(param_2[2] == (((((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3]) - param_1[4]) + param_1[5])
- param_1[6]) - param_1[7]) + param_1[8]) -
param_1[9]) - param_1[10]) - param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) + param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) + param_1[0x11] +
param_1[0x12] + param_1[0x13] + param_1[0x14] +
param_1[0x15]) - param_1[0x16]) + param_1[0x17] +
param_1[0x18] + param_1[0x19] + param_1[0x1a]) -
param_1[0x1b]) + param_1[0x1c]) - param_1[0x1d]) +
param_1[0x1e]) - param_1[0x1f]) + param_1[0x20] +
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) +
param_1[0x24] + param_1[0x25] + param_1[0x26]) -
param_1[0x27]) + param_1[0x28]) - param_1[0x29])
solver.add(param_2[3] == (((((((((((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2])
- param_1[3]) - param_1[4]) -
param_1[5]) + param_1[6] + param_1[7]) -
param_1[8]) - param_1[9]) - param_1[10]) -
param_1[0xb]) + param_1[0xc]) - param_1[0xd])
+ param_1[0xe]) - param_1[0xf]) + param_1[0x10])
- param_1[0x11]) + param_1[0x12] + param_1[0x13] +
param_1[0x14]) - param_1[0x15]) + param_1[0x16] +
param_1[0x17] + param_1[0x18]) - param_1[0x19]) -
param_1[0x1a]) + param_1[0x1b]) - param_1[0x1c]) +
param_1[0x1d] + param_1[0x1e]) - param_1[0x1f]) -
param_1[0x20]) - param_1[0x21]) + param_1[0x22]) -
param_1[0x23]) + param_1[0x24] + param_1[0x25] +
param_1[0x26]) - param_1[0x27]) + param_1[0x28] + param_1[0x29])
solver.add(param_2[4] == (((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) -
param_1[2]) + param_1[3]) -
param_1[4]) - param_1[5]) + param_1[6]
+ param_1[7] + param_1[8] + param_1[9])
- param_1[10]) + param_1[0xb] +
param_1[0xc]) - param_1[0xd]) +
param_1[0xe]) - param_1[0xf]) +
param_1[0x10] + param_1[0x11]) -
param_1[0x12]) + param_1[0x13]) - param_1[0x14]
) + param_1[0x15]) - param_1[0x16]) -
param_1[0x17]) - param_1[0x18]) + param_1[0x19]) -
param_1[0x1a]) - param_1[0x1b]) - param_1[0x1c]) +
param_1[0x1d] + param_1[0x1e] + param_1[0x1f]) -
param_1[0x20]) + param_1[0x21]) - param_1[0x22]) -
param_1[0x23]) + param_1[0x24]) - param_1[0x25]) +
param_1[0x26]) - param_1[0x27]) - param_1[0x28]) - param_1[0x29])
solver.add(param_2[5] == ((((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3] + param_1[4] + param_1[5] +
param_1[6] + param_1[7] + param_1[8]) -
param_1[9]) - param_1[10]) - param_1[0xb]
) - param_1[0xc]) - param_1[0xd]) -
param_1[0xe]) + param_1[0xf]) - param_1[0x10])
+ param_1[0x11]) - param_1[0x12]) + param_1[0x13]
+ param_1[0x14]) - param_1[0x15]) + param_1[0x16])
- param_1[0x17]) + param_1[0x18]) - param_1[0x19]) +
param_1[0x1a] + param_1[0x1b]) - param_1[0x1c]) +
param_1[0x1d]) - param_1[0x1e]) + param_1[0x1f] +
param_1[0x20] + param_1[0x21]) - param_1[0x22]) -
param_1[0x23]) - param_1[0x24]) + param_1[0x25]) -
param_1[0x26]) - param_1[0x27]) + param_1[0x28] + param_1[0x29])
solver.add(param_2[6] == (((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3] + param_1[4]) - param_1[5]) +
param_1[6] + param_1[7] + param_1[8] +
param_1[9]) - param_1[10]) + param_1[0xb] +
param_1[0xc]) - param_1[0xd]) + param_1[0xe] +
param_1[0xf] + param_1[0x10] + param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) - param_1[0x14])
- param_1[0x15]) - param_1[0x16]) - param_1[0x17]) +
param_1[0x18] + param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b] + param_1[0x1c] + param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) +
param_1[0x24] + param_1[0x25]) - param_1[0x26]) -
param_1[0x27]) + param_1[0x28]) - param_1[0x29])
solver.add(param_2[7] == ((((((((((((((((((((((((((((((param_1[0] + param_1[1]) - param_1[2])
- param_1[3]) - param_1[4]) + param_1[5]
+ param_1[6]) - param_1[7]) + param_1[8] +
param_1[9]) - param_1[10]) + param_1[0xb]) -
param_1[0xc]) + param_1[0xd]) - param_1[0xe]) +
param_1[0xf]) - param_1[0x10]) + param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) + param_1[0x14]) -
param_1[0x15]) + param_1[0x16]) - param_1[0x17]) -
param_1[0x18]) + param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b] + param_1[0x1c] + param_1[0x1d] +
param_1[0x1e] + param_1[0x1f] + param_1[0x20]) -
param_1[0x21]) + param_1[0x22]) - param_1[0x23]) +
param_1[0x24] + param_1[0x25] + param_1[0x26] +
param_1[0x27]) - param_1[0x28]) - param_1[0x29])
solver.add(param_2[8] == (((((((((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2]) +
param_1[3] + param_1[4]) - param_1[5]) +
param_1[6] + param_1[7] + param_1[8] +
param_1[9] + param_1[10]) - param_1[0xb])
- param_1[0xc]) + param_1[0xd]) -
param_1[0xe]) + param_1[0xf] + param_1[0x10] +
param_1[0x11] + param_1[0x12]) - param_1[0x13])
+ param_1[0x14] + param_1[0x15]) - param_1[0x16])
- param_1[0x17]) + param_1[0x18] + param_1[0x19] +
param_1[0x1a]) - param_1[0x1b]) + param_1[0x1c]) -
param_1[0x1d]) - param_1[0x1e]) - param_1[0x1f]) -
param_1[0x20]) - param_1[0x21]) + param_1[0x22]) -
param_1[0x23]) - param_1[0x24]) + param_1[0x25]) -
param_1[0x26]) - param_1[0x27]) + param_1[0x28]) - param_1[0x29])
solver.add(param_2[9] == (((((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2]) -
param_1[3]) + param_1[4] + param_1[5] +
param_1[6]) - param_1[7]) - param_1[8]) -
param_1[9]) - param_1[10]) + param_1[0xb] +
param_1[0xc] + param_1[0xd]) - param_1[0xe])
+ param_1[0xf] + param_1[0x10]) - param_1[0x11]
) - param_1[0x12]) + param_1[0x13] +
param_1[0x14]) - param_1[0x15]) - param_1[0x16]) -
param_1[0x17]) + param_1[0x18]) - param_1[0x19]) -
param_1[0x1a]) - param_1[0x1b]) + param_1[0x1c] +
param_1[0x1d] + param_1[0x1e]) - param_1[0x1f]) +
param_1[0x20] + param_1[0x21]) - param_1[0x22]) -
param_1[0x23]) - param_1[0x24]) - param_1[0x25]) +
param_1[0x26]) - param_1[0x27]) + param_1[0x28] + param_1[0x29])
solver.add(param_2[10] == ((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) +
param_1[2] + param_1[3]) -
param_1[4]) - param_1[5]) +
param_1[6] + param_1[7]) - param_1[8])
- param_1[9]) - param_1[10]) -
param_1[0xb]) + param_1[0xc] + param_1[0xd]
+ param_1[0xe]) - param_1[0xf]) +
param_1[0x10]) - param_1[0x11]) +
param_1[0x12] + param_1[0x13] + param_1[0x14])
- param_1[0x15]) + param_1[0x16]) - param_1[0x17]
) - param_1[0x18]) - param_1[0x19]) + param_1[0x1a]
) - param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d]) -
param_1[0x1e]) + param_1[0x1f] + param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) + param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) + param_1[0x26]) -
param_1[0x27]) + param_1[0x28] + param_1[0x29])
solver.add(param_2[0xb] == ((((((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2]
+ param_1[3] + param_1[4]) -
param_1[5]) + param_1[6] + param_1[7])
- param_1[8]) + param_1[9] + param_1[10]
) - param_1[0xb]) - param_1[0xc]) -
param_1[0xd]) - param_1[0xe]) + param_1[0xf]
) - param_1[0x10]) - param_1[0x11]) -
param_1[0x12]) + param_1[0x13] + param_1[0x14]) -
param_1[0x15]) + param_1[0x16]) - param_1[0x17]) +
param_1[0x18] + param_1[0x19] + param_1[0x1a] +
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d] +
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) +
param_1[0x24] + param_1[0x25]) - param_1[0x26]) -
param_1[0x27]) - param_1[0x28]) - param_1[0x29])
solver.add(param_2[0xc] == (((((((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) -
param_1[2]) - param_1[3]) +
param_1[4]) - param_1[5]) -
param_1[6]) + param_1[7] +
param_1[8]) - param_1[9]) +
param_1[10]) - param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) +
param_1[0xe]) - param_1[0xf]) +
param_1[0x10]) - param_1[0x11]) +
param_1[0x12]) - param_1[0x13]) -
param_1[0x14]) - param_1[0x15]) - param_1[0x16]
) + param_1[0x17]) - param_1[0x18]) +
param_1[0x19]) - param_1[0x1a]) + param_1[0x1b]) -
param_1[0x1c]) + param_1[0x1d]) - param_1[0x1e]) -
param_1[0x1f]) + param_1[0x20] + param_1[0x21] +
param_1[0x22]) - param_1[0x23]) - param_1[0x24]) -
param_1[0x25]) - param_1[0x26]) + param_1[0x27]) -
param_1[0x28]) - param_1[0x29])
solver.add(param_2[0xd] == (((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) +
param_1[2]) - param_1[3]) +
param_1[4]) - param_1[5]) +
param_1[6]) - param_1[7]) + param_1[8]
) - param_1[9]) + param_1[10]) -
param_1[0xb]) + param_1[0xc] + param_1[0xd]
+ param_1[0xe] + param_1[0xf]) -
param_1[0x10]) - param_1[0x11]) -
param_1[0x12]) + param_1[0x13] + param_1[0x14]
+ param_1[0x15]) - param_1[0x16]) -
param_1[0x17]) + param_1[0x18] + param_1[0x19]) -
param_1[0x1a]) - param_1[0x1b]) + param_1[0x1c] +
param_1[0x1d]) - param_1[0x1e]) - param_1[0x1f]) -
param_1[0x20]) + param_1[0x21]) - param_1[0x22]) -
param_1[0x23]) + param_1[0x24]) - param_1[0x25]) -
param_1[0x26]) - param_1[0x27]) + param_1[0x28]) - param_1[0x29])
solver.add(param_2[0xe] == (((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2]) -
param_1[3]) - param_1[4]) - param_1[5]) +
param_1[6]) - param_1[7]) + param_1[8] +
param_1[9] + param_1[10]) - param_1[0xb]) +
param_1[0xc]) - param_1[0xd]) - param_1[0xe]) +
param_1[0xf] + param_1[0x10] + param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) + param_1[0x16] + param_1[0x17] +
param_1[0x18]) - param_1[0x19]) + param_1[0x1a] +
param_1[0x1b] + param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) + param_1[0x20] +
param_1[0x21] + param_1[0x22] + param_1[0x23] +
param_1[0x24] + param_1[0x25] + param_1[0x26]) -
param_1[0x27]) - param_1[0x28]) - param_1[0x29])
solver.add(param_2[0xf] == ((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3] + param_1[4] + param_1[5]) -
param_1[6]) + param_1[7]) - param_1[8]) -
param_1[9]) - param_1[10]) + param_1[0xb] +
param_1[0xc] + param_1[0xd]) - param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) + param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) + param_1[0x16] + param_1[0x17] +
param_1[0x18] + param_1[0x19] + param_1[0x1a] +
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) + param_1[0x20]) -
param_1[0x21]) + param_1[0x22] + param_1[0x23] +
param_1[0x24] + param_1[0x25]) - param_1[0x26]) +
param_1[0x27] + param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x10] == ((((((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3]) - param_1[4]) - param_1[5]) +
param_1[6] + param_1[7] + param_1[8] +
param_1[9] + param_1[10]) - param_1[0xb]) +
param_1[0xc]) - param_1[0xd]) + param_1[0xe] +
param_1[0xf] + param_1[0x10]) - param_1[0x11]) +
param_1[0x12]) - param_1[0x13]) + param_1[0x14]) -
param_1[0x15]) - param_1[0x16]) - param_1[0x17]) -
param_1[0x18]) - param_1[0x19]) + param_1[0x1a] +
param_1[0x1b] + param_1[0x1c] + param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) + param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) + param_1[0x23]) -
param_1[0x24]) + param_1[0x25]) - param_1[0x26]) + param_1[0x27])
- param_1[0x28]) + param_1[0x29])
solver.add(param_2[0x11] == ((((((((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3] + param_1[4]) - param_1[5]) +
param_1[6] + param_1[7] + param_1[8]) -
param_1[9]) - param_1[10]) + param_1[0xb]) -
param_1[0xc]) + param_1[0xd] + param_1[0xe] +
param_1[0xf]) - param_1[0x10]) + param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) + param_1[0x14]) -
param_1[0x15]) + param_1[0x16]) - param_1[0x17]) -
param_1[0x18]) + param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) + param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) + param_1[0x23]) -
param_1[0x24]) + param_1[0x25]) - param_1[0x26]) + param_1[0x27] +
param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x12] == ((((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2]) -
param_1[3]) + param_1[4] + param_1[5]) -
param_1[6]) + param_1[7]) - param_1[8]) +
param_1[9] + param_1[10]) - param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) + param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) + param_1[0x11] +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) - param_1[0x16]) - param_1[0x17]) -
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) -
param_1[0x1b]) + param_1[0x1c] + param_1[0x1d] +
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) + param_1[0x22]) - param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) - param_1[0x26]) - param_1[0x27])
- param_1[0x28]) + param_1[0x29])
solver.add(param_2[0x13] == ((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3]) - param_1[4]) - param_1[5]) +
param_1[6]) - param_1[7]) - param_1[8]) -
param_1[9]) - param_1[10]) - param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) + param_1[0xe] +
param_1[0xf] + param_1[0x10]) - param_1[0x11]) +
param_1[0x12] + param_1[0x13] + param_1[0x14] +
param_1[0x15]) - param_1[0x16]) + param_1[0x17] +
param_1[0x18]) - param_1[0x19]) + param_1[0x1a] +
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d] +
param_1[0x1e] + param_1[0x1f] + param_1[0x20] + param_1[0x21])
- param_1[0x22]) + param_1[0x23]) - param_1[0x24]) -
param_1[0x25]) - param_1[0x26]) + param_1[0x27] + param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x14] == ((((((((((((((((((((((((((((((((((((param_1[0] + param_1[1]) - param_1[2]) -
param_1[3]) - param_1[4]) + param_1[5]) -
param_1[6]) + param_1[7]) - param_1[8]) -
param_1[9]) + param_1[10] + param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) + param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) + param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) + param_1[0x14] +
param_1[0x15]) - param_1[0x16]) + param_1[0x17] +
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) -
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) +
param_1[0x21]) - param_1[0x22]) + param_1[0x23] + param_1[0x24]
) - param_1[0x25]) + param_1[0x26]) - param_1[0x27]) +
param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x15] == (((((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2]) -
param_1[3]) + param_1[4] + param_1[5] +
param_1[6] + param_1[7]) - param_1[8]) -
param_1[9]) - param_1[10]) - param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) - param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) + param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) + param_1[0x14]) -
param_1[0x15]) + param_1[0x16] + param_1[0x17] +
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) -
param_1[0x24]) + param_1[0x25]) - param_1[0x26]) - param_1[0x27])
- param_1[0x28]) + param_1[0x29])
solver.add(param_2[0x16] == (((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3] + param_1[4] + param_1[5] +
param_1[6] + param_1[7]) - param_1[8]) +
param_1[9]) - param_1[10]) + param_1[0xb]) -
param_1[0xc]) + param_1[0xd] + param_1[0xe] +
param_1[0xf]) - param_1[0x10]) + param_1[0x11] +
param_1[0x12]) - param_1[0x13]) - param_1[0x14]) +
param_1[0x15] + param_1[0x16]) - param_1[0x17]) +
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d] +
param_1[0x1e] + param_1[0x1f]) - param_1[0x20]) +
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) + param_1[0x26]) - param_1[0x27]) + param_1[0x28] +
param_1[0x29])
solver.add(param_2[0x17] == (((((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3]) - param_1[4]) - param_1[5]) -
param_1[6]) - param_1[7]) + param_1[8]) -
param_1[9]) - param_1[10]) + param_1[0xb] +
param_1[0xc]) - param_1[0xd]) - param_1[0xe]) +
param_1[0xf]) - param_1[0x10]) - param_1[0x11]) +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) + param_1[0x16]) - param_1[0x17]) +
param_1[0x18] + param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d] +
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) + param_1[0x26]) - param_1[0x27]) - param_1[0x28]) -
param_1[0x29])
solver.add(param_2[0x18] == (((((((((((((((((((((((((param_1[0] + param_1[1]) - param_1[2]) +
param_1[3] + param_1[4]) - param_1[5]) +
param_1[6] + param_1[7]) - param_1[8]) +
param_1[9] + param_1[10]) - param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) - param_1[0xe]) +
param_1[0xf] + param_1[0x10] + param_1[0x11]) -
param_1[0x12]) + param_1[0x13] + param_1[0x14] +
param_1[0x15] + param_1[0x16] + param_1[0x17] +
param_1[0x18] + param_1[0x19]) - param_1[0x1a]) -
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d] +
param_1[0x1e]) - param_1[0x1f]) + param_1[0x20] +
param_1[0x21] + param_1[0x22]) - param_1[0x23]) - param_1[0x24]
) - param_1[0x25]) - param_1[0x26]) + param_1[0x27] +
param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x19] == ((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3]) - param_1[4]) + param_1[5] +
param_1[6]) - param_1[7]) + param_1[8] +
param_1[9] + param_1[10]) - param_1[0xb]) -
param_1[0xc]) + param_1[0xd]) - param_1[0xe]) +
param_1[0xf]) - param_1[0x10]) + param_1[0x11] +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) + param_1[0x16] + param_1[0x17]) -
param_1[0x18]) - param_1[0x19]) + param_1[0x1a]) -
param_1[0x1b]) + param_1[0x1c]) - param_1[0x1d]) +
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) +
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) + param_1[0x26]) - param_1[0x27]) + param_1[0x28] +
param_1[0x29])
solver.add(param_2[0x1a] == (((((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3] + param_1[4]) - param_1[5]) -
param_1[6]) + param_1[7]) - param_1[8]) -
param_1[9]) - param_1[10]) - param_1[0xb]) +
param_1[0xc]) - param_1[0xd]) + param_1[0xe]) -
param_1[0xf]) + param_1[0x10]) - param_1[0x11]) +
param_1[0x12]) - param_1[0x13]) - param_1[0x14]) +
param_1[0x15] + param_1[0x16] + param_1[0x17] +
param_1[0x18] + param_1[0x19]) - param_1[0x1a]) -
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) +
param_1[0x1e] + param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) + param_1[0x23] + param_1[0x24])
- param_1[0x25]) - param_1[0x26]) + param_1[0x27] + param_1[0x28] + param_1[0x29])
solver.add(param_2[0x1b] == (((((((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2]) -
param_1[3]) + param_1[4]) - param_1[5]) -
param_1[6]) - param_1[7]) - param_1[8]) -
param_1[9]) - param_1[10]) - param_1[0xb]) +
param_1[0xc] + param_1[0xd]) - param_1[0xe]) +
param_1[0xf] + param_1[0x10] + param_1[0x11] +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) - param_1[0x16]) - param_1[0x17]) +
param_1[0x18] + param_1[0x19] + param_1[0x1a]) -
param_1[0x1b]) + param_1[0x1c] + param_1[0x1d] +
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) + param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) - param_1[0x26]) - param_1[0x27]) - param_1[0x28]) -
param_1[0x29])
solver.add(param_2[0x1c] == ((((((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3] + param_1[4]) - param_1[5]) +
param_1[6] + param_1[7]) - param_1[8]) -
param_1[9]) + param_1[10] + param_1[0xb]) -
param_1[0xc]) + param_1[0xd]) - param_1[0xe]) +
param_1[0xf]) - param_1[0x10]) + param_1[0x11] +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) + param_1[0x16]) - param_1[0x17]) -
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) + param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) + param_1[0x22] + param_1[0x23] + param_1[0x24]) -
param_1[0x25]) - param_1[0x26]) + param_1[0x27] + param_1[0x28] + param_1[0x29])
solver.add(param_2[0x1d] == ((((((((((((((((((((((((((param_1[0] + param_1[1]) - param_1[2]) -
param_1[3]) - param_1[4]) + param_1[5] +
param_1[6] + param_1[7]) - param_1[8]) +
param_1[9]) - param_1[10]) - param_1[0xb]) +
param_1[0xc]) - param_1[0xd]) + param_1[0xe] +
param_1[0xf]) - param_1[0x10]) + param_1[0x11] +
param_1[0x12]) - param_1[0x13]) + param_1[0x14] +
param_1[0x15] + param_1[0x16] + param_1[0x17]) -
param_1[0x18]) + param_1[0x19] + param_1[0x1a]) -
param_1[0x1b]) + param_1[0x1c] + param_1[0x1d] + param_1[0x1e]
+ param_1[0x1f] + param_1[0x20]) - param_1[0x21]) -
param_1[0x22]) + param_1[0x23] + param_1[0x24]) - param_1[0x25])
+ param_1[0x26] + param_1[0x27]) - param_1[0x28]) + param_1[0x29])
solver.add(param_2[0x1e] == ((((((((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3]) - param_1[4]) - param_1[5]) -
param_1[6]) - param_1[7]) + param_1[8] +
param_1[9]) - param_1[10]) - param_1[0xb]) -
param_1[0xc]) + param_1[0xd]) - param_1[0xe]) -
param_1[0xf]) + param_1[0x10]) - param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) + param_1[0x14]) -
param_1[0x15]) - param_1[0x16]) + param_1[0x17] +
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) + param_1[0x23] + param_1[0x24] +
param_1[0x25]) - param_1[0x26]) + param_1[0x27] + param_1[0x28] + param_1[0x29])
solver.add(param_2[0x1f] == ((((((((((((((((((((((((((((((param_1[0] + param_1[1]) - param_1[2]) +
param_1[3] + param_1[4]) - param_1[5]) -
param_1[6]) + param_1[7] + param_1[8] +
param_1[9] + param_1[10] + param_1[0xb] +
param_1[0xc]) - param_1[0xd]) - param_1[0xe]) -
param_1[0xf]) + param_1[0x10] + param_1[0x11] +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) +
param_1[0x15]) - param_1[0x16]) + param_1[0x17]) -
param_1[0x18]) - param_1[0x19]) + param_1[0x1a] +
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) +
param_1[0x21]) - param_1[0x22]) + param_1[0x23]) -
param_1[0x24]) + param_1[0x25]) - param_1[0x26]) + param_1[0x27])
- param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x20] == (((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3]) - param_1[4]) + param_1[5] +
param_1[6] + param_1[7] + param_1[8]) -
param_1[9]) + param_1[10] + param_1[0xb]) -
param_1[0xc]) + param_1[0xd] + param_1[0xe]) -
param_1[0xf]) + param_1[0x10]) - param_1[0x11]) +
param_1[0x12] + param_1[0x13] + param_1[0x14]) -
param_1[0x15]) - param_1[0x16]) + param_1[0x17]) -
param_1[0x18]) + param_1[0x19] + param_1[0x1a] +
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) + param_1[0x22] + param_1[0x23] + param_1[0x24] +
param_1[0x25]) - param_1[0x26]) + param_1[0x27]) - param_1[0x28]) + param_1[0x29])
solver.add(param_2[0x21] == (((((((((((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2]) +
param_1[3] + param_1[4] + param_1[5] +
param_1[6]) - param_1[7]) - param_1[8]) +
param_1[9] + param_1[10] + param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) + param_1[0xe] +
param_1[0xf]) - param_1[0x10]) + param_1[0x11]) -
param_1[0x12]) + param_1[0x13]) - param_1[0x14]) +
param_1[0x15] + param_1[0x16] + param_1[0x17]) -
param_1[0x18]) - param_1[0x19]) + param_1[0x1a] +
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) +
param_1[0x24]) - param_1[0x25]) + param_1[0x26]) - param_1[0x27])
- param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x22] == ((((((((((((((((((((((((((((((param_1[0] + param_1[1]) - param_1[2]) +
param_1[3]) - param_1[4]) - param_1[5]) -
param_1[6]) + param_1[7] + param_1[8] +
param_1[9] + param_1[10] + param_1[0xb]) -
param_1[0xc]) - param_1[0xd]) - param_1[0xe]) +
param_1[0xf]) - param_1[0x10]) + param_1[0x11]) -
param_1[0x12]) + param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) + param_1[0x16] + param_1[0x17]) -
param_1[0x18]) - param_1[0x19]) + param_1[0x1a] +
param_1[0x1b] + param_1[0x1c] + param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) - param_1[0x24]
) + param_1[0x25] + param_1[0x26] + param_1[0x27]) - param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x23] == ((((((((((((((((((((((((((param_1[0] - param_1[1]) + param_1[2] +
param_1[3] + param_1[4]) - param_1[5]) -
param_1[6]) + param_1[7] + param_1[8]) -
param_1[9]) - param_1[10]) + param_1[0xb] +
param_1[0xc] + param_1[0xd]) - param_1[0xe]) -
param_1[0xf]) + param_1[0x10]) - param_1[0x11]) +
param_1[0x12] + param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) - param_1[0x16]) + param_1[0x17] +
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b] + param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) + param_1[0x1f] + param_1[0x20]) - param_1[0x21])
+ param_1[0x22] + param_1[0x23] + param_1[0x24] + param_1[0x25] +
param_1[0x26] + param_1[0x27]) - param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x24] == (((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2]) -
param_1[3]) - param_1[4]) - param_1[5]) -
param_1[6]) + param_1[7] + param_1[8] +
param_1[9]) - param_1[10]) + param_1[0xb] +
param_1[0xc]) - param_1[0xd]) + param_1[0xe] +
param_1[0xf] + param_1[0x10] + param_1[0x11] +
param_1[0x12] + param_1[0x13] + param_1[0x14] +
param_1[0x15]) - param_1[0x16]) - param_1[0x17]) +
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) -
param_1[0x1b]) - param_1[0x1c]) + param_1[0x1d] +
param_1[0x1e] + param_1[0x1f] + param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) -
param_1[0x24]) + param_1[0x25]) - param_1[0x26]) + param_1[0x27] +
param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x25] == ((((((((((((((((((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2])
+ param_1[3]) - param_1[4]) + param_1[5]
) - param_1[6]) - param_1[7]) - param_1[8]
) - param_1[9]) + param_1[10]) - param_1[0xb]
) - param_1[0xc]) - param_1[0xd]) - param_1[0xe]
) - param_1[0xf]) - param_1[0x10]) + param_1[0x11]
+ param_1[0x12]) - param_1[0x13]) - param_1[0x14]) -
param_1[0x15]) + param_1[0x16]) - param_1[0x17]) +
param_1[0x18]) - param_1[0x19]) - param_1[0x1a]) +
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) +
param_1[0x1e] + param_1[0x1f]) - param_1[0x20]) +
param_1[0x21]) - param_1[0x22]) + param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) + param_1[0x26]) - param_1[0x27])
- param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x26] == ((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3]) - param_1[4]) + param_1[5] +
param_1[6] + param_1[7]) - param_1[8]) -
param_1[9]) - param_1[10]) + param_1[0xb] +
param_1[0xc] + param_1[0xd]) - param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) - param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) + param_1[0x14] +
param_1[0x15]) - param_1[0x16]) + param_1[0x17] +
param_1[0x18] + param_1[0x19] + param_1[0x1a] +
param_1[0x1b]) - param_1[0x1c]) - param_1[0x1d]) +
param_1[0x1e] + param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) + param_1[0x22]) - param_1[0x23]) - param_1[0x24]
) - param_1[0x25]) + param_1[0x26] + param_1[0x27] + param_1[0x28]) - param_1[0x29])
solver.add(param_2[0x27] == (((((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2]) -
param_1[3]) - param_1[4]) + param_1[5]) -
param_1[6]) - param_1[7]) - param_1[8]) +
param_1[9]) - param_1[10]) + param_1[0xb]) -
param_1[0xc]) + param_1[0xd] + param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) - param_1[0x11]) +
param_1[0x12] + param_1[0x13] + param_1[0x14] +
param_1[0x15] + param_1[0x16]) - param_1[0x17]) +
param_1[0x18] + param_1[0x19] + param_1[0x1a] + param_1[0x1b]
+ param_1[0x1c]) - param_1[0x1d]) + param_1[0x1e] +
param_1[0x1f] + param_1[0x20] + param_1[0x21] + param_1[0x22]) -
param_1[0x23]) - param_1[0x24]) + param_1[0x25] + param_1[0x26] +
param_1[0x27]) - param_1[0x28]) + param_1[0x29])
solver.add(param_2[0x28] == ((((((((((((((((((((((param_1[0] - param_1[1]) - param_1[2]) -
param_1[3]) + param_1[4] + param_1[5] + param_1[6]
) - param_1[7]) + param_1[8] + param_1[9]) -
param_1[10]) + param_1[0xb]) - param_1[0xc]) -
param_1[0xd]) - param_1[0xe]) + param_1[0xf] +
param_1[0x10] + param_1[0x11] + param_1[0x12] +
param_1[0x13] + param_1[0x14] + param_1[0x15] +
param_1[0x16]) - param_1[0x17]) + param_1[0x18] +
param_1[0x19]) - param_1[0x1a]) + param_1[0x1b] +
param_1[0x1c]) - param_1[0x1d]) + param_1[0x1e] + param_1[0x1f]
+ param_1[0x20]) - param_1[0x21]) - param_1[0x22]) +
param_1[0x23] + param_1[0x24]) - param_1[0x25]) + param_1[0x26] + param_1[0x27] + param_1[
0x28] + param_1[0x29])
solver.add(param_2[0x29] == (((((((((((((((((((((((((((((((param_1[0] + param_1[1] + param_1[2] +
param_1[3] + param_1[4] + param_1[5] +
param_1[6]) - param_1[7]) - param_1[8]) -
param_1[9]) + param_1[10] + param_1[0xb]) -
param_1[0xc]) + param_1[0xd]) - param_1[0xe]) -
param_1[0xf]) - param_1[0x10]) - param_1[0x11]) -
param_1[0x12]) - param_1[0x13]) + param_1[0x14]) -
param_1[0x15]) + param_1[0x16]) - param_1[0x17]) -
param_1[0x18]) + param_1[0x19] + param_1[0x1a] +
param_1[0x1b] + param_1[0x1c]) - param_1[0x1d]) -
param_1[0x1e]) - param_1[0x1f]) - param_1[0x20]) -
param_1[0x21]) - param_1[0x22]) - param_1[0x23]) -
param_1[0x24]) - param_1[0x25]) - param_1[0x26]) - param_1[0x27]) - param_1[0x28]) +
param_1[0x29])
flag = ''
if solver.check() == sat:
r = solver.model()
for i in range(0x2a):
temp = r[param_1[i]].as_long() ^ i
temp = (temp >> 3 | temp << 5) & 0xFF
flag += chr(temp)
print flag
#SUCTF{Un1c0rn_Engin3_Is_@_P0wer7ul_TO0ls!}