Enable concrete playback without requiring extra setup

[celinval]

Requested feature: Concrete playback requires an extra setup which should be automated by the extension
Use case: Running concrete playback should work as long as Kani works
Link to relevant documentation (Rust reference, Nomicon, RFC):

This will probably be fairly easy if we implement model-checking/kani#2440.