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 = 18create_vars(var_num, size = 17) # create 18 BitVecs(x0...x17) with 17 bits sizesolver()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 = 0start_time = time.time()while s.check() == sat:  prepare_founded_values(var_num)  print prepare_key(var_num)  iterate_all(var_num)  i += 1print('--- %.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}