Skip to content

Fix timeouts and failure generation#705

Merged
marcoeilers merged 6 commits into
masterfrom
meilers_check_timeout_and_failure_gen
Apr 14, 2023
Merged

Fix timeouts and failure generation#705
marcoeilers merged 6 commits into
masterfrom
meilers_check_timeout_and_failure_gen

Conversation

@marcoeilers

@marcoeilers marcoeilers commented Apr 14, 2023

Copy link
Copy Markdown
Contributor

This PR makes three changes:

  • It modifies checkSmoke to have an option to use the assert timeout (by default, none) instead of the check timeout.
  • It modifies smoke checks whose failure would lead to a verification error to use the assert timeout instead (since we don't want verification failures due to timeouts unless the assert timeout is set).
  • It moves the code that generates the error message in QP consumes until after the crucial assert, which is important to get the correct counterexample.

@jcp19 jcp19 left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@marcoeilers marcoeilers merged commit 4c9e733 into master Apr 14, 2023
@marcoeilers marcoeilers deleted the meilers_check_timeout_and_failure_gen branch April 14, 2023 13:46
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.

2 participants