Dafny and similar languages use SMT; their semantics need to be such that you're giving enough information for your proof to verify in sufficient time, otherwise you'll be waiting for a very long time or your proof is basically undecidable.

I'm not sure about benchmarks comparing languages, but Dafny goes through a lot of tweaking to make the process faster.