Tags: z3 rev 

Rating: 1.0

today I'm too lazy to write a beautiful write-up, so only a script :D

briefly it's the most common rev task with equation, it's just check flag in different threads.

```
from z3_staff import * # https://github.com/KosBeg/z3_staff

create_vars(45, size=8, step=8)
solver()
init_vars(globals())
set_ranges(step=8)

add_eq(9*x200+5*x64+x296*28*x184+6*x104-6*x136-3*x208-2*x288-6*x32-10*x232-8*x24+x192*99*x72+4*x152+x88*84*x96==1373634)
add_eq(-11*x184+9*x288+-7*x288+x304*78*x0-8*x320-x320-x336*10*x272-7*x288+x288+x104*x112*560*x272-x256+11*x256+15*x280==805471623)
add_eq(2*x96+x24*225*x0-12*x288-7*x24-x344*12*x56-12*x344-x0-x32*18*x232-x88*x168*75*x16+12*x96+15*x200==-31526095)
add_eq(5*x184+x8+4*(2*x232-x144-x168)+x224*39*x96-x288*x176*30*x168+8*x208-x208+x144+12*x0-10*x136-12*x216*x136==-20510795)
add_eq(x144+5*x296+15*x344+x128+11*x104+x48*15*x184-6*x160-x64*10*x184+135*x160*x48+10*x152-6*x144+14*x16-12*x264==1333282)
add_eq(x80*x0*182*x192+x256*2*x240-4*x312-x312+10*x256+8*x136-8*x240+4*x272-12*x232-x96*55*x328+x64*x32*1144*x136==1381453791)
add_eq(-7*x160+-3*x344+x232-7*x280+11*x272-x312*x208*18*x296-4*x0+2*x64-8*x216+8*x120-x120-x208*8*x264-13*x208==-19729480)
add_eq(13*x232+x288*132*x0+13*x152+3*x8-x240*14*x240+x272*60*x24-14*x208-8*x224-x224+3*x152+10*x56-x32+x240+8*x336==1311351)
add_eq(x80+x72*10*x112+8*x352-3*x104-x56*90*x208-6*x216+11*x8+6*x216+2*x192+x216-x232-8*x264-x264+6*x8-13*x88==-563008)
add_eq(-7*x192+-11*x216+-11*x72+x96+x304*70*x240-10*x232-2*x320-6*x224-x344*8*x48+10*x200-2*x96-x24*x344*((x320<<8)-32*x320)==-267345737)
add_eq(11*x248+13*x144+x144*84*x208-12*x56+14*x336+6*x184-x160*x264*1260*x192-x352*98*x136+x328*270*x344*x264+10*x64==-701812476)
add_eq(x344+x216+3*x232+-9*x160+4*x120-x200-x328+15*x96-6*x104+4*x72-x32*24*x224+130*x32*x328+14*x24+8*x0-x0==584152)
add_eq(x184+5*x328+9*x24+x8*15*x328+5*x176-15*x200-x248*24*x176-4*x96-x128*36*x352-10*x32+9*x64-45*x272*x8==-923909)
add_eq(-5*x184+15*x208+8*x200+15*x184-x8*90*x48-6*x256-4*x64-13*x256+x208-x112*70*x184-4*x72-8*x152-x96*78*x264==-1952483)
add_eq(15*x280+-13*x112+-7*x328+-7*x304+9*x24+x312*x72*360*x128+6*x192-x240+135*x16*x128-9*x72+4*x240-x184*112*x80==118806054)
add_eq(3*x248+6*x152-x56*130*x288+12*x320-x96*42*x248+4*x16+10*x0+x80*99*x224-x272*40*x192-8*x40+x96+7*x0==-1038889)
add_eq(-11*x344+x160*20*x352+x280*60*x40-x320*x24*1008*x8+8*x352-10*x224-7*x280-2*x216-4*x136-x136-8*x208-x144-8*x72==-1324642844)
add_eq(9*x40+x64+x0+10*x24-x104*84*x16+x216*16*x224+12*x224+2*x88-14*x320-12*x256+15*x80-4*x184-x184-3*x88-5*x40==-914171)
add_eq(x352*55*x120+x136*48*x288+2*(x152+6*x16)-x112*14*x304+11*x16-12*x48*x112+8*x88-x88+x184*13*x144-10*x32+3*x168==986086)
add_eq(-3*x136+9*x192+4*x296+9*x272-4*x272+8*x120+x56*40*x336+10*x120-x88*x216*360*x128+12*x40-15*x80*x128+13*x8==-62537013)
add_eq(-3*x104+-13*x304+15*x208+11*x104+x184*110*x64+2*(-3*x200+5*x216)+x296*x72*550*x272-4*x56-x56-x248*135*x296+12*x88-9*x64==498719083)
add_eq(11*x48+x200+7*(x256+x208)+x288*180*x264+x280*99*x72-12*x336-x176*32*x216+10*x120+15*x64+8*x32-10*x264+14*x64==910067)
add_eq(9*x176+-7*x216+8*x8+4*(3*x72-3*x248)-6*x80+2*x304+8*x328-x328-4*x104-x104-2*x64-x80*60*x128+x8*60*x304-x224*7*x8==447630)
add_eq(9*x320+11*x144+3*x168+-13*x8+x248+x240-4*x232+8*x32-x32-x288*210*x232-14*x296-6*x352*x168-2*x312+8*x232+4*x280==-1562727)
add_eq(13*x160+7*x16-14*x336-4*x192+8*x296+x152*78*x288-63*x192*x336-x144-2*x160-4*x248+4*x120+10*x304+7*x160-4*x208==-471203)
add_eq(-7*x152+7*x112+13*x48+x336+x184*4*x136-2*x320-13*x136+9*x112+14*x8-x40*39*x104+6*x256+4*x232-x296+14*x192==-262868)
add_eq(11*x72+x8*56*x16-4*x48-x48-x160*77*x112-12*x272-11*x304-8*x40-15*x208+x88*x328*72*x232-x144*x280*528*x256==-716423735)
add_eq(15*x40+x264*130*x320+x32+2*x80-x280*132*x128+x112*75*x184-2*x192-6*x256-2*x208+4*x320-11*x120+4*x152-8*x40==856586)
add_eq(13*x264+x160+4*(x48-x160)+8*x352-x352-x104*90*x288+6*x160-4*x296-x296+x88*x256*20*x56-4*x72-x72+2*x232-10*x0+x184*156*x88==5981100)
add_eq(9*x24+-5*x272+6*x352-11*x168-14*x32-8*x40+x312*1344*x32*x168+5*x320+15*x8-x216*15*x208-10*x104+11*x128+8*x136-x136==1411741755)
add_eq(3*x328+5*x48+8*x80+10*x64-x328*28*x72-10*x240+10*x168+10*x152-x192+5*x64-10*x176-3*x184+4*x256+9*x240+11*x224==-117294)
add_eq(13*x56+-7*x104+9*x216+-2*x280+12*x272-3*x112+63*x352*x216-7*x160+x296*70*x336-x256*156*x152-2*x96-12*x80==656269)
add_eq(9*x344+15*x232+x8*120*x352+12*x104+12*x120+14*x256+10*x200+13*x296-4*x176-x176+8*x208-x208-4*x288-x288-x104+7*x104-x320*36*x304==1256993)
add_eq(5*x248+-15*x312+x152*90*x144+x216*16*x128-x352*x328*70*x224+2*x64+x336*35*x304+10*x56+2*x96+8*x232+4*x160==-53357640)
add_eq(15*x0+13*x104+-13*x24+3*x120+3*x272+6*x312-x256*60*x304+15*x264+x48*60*x256-4*x240-x240-8*x288-x288-x88+8*x280+7*x0==-119712)
add_eq(-11*x48+13*x232+13*x224+x232+-7*x160+5*x128+15*x80+4*x328+2*x136-15*x144-10*x240-6*x192+13*x0-48*x344*x144-2*x56==-586617)
add_eq(11*x144-8*x176+4*x136-9*x232+8*x112-8*x8-12*x304+2*x208-11*x112+6*x24+x312*3*x280-10*x128+22*x168*x232+14*x336==302239)
add_eq(9*x0+9*x8+x48*156*x192-4*x256-x256+2*x312+15*x72+10*x192-4*x152+8*x160+4*x160-8*x184-x184+13*x320-7*x232-3*x288-12*x0==1457854)
add_eq(13*x8+-3*x200+x224*150*x216+-13*x344+x304*12*x0-4*x232-x80-2*x336+4*x208-8*x264-10*x96+x312*18*x192+13*x160==1675940)
add_eq(13*x40+13*x288+7*x72-15*x240-12*x344+11*x320-12*x144+12*x96-11*x144-x32*104*x0-x160*132*x8-8*x48+8*x152-x152+5*x112==-2582478)

set_known_bytes('VolgaCTF{*}', step=8, type='ff')

i = 0
start_time = time.time()
while s.check() == sat:
prepare_founded_values(step=8)
print prepare_key(step=8)
iterate_all(step=8)
i += 1
print('--- %.2f second(s) && %d answer(s) ---' % ((time.time() - start_time), i) )
```

```
PS C:\!CTF> python YSNP_solver.py
VolgaCTF{D1$guis3_y0ur_code_and_y0u_@re_s@fe}
--- 1.33 second(s) && 1 answer(s) ---
```

flag is: VolgaCTF{D1$guis3_y0ur_code_and_y0u_@re_s@fe}