I had a lot of contact with computer science students coming from the other side, meaning they used Z3 or other (SMT) solvers as blackboxes which they just use

I had a lot of contact with computer science students coming from the other side, meaning they used Z3 or other (SMT) solvers as blackboxes which they just use at a certain point in their algorithm without having thought what theories they are using (the T in SMT) and what's undecidable in general or in that theory. So I had quite a few "groundbreaking" approaches end in disappointment. It's important to know the capabilities and limits of your tools.