ATPs go quite a bit beyond what a SMT can do, however you're not stuck with just using ATPs when they are supported. You can still allow for proofs to be manual

ATPs go quite a bit beyond what a SMT 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 SARK 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.