I have an assignment to solve this equation in z3:
????^???? ≡ 16779582829584320111 mod 2⁶⁴,
x>=2 and y>=2 are both integers

I tried using both ints and bitvectors, it can never find a solution. I know that z3 isn’t used for non-linear tasks, so I know there has to be some sort of a trick, but I can’t figure it out