Make CSE more useful by reusing the previous proof

[Stevengre]

Currently, the proof will re-run all the things when using --reinit and unchange if there is a proof. Therefore, the CSE won't bring a lot of improvement for the tests which just call a function once.

My idea is to provide incremental verification: If only the tests changes, don't re-generate the summary for the external callee functions. Intead, use the summary directly. I think this will significantly enhance the verification experience, especially in scenarios where only the tests will be modified during the audit.