# Comprehensive 2 65 points >Reversing - Solved (66 solves)
>Written by boomo
>His power level increased... What do I do now??
>[comprehensive2.py](comprehensive2.py)
>Output: [1, 18, 21, 18, 73, 20, 65, 8, 8, 4, 24, 24, 9, 18, 29, 21, 3, 21, 14, 6, 18, 83, 2, 26, 86, 83, 5, 20, 27, 28, 85, 67, 5, 17, 2, 7, 12, 11, 17, 0, 2, 20, 12, 26, 26, 30, 15, 44, 15, 31, 0, 12, 46, 8, 28, 23, 0, 11, 3, 25, 14, 0, 65]
It got a Python script and the program output
Lets analyze the script:```py# m is unknown stringm = '[?????]'# n also unknown stringn = '[?????]'# a is all lowercase alphaberta = 'abcdefghijklmnopqrstuvwxyz'# p is all punctuation characterp = ' !"#$%&\'()*+,-./:;<=>?@[\\]^_`{|}~'# the length of m must equal 63assert len(m) == 63 # m only contain characters from a and passert set(m).issubset(set(a + p))# the length of n must equal 7assert len(n) == 7 # n only contain characters from aassert set(n).issubset(set(a))# m only contain one "tjctf{" stringassert m.count('tjctf{') == 1 # m only contain one "}" stringassert m.count('}') == 1 # m contain 5 space characterassert m.count(' ') == 5```
Under all these condition, `m` and `n` will scramble with some calculation then become output:```py# The logic is same as the original codetext = []for k in range(0, 63, 21):	for j in range (0, 21, 3):		for i in range(j + k, j + k + 3):			text.append(m[i] ^ n[j // 3] ^ n[i - j - k] ^ n[k // 21])print(text)# [1, 18, ..., 65]```
Seems like a **z3 problem (SAT solver)**
z3 is normally used for Reversing Challenge to calculate the possible input based on the calculation and output 
## Condition of m- m is length of 63- m contains lowercase letter or punctuation- m contain the flag format (tjctf{}) - m contain 5 spaces (" ")
## Condition of n- n is length of 7- n contains only lowercase letter
We can guess the m and n will be something like:```pym = 'the flag is here!  tjctf{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa}'n = 'abcdefg'```
Based on the condition above, we can use z3 to calculate the possible input:```pyfrom z3 import *# Declare m and n as BitVectorm = [BitVec("a%i"%i,8) for i in range(63)]n = [BitVec("n%i"%i,8) for i in range(7)]output = [1, 18, ..., 65]
a = 'abcdefghijklmnopqrstuvwxyz'p = ' !"#$%&\'()*+,-./:;<=>?@[\\]^_`{|}~'s = Solver()# Add condition that m is in a and p onlyfor i in range(63):	condition = "Or("	for c in (a+p):		condition += "m[%i]==%i," %(i,ord(c)) 	s.add(eval(condition[:-1]+")"))
# Add condition that n is in a onlyfor i in range(7):	condition = "Or("	for c in (a):		condition += "n[%i]==%i," %(i,ord(c)) 	s.add(eval(condition[:-1]+")"))
# Add condition that m contain 5 spacess.add(z3.Sum([ z3.If(bv == ord(' '), 1, 0) for bv in m ]) == 5)
# Add condition that m contain the flag format tjctf{}# In range(63-5) because tjctf{ must be togethers.add(z3.Sum([ z3.If(And(m[i] == ord('t'),m[i+1] == ord('j'),m[i+2] == ord('c'),m[i+3] == ord('t'),m[i+4] == ord('f')), 1, 0) for i in range(63-5)]) == 1)# Add condition that m contain one }s.add(z3.Sum([ z3.If(bv == ord('}'), 1, 0) for bv in m ]) == 1)```After we add the conditions, we can add the calculation for produce the output:```pyindex = 0for k in range(0, len(m), 21):	for j in range (0, 21, 3):		for i in range(j + k, j + k + 3):			# Add condition that this calculation must equal the output			s.add((m[i] ^ n[j // 3] ^ n[i - j - k] ^ n[k // 21]) == output[index])			index += 1```Then finally, check is it solvable, print out the flag!```pyif s.check() == sat:	modl = s.model()	m_result = ""	for i in range(63):		m_result += chr(modl[m[i]].as_long())	print(m_result)```Result:```hata o sagashiteimasu ka? dozo, tjctf{sumimasen_flag_kudasaii}.```
[Full python script](solve.py)
My z3 script is refer from a [DawgCTF2020 challenge writeup](https://github.com/toomanybananas/dawgctf-2020-writeups/tree/master/reversing/potentially-eazzzy)
## Flag```tjctf{sumimasen_flag_kudasaii}```