Skip to content

Delete Generator/discriminant test#2334

Merged
karkhaz merged 1 commit intomodel-checking:mainfrom
karkhaz:kk-turn-off-discriminant
Apr 3, 2023
Merged

Delete Generator/discriminant test#2334
karkhaz merged 1 commit intomodel-checking:mainfrom
karkhaz:kk-turn-off-discriminant

Conversation

@karkhaz
Copy link
Contributor

@karkhaz karkhaz commented Apr 3, 2023

This test is flaky in CI; removing until we can diagnose and fix the failure.

Description of changes:

Describe Kani's current behavior and how your code changes that behavior. If there are no issues this PR is resolving, explain why this change is necessary.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

This test is flaky in CI; removing until we can diagnose and fix the
failure.
@karkhaz karkhaz marked this pull request as ready for review April 3, 2023 19:21
@karkhaz karkhaz requested a review from a team as a code owner April 3, 2023 19:21
qinheping
qinheping previously approved these changes Apr 3, 2023
@qinheping
Copy link
Contributor

Can we instead make it a fixme test and create an issue to remind us to fix it later? https://model-checking.github.io/kani/regression-testing.html#fixme-tests

@qinheping qinheping dismissed their stale review April 3, 2023 19:30

Haven't read the slack message before approval

@karkhaz
Copy link
Contributor Author

karkhaz commented Apr 3, 2023

I'm not sure if fixme would work here because the test is flaky. It sometimes appears to memout in CI, but otherwise works. So we can't add an expected result I think...

@zhassan-aws
Copy link
Contributor

I agree adding fixme won't work because the test sometimes passes, so the kani-fixme suite may fail.

But, as @qinheping pointed out, can we at least file an issue to track re-enabling this test?

@karkhaz
Copy link
Contributor Author

karkhaz commented Apr 3, 2023

Yes, opened #2337

@karkhaz karkhaz merged commit fea4641 into model-checking:main Apr 3, 2023
@karkhaz karkhaz deleted the kk-turn-off-discriminant branch April 3, 2023 19:57
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.

3 participants