# Smart Solver solved without SMT and Z3Well the heading is intentional since I did not know about SMT and Z3 when I solved this problem during the CTF, and solved it logically. So read this if you are interested in a logical solution to the problem.
# Overview
The binary that we are provided uses a lot of instructions to compare each character of a string with all other characters of the string, if any of the test fails it just jumps to a location that exits. So we have to find that string which passes all tests. 
# Observations- The string length is `73`- The operations compare the numeric value of characters with each other so it defines a lexographic order for a character with all other characters of the string.
# Idea
Given a string with 73 characters `s[73]`, Consider a `73 X 73` 2-d array `a[73][73]`. Define `a[i][j]` in the following manner -:```if(s[i] == s[j]):	a[i][j] = -1elif(s[i] < s[j]):	a[i][j] = 0else:	a[i][j] = 1```
Now note that we can obtain the entire 2-d array `a` from the binary if we are able to parse the instructions in the disassembled code of the binary. This is because each character is compared with a number of other characters using either the `jbe` or `jae` instruction and if it is not compared with some character then it is safe to assume that both of them are equal, since no other possibility exists.
## Code to parse the binary and get the 2-d array
### Some debugging aids which can be safely ignoredThe code includes some `try-except` and `assert` statements to verify that what we are doing is right. The variable `ct` is the error counter. The code throws one error at an instruction before the comparisons are even started so `ct` is not allowed to be greater than 1. 
```import reimport jsonimport sysa=[[-1 for i in range(73)] for i in range(73)]
def dump_data():    # Objective a[i][j] = 0 if s[i] < s[j] , 1 if(s[i] > s[j]), -1 if (s[i] == s[j])     regex = '.*movzx  e([ad])x,BYTE PTR \[rbp-(0x[0-9a-f]*)\].*'	# regex to match src and dest    jmp_reg = '.*j([ab])e.*'	# regex to match operator (less or greater)     src,dst=-1,-1    ct=0    with open("disassembly",'r') as f:        for line in f.readlines():            # print(line)            try:                reg, pos = re.match(regex, line).groups()                pos = int(pos, 16) - 0xd8
                if(reg == 'd'):                    assert src == -1                    src = pos                    print("Setting src to ",pos)                elif(reg == 'a'):                    assert dst == -1                    dst = pos                    print("Setting dst to ", pos)              except Exception as e:                 if isinstance(e, AssertionError):                    ct += 1                    print(src, dst)                    print(line)                    if(ct>1):                        sys.exit(-1)                try:                    oper = re.match(jmp_reg, line).groups()[0]                    assert src != -1 and dst != -1 and a[src][dst] == -1                    if oper == 'b':                        print("oper is b")                        a[src][dst] = 0                    else:                        print("Oper is a")                        a[src][dst] = 1                    src, dst = -1, -1                except Exception as e:                    if isinstance(e,AssertionError):                        ct += 1                        print(src, dst)                        print(line)                        if(ct > 1):                            sys.exit(-1)      open("out", 'w').write(json.dumps(a))```
# Reversing the 2-d array to obtain flagSo now we have `a[73][73]`. How to obtain the string `s[73]` from this 2-d array. So the idea is this, we can first group indices that map to the same character i.e indexes `x` and `y` belong to the same group if `s[x][y] == -1 == s[y][x]`.
**Note:** We do not need to ensure the second condition since that is a problem constraint and it cannot fail otherwise the data would be wrong. So what I mean is that for data to be correct the following invariant needs to be satisfied```s[i][j] = ~s[j][i] if (s[i][j] != -1) else s[i][j] == -1 == s[j][i]```
- Once we have grouped the characters we know that characters at indices in the same group are same. - Also note that suppose for an index `i` we can compute `less_ct[i] = count({j: s[i][j] == 0})`, `gt_ct[i] = count({j: s[i][j] == 1})` and `eq_ct[i] = count({j: a[i][j] == 0})` . `less_ct[i]` is a count of the number of characters which are lexographically **larger** than `s[i]`.-  Now suppose character indices `i1, i2, i3` belong to a group `G` i.e they map to same character. So they will have the same values of these quantities since the character comparison will yield equivalent results. So the variables `less_ct, gt_ct` are indeed a characterstic of the group and not of a particular index.-  Now suppose a group is mapped to the character `'b'`. How will its `less_ct` compare to the group that maps to the character `'c'`? It is obvious that the number of characters that are lexographically larger than `'c'` are less than the number of characters that are lexographically larger than `'b'` since the latter set will also include the characters that are equal to `'c'`.-   So it is convincing enough that if we sort these groups on the basis of `less_ct` and start assigning them the characters from `'a'` we could complete the entire string.
**Note:** We have made an assumption that all characters from `'a'` to `'z'` are being used. And this assumption only holds true if the number of groups that we are able to form are >= 26. In our case we got 28 groups i.e. all 26 alpahabets and `'{'` and `'}'`
## Code to obtain string from 2-d array
**Note:** It seemed like that we need to reverse the flag after obtaining the entire string to have the format `flag{...}````def rev():    data=json.loads(open('out','r').read())    ingroup = [False for i in range(73)]
    groups=[]
    for i in range(73):        if(ingroup[i]):            continue        ele = data[i]        eq_ct,less_ct,gt_ct=0,0,0        same_indexes = []        for j in range(73):            b=ele[j]            if b==-1:                eq_ct+=1                same_indexes.append(j)                ingroup[j] = True            elif (b==0):                less_ct+=1            else:                gt_ct+=1        groups.append({"eq_ct":eq_ct,"less_ct":less_ct,"gt_ct":gt_ct,"same_indexes":same_indexes})    groups.sort(key=lambda x: x['less_ct'])    flag=['' for i in range(73)]    for i in range(len(groups)):        c = chr(ord('a')+i) if(i!=len(groups)-1) else '}'        group = groups[i]        for index in group['same_indexes']:            flag[index] = c    flag="".join(flag)[::-1]    print(flag)```
# Result`flag{thequickbrownfoxjumpedoverthelazydogandlearnedhowtoautomateanalysis}`