In main function we have something like

```
void main(int argc, const char **argv)
{
int num, flag_len;
char *str1, *str2;
char flg[18];

menu();
if ( argc > 1 )
{
flag_len = strlen(argv[1]);
str1 = &g_DEAEBAAC;
str2 = &g_8C2A6EAE;
num = 4919;
calculate(&g_DEAEBAAC, &g_8C2A6EAE, &num);
if ( 6 * num / 6 != flag_len ) // in the debugger you can see that the required length = 18
{
puts("Wrong pass :(");
exit(0);
}
strcpy(flg, argv[1]);
func_one(flg[0], flg[1]);
func_two(flg[1], flg[2]);
func_three(flg[2], flg[3], flg[4]);
func_four(flg[5], flg[6], flg[7]);
func_five(flg[8], flg[9], flg[11]);
func_six(flg[10], flg[12], flg[13]);
func_sev(flg[14], flg[15], flg[16]);
func_final(flg[16], flg[17]);
puts("Daaaaaaamn , that was ez , validate the task with that input ;) ");
}
else
{
puts("Usage : ./prog PASS");
}
}
```

In func_NUM we have equations which we can solve with z3.

So let's write a script!

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

var_num = 18
create_vars(var_num, size = 17) # create 18 BitVecs(x0...x17) with 17 bits size
solver()
init_vars(globals())
set_ranges(var_num) # set ASCII ranges for x0...x17

# add_eq( x0 > 29 ) # we have flagFormat - {x0...x4, x17}, so we can skip it
# add_eq( x1 <= 120 )
# add_eq( pw == z3_pow((x1 ^ x0), 4919.0) )
# add_eq( fmd == x1 * fmod(pw, 500.0) )
# add_eq( z3_pow(fmd, 2.0) - (282000 * x0 * x1 + 4900000) == 10663648 )
# add_eq( x4 * (x3 ^ x2) - x2 == 641 )
# add_eq( x2 * x2 / x4 + x3 == 179 )
add_eq( x5 + (x7 ^ x6) % 4 == 113 )
add_eq( x6 * x7 / x5 == 117 )
add_eq( x7 > 49 )
add_eq( (2 * x9 ^ x8 * x11) == 8983 )
add_eq( x11 * x8 - (x9 ^ x8 * x11) == 116 )
add_eq( ((311 - x12) ^ x10 * x13) == 9819 )
add_eq( x12 + 3 * x10 - 2 * x13 * x10 == -19332 )
add_eq( 202 * (x16 * x14 + x15) - x15 * (x14 ^ x16) == 1998612 )
add_eq( ((x16 + x17) * x16 * x17 ^ 0x1337) - (x16 - (x17 ^ x16) + x16) == 2816180 )

set_known_bytes('Flag{*}', var_num) # set flagFormat

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

but due collisions -_- we have
```
Flag{qss_that_bad}
Flag{nqrath_t_bad}
Flag{ntoath_t_bad}
Flag{nunath_t_bad}
Flag{npsath_t_bad}
Flag{ppuath_t_bad}
Flag{ppu_that_bad}
Flag{pqt_that_bad}
Flag{qqu_that_bad}
Flag{pqtath_t_bad}
Flag{qquath_t_bad}
Flag{notath_t_bad}
Flag{not_that_bad}
Flag{nqr_that_bad}
Flag{oqsath_t_bad}
Flag{nto_that_bad}
Flag{prsath_t_bad}
Flag{prs_that_bad}
Flag{psrath_t_bad}
Flag{psr_that_bad}
Flag{qssath_t_bad}
Flag{oqs_that_bad}
Flag{nspath_t_bad}
Flag{nsp_that_bad}
Flag{osqath_t_bad}
Flag{osq_that_bad}
Flag{pupath_t_bad}
Flag{pup_that_bad}
Flag{quqath_t_bad}
Flag{quq_that_bad}
Flag{ptqath_t_bad}
Flag{ptq_that_bad}
Flag{nps_that_bad}
Flag{nrqath_t_bad}
Flag{nrq_that_bad}
Flag{nnuath_t_bad}
Flag{nnu_that_bad}
Flag{oouath_t_bad}
Flag{oou_that_bad}
Flag{nun_that_bad}
Flag{ouo_that_bad}
Flag{ouoath_t_bad}
--- 0.63 seconds && 42 answer(s) ---
```

Rigth flag is: Flag{not_that_bad}