kani: add --concrete-playback when running tests

bchalios · bchalios · commit 98b3278c1372 · 2024-09-30T16:02:02.000+03:00
So that we can get a backtrace when failures happen.

Signed-off-by: Babis Chalios &lt;bchalios@amazon.es&gt;
diff --git a/tests/integration_tests/test_kani.py b/tests/integration_tests/test_kani.py
@@ -33,7 +33,7 @@ def test_kani(results_dir):
     # --output-format terse is required by -j
     # --enable-unstable is needed to enable `-Z` flags
     _, stdout, _ = utils.check_output(
-        "cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse",
+        "cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse -Zconcrete-playback --concrete-playback=print",
         timeout=2400,
     )
 

Original file line number	Diff line number	Diff line change
`@@ -33,7 +33,7 @@ def test_kani(results_dir):`
`33`	`33`	`# --output-format terse is required by -j`
`34`	`34`	# --enable-unstable is needed to enable `-Z` flags
`35`	`35`	`_, stdout, _ = utils.check_output(`
`36`		`- "cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse",`
	`36`	`+ "cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse -Zconcrete-playback --concrete-playback=print",`
`37`	`37`	`timeout=2400,`
`38`	`38`	`)`
`39`	`39`