TLDR: p & q are chosen such that `p = 2 * q + 1`. `phi` is given, but `n` is unknown. Use Z3 to solve for `q`, calculate `p` and eventually `n`, and decrypt `ct`.

https://meashiri.github.io/ctf-writeups/posts/202306-nahamcon/#rsa-outro

Original writeup (https://meashiri.github.io/ctf-writeups/posts/202306-nahamcon/#rsa-outro).