ATPs go quite a bit beyond what a SMT solver can do, however you're not stuck with just using ATPs when they are supported. You can still allow for proofs to be manually written with an ATP doesn't work, and in fact SPARK allows for this with Rocq.

Most of what I have to prove is floating-point code where a manual proof is too much of a headache to ever attempt though.