Tracking issue for UX improvements to the concrete playback feature

[sanjit-bhat]

If you have any feedback for the UX of the concrete playback feature, please comment it below. Getting feedback and iterating on it will help us stabilize the feature in the future.

[camshaft]

For the bolero integration, it would be really helpful to pass kani a directory to write the failure outputs into. Something like --concrete-out-dir path/to/dir. On failure, kani would write a the byte representation to a file with the name as the hash of the contents. The nice thing about this is the bytes should map to the same representation used for libfuzzer, which means we can actually replay these failure files using the existing bolero corpus replay feature. We'd also get input shrinking for free as well.

[celinval]

We should remove this extra setup step: https://model-checking.github.io/kani/debugging-verification-failures.html#setup