# Random Maze
This challenge can be solved with z3 after we gather all the constraints, let's look at the main function:
Before entering `traverse()`, each of our input index is taken out for a small check:

if ( (path[i] & 3) == 0 || path[i] == 3 * (path[i] / 3) || path[i] > 0x64 || path[i] <= 0x13 )
      oops();

We don't want `oops()` to be called, so our first constraint is:

s.add(Not(Or([(path[i] & 3) == 0, path[i] % 3 == 0, path[i] > 0x64, path[i] <= 0x13])))

Also it worth noting that each path is smaller than `0x64`, we will use this later.
Next, let's dive into the `traverse()` function:
There are a few things we want to add to our solver here:

First, the code `flag[i] ^= path[i];` updates the global variable `flag` with our input. We will do the same with our script.

for i in range(PATH_LEN):
    flag[i] = flag[i] ^ path[i]

And add constraints for the two if-else blocks to avoid `oops()`, the first one is:

if ( i )
{
    if ( flag[i] + flag[i - 1] != sums[i - 1] )
        oops();
    ...
}

Rewrite it for our solver so the if statement is not satisfied:

if(i > 0):
    s.add(flag[i] + flag[i-1] == sum[i-1])

For the second check:

else if ( !(unsigned __int8)check_prime(flag[0]) )
{
    oops();
}

That means the `flag[0]` should be a prime number to avoid `oops()`. Since we already know that each path has to be smaller than 0x64, here is our constraint.

s.add(Or([flag[0] == x for x in [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97]]))

## Full script

from z3 import *

flag = [BitVecVal(x, 8) for x in b"ON#X~o8&"]

sum = [BitVecVal(x, 8) for x in [0xCE, 0xA1, 0xAE, 0xAD, 0x64, 0x9F, 0xD5, 0]]

s = Solver()

PATH_LEN = 8
path = []
for i in range(PATH_LEN):
    path.append(BitVec(f'path[{i}]', 8))
    s.add(Not(Or([(path[i] & 3) == 0, path[i] % 3 == 0, path[i] > 0x64, path[i] <= 0x13])))

for i in range(PATH_LEN):
    flag[i] = flag[i] ^ path[i]
    if(i > 0):
        s.add(flag[i] + flag[i-1] == sum[i-1])

s.add(Or([flag[0] == x for x in [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97]]))

if s.check() == sat:
    print("Solution found!")
    m = s.model()
    print(''.join([hex(m[path[i]].as_long())[2:] for i in range(PATH_LEN)][::-1])) # 41565e4d2217232e

else:
    print("Can not find any solution!")

Try the output of the above script on the challenge and we can get the flag.

can you solve the maze? :3
choose ur path >> 41565e4d2217232e
running your path! hope this works:
uoftctf{am4z31ng}

## Flag

uoftctf{am4z31ng}