It looks like you might be following a similar workflow to my recently created Formal Equivalence example - is that so?
One suggestion (which is also included in the documentation above) is to try using the 'FindViolation' strategy first (as I did in the example).
Some simple code to demonstrate:
opts = sldvoptions;
opts.Mode = 'PropertyProving';
opts.ProvingStrategy = 'FindViolation';
opts.MaxViolationSteps = 99;
'FindViolation' (as opposed to 'Prove') often tends to take less time to run.
How large are the models being analyzed? How many objectives are being analyzed? (Is it just one Proof Objective?)
You can stop analysis and generate results for debugging, however you'd only be able to analyze results for completed objectives.
If you continue to run into long analysis times, I recommend reaching out to MathWorks Technical Support.
