Decompiled the binary with IDA:```cint print_flag(){  char s[264]; // [rsp+0h] [rbp-110h] BYREF  FILE *stream; // [rsp+108h] [rbp-8h]
  stream = fopen("flag.txt", "r");  if ( !stream )    return puts("Cannot read flag.txt.");  fgets(s, 256, stream);  s[strcspn(s, "\n")] = 0;  return puts(s);}int __cdecl main(int argc, const char **argv, const char **envp){  int v4; // [rsp+Ch] [rbp-114h] BYREF  char s[264]; // [rsp+10h] [rbp-110h] BYREF  char *i; // [rsp+118h] [rbp-8h]
  puts("Welcome to Finals Simulator 2023: Math Edition!");  printf("Question #1: What is sin(x)/n? ");  fflush(stdout);  fgets(s, 256, stdin);  s[strcspn(s, "\n")] = 0;  if ( !strcmp(s, "six") )  {    printf("Question #2: What's the prettiest number? ");    fflush(stdout);    __isoc99_scanf("%d", &v4;;    if ( 42 * (v4 + 88) == 561599850 )    {      printf("Question #3: What's the integral of 1/cabin dcabin? ");      fflush(stdout);      getchar();      fgets(s, 256, stdin);      s[strcspn(s, "\n")] = 0;      for ( i = s; *i; ++i )        *i = 17 * *i % mod;      putchar(10);      if ( !strcmp(s, &enc) )      {        puts("Wow! A 100%! You must be really good at math! Here, have a flag as a reward.");        print_flag();      }      else      {        puts("Wrong! You failed.");      }      return 0;    }    else    {      puts("Wrong! You failed.");      return 0;    }  }  else  {    puts("Wrong! You failed.");    return 0;  }}```It seems the challenge consists of three parts, let's do them one by one. 
The first one is easy, the answer is just "six";
The second is also easy, just a basic linear equation. If you don't want to solve it by hand, use z3-solver and type:```pyimport z3v4 = z3.Int('v4')s = z3.Solver()s.add(42 * (v4 + 88) == 561599850)if s.check() == z3.sat:	v4 = s.model().eval(v4).as_long()	print(v4)```it will tell you the answer.
The third one is the main part of this challenge. First, export the value of `mod` and the data of `enc`(it's located at the .data section, with the address of 0x3080 and ends with a zero byte `0x00`). You can use hex editors like `010editor` or command `dd` to do this. Then use z3-solver again to solve the equations:```pyenc = bytearray.fromhex("""0E C9 9D B8 26 83 26 41 74 E9 26 A5 83 94 0E 63 37 37 37""")n = len(enc)mod = 0xFDimport z3flag = [z3.Int(f'flag_{i}') for i in range(n)]s = z3.Solver()s.add([17*flag[i]%mod==enc[i] for i in range(n)])if s.check() == z3.sat:	flag = bytes([s.model().eval(flag[i]).as_long() for i in range(n)]).decode()	print(flag)else:	print('unsat')```finally, send the answers to remote server by `nc` and getflag:```six13371337it's a log cabin!!!
# lactf{im_n0t_qu1t3_sur3_th4ts_h0w_m4th_w0rks_bu7_0k}```