Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

samuelpilz
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant