Solve with Z3 :)

equation.py

from z3 import Solver, IntVector

###### DO NOT EDIT
sVar2 = 20

__s = IntVector('__s', sVar2)

cVar1 = __s[16]
iVar3 = __s[6]
iVar4 = __s[4]
iVar5 = __s[10]
iVar6 = __s[0]
iVar7 = __s[8]
iVar8 = __s[19]
iVar9 = __s[13] * __s[16]
iVar11 = __s[11]
iVar12 = __s[5]
iVar13 = __s[9]
iVar14 = __s[14]
iVar15_0 = __s[7]
iVar15 = __s[12]
iVar16 = __s[17]
iVar17 = __s[18]
iVar18 = __s[15]
iVar19 = __s[2]
iVar20 = __s[3]

solver = Solver()
###### DO NOT EDIT


####### EDIT BELOW THIS LINE

iVar14 * iVar11 + iVar14 + iVar20 ==  0x2cbb
iVar3 * 2 - iVar11 == 0x7d
iVar15_0 * iVar11 == 0x1a59
(iVar12 - iVar4) - iVar3 == -0xa8
iVar13 * iVar5 * iVar14 + iVar17 == 0x8d125
__s[10] == ord('f')
iVar16 + iVar17 + iVar12 == 0xcb
iVar16 * iVar4 + iVar6 == 0x168a
iVar18 + iVar7 + iVar20 * iVar17 == 0x3119
iVar20 * iVar6 + iVar14 + iVar13 == 0x3037
(iVar12 - iVar20) + iVar20 * iVar12 == 0x1741
iVar8 * iVar11 * iVar19 + iVar15_0 == 0x127bb9
(iVar17 - iVar12) + iVar15_0 == 0x7b
iVar17 + iVar18 == 0x98
iVar20 * iVar14 * iVar6 == 0x15ecd6
iVar19 + iVar20 == 0xe1
iVar6 == ord('c')
iVar15 - iVar20 * iVar5 == -0x30b0
iVar14 + iVar13 + iVar14 * iVar6 == 0x2e48
iVar6 + iVar5 * 2 + iVar13 == 0x15f
iVar12 - iVar9 * iVar12 == -0x458a5
(iVar16 + iVar8) - iVar20 * iVar15 == -0x26b4
iVar15 - iVar17 + iVar6 == 0x50
iVar13 * iVar5 + iVar6 == 0x1383
iVar5 + iVar15 - iVar16 == 0x83
iVar14 - iVar20 * iVar14 == -0x383c
cVar1 == ord('r')
iVar13 - (iVar17 + iVar12) == -0x66
iVar19 == 0x66
iVar17 - iVar11 * iVar4 == -0x2750
iVar8 * iVar17 - iVar6 == 0x30ee
iVar16 * iVar12 * 0x66 == 0x40abe
iVar15 * iVar11 + iVar3 == 0x1edc
(iVar4 + iVar18) - iVar11 == 0x3f
iVar5 + iVar12 - __s[1] == 0x23
iVar18 * iVar17 * iVar12 + iVar5 == 0x3da55
iVar12 - iVar7 + iVar8 == 0x4f
iVar7 * iVar4 + cVar1 == 0x2827
__s[1] + iVar4 + iVar9 == 0x1795