Fix resource limit & timeout handling if some assertion in the batch has already failed

[samuelpilz]

This PR addresses the root cause of dafny-lang/dafny#5805. In short, this issue arises when boogie runs into a timeout or resource limit while trying to verify subsequent assertions in an assertion batch where one assertion already failed.

In that case, the record VerificationRunResult has set the SolverOutcome to Invalid and contains the counterexamples that were found before running into a timeout. The method VerificationRunResult.ComputePerAssertOutcomes then assigns Valid to all assertions for which no counterexamples have been found because of the timeout, giving issue dafny-lang/dafny#5805.

From the standpoint of the method ComputePerAssertOutcomes two scenarios are indistinguishable:

• One or more assertions are found invalid and the rest have been verified
• One or more assertions are found invalid and the the verification of the rest has hit a timeout

This PR suggests to fix this by reporting the timeout alongside the found counterexamples.

This change is expected to have some effects for programs built on boogie: I assume that the VerificationRunResult only had a nonempty list of CounterExamples when the SolverOutcome is Invalid. I expect that programs built on boogie would need to adapt to this new possibility and report the verification failure errors accordingly.

[keyboardDrummer]

Sorry for the slow response. Can you add a test for the new behavior?

[shazqadeer]

@samuelpilz : If you are still interested in landing this PR, I would like to provide feedback. I am less concerned about a test case and more concerned about the specification of the value being returned by the method you are changing. If you do not wish to pursue this PR further, I would like to close it.