I'm no expert. my understanding though is that one of the reasons for contracts is solvers cannot possibly handle all the possible states of a program. if you can throw a contract in places they can break your whole program into subsets. That is, when analyzing a function and everything it calls, it just assumes the contract holds. And if everything works correctly according to contract and doesn't crash, well, they know that function is satisfied. Then they don't need to go back and say, well, everything calling that previous function only needs to meet the contracts, they don't need to prove everything that function calls is correct. This they can only do a subset of the full program analysis prove the whole program.