```             ███                   █████
░░░                   ░░███
████████   ████   █████   ██████  ░███████    ██████   █████ ████
░░███░░███ ░░███  ███░░   ███░░███ ░███░░███  ░░░░░███ ░░███ ░███
░███ ░███  ░███ ░░█████ ░███ ░░░  ░███ ░███   ███████  ░███ ░███
░███ ░███  ░███  ░░░░███░███  ███ ░███ ░███  ███░░███  ░███ ░███
████ █████ █████ ██████ ░░██████  ████ █████░░████████ ░░███████
░░░░ ░░░░░ ░░░░░ ░░░░░░   ░░░░░░  ░░░░ ░░░░░  ░░░░░░░░   ░░░░░███
███ ░███
░░██████
░░░░░░
```

Intro

Well, I screwed up. I was only able to solve only one rev chall, their warmup. I guess it’s normal for a n00b like me, though.

The Large Cherries

We’re given a file called Lao-Tzu.

There’s a ptrace at the very top, so if you bypass it, you will see that:

It asks for two kinds of inputs, and for the first time, it asks for 9 characters and 10 characters the second time.

The first input is sent to this function, called `magic_word`.

The function essentially makes sure that certain conditions are met for input[0] to input[7], even though the input asks for 9 characters. This is our key to solving this chall.

``````from z3 import Solver, Xor, BitVec

a = [BitVec('a%s' % i,64 ) for i in range(9)]

s = Solver()
s.check()
m = s.model()
print(s.model())
b= []
for i in range(8):
b.append(chr(int(m[a[i]].as_string())))
c = ''.join(b)
print(c)
``````

Now, this piece of code gives out `t0m7r00z`, which is only 8 characters. This will be important later.

The second piece of input is a 10 character input, that checks if all of the characters add up to `0x294`, i.e. `660`. That happens to be the sum of digital sum of `t0m7r00z`.

Therefore, we need to add something extra to the mix. This character can be quite literally anything, and I just typed `t0m7r00za` as both inputs.

Flag: `Poseidon{Its_L3_t3Mp5_DeS_C3r1s35}`