From c15122e3ef298875c4623165099ceee3338792d4 Mon Sep 17 00:00:00 2001 From: Patrick Roy Date: Fri, 6 Jun 2025 10:16:21 +0100 Subject: [PATCH 1/2] test: use kani built-in --harness-timeout option Set a per-harness timeout of 30 minutes. This should hopefully make it easier to debug scenarios where proofs end up hanging indefinitely, as we now no longer hit the pytest timeout, but instead a timeout built into kani (which should tell us what exact harness timed out). Signed-off-by: Patrick Roy --- tests/integration_tests/test_kani.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/integration_tests/test_kani.py b/tests/integration_tests/test_kani.py index 9b087a5375f..9660dde75fc 100644 --- a/tests/integration_tests/test_kani.py +++ b/tests/integration_tests/test_kani.py @@ -34,7 +34,7 @@ def test_kani(results_dir): # --output-format terse is required by -j # -Z unstable-options is needed to enable the other `-Z` flags _, stdout, _ = utils.check_output( - "cargo kani -Z unstable-options -Z stubbing -Z function-contracts -Z restrict-vtable -j --output-format terse", + "cargo kani -Z unstable-options -Z stubbing -Z function-contracts -Z restrict-vtable -j --output-format terse --harness-timeout 40m", timeout=TIMEOUT, ) From db365d1eaf6d8b13ea27301b0080d264fcfbd3df Mon Sep 17 00:00:00 2001 From: Patrick Roy Date: Fri, 6 Jun 2025 10:21:09 +0100 Subject: [PATCH 2/2] ci: run kani tests if test_kani.py is changed Just so that we run the test when we change only the test itself. Signed-off-by: Patrick Roy --- .buildkite/pipeline_pr.py | 1 + 1 file changed, 1 insertion(+) diff --git a/.buildkite/pipeline_pr.py b/.buildkite/pipeline_pr.py index 07f7e603d39..8744a0dcb6a 100755 --- a/.buildkite/pipeline_pr.py +++ b/.buildkite/pipeline_pr.py @@ -53,6 +53,7 @@ not changed_files or any(x.suffix in [".rs", ".toml", ".lock"] for x in changed_files) or any(x.parent.name == "devctr" for x in changed_files) + or any(x.name == "test_kani.py" for x in changed_files) ): kani_grp = pipeline.build_group( "🔍 Kani",