Concrete playback prints characters for interpreted values in ARM64 Linux

[adpaco-aws]

I tried this code:

Applies to all the tests listed in this comment. For example, tests/ui/concrete-playback/u8/main.rs:

#[kani::proof]
pub fn harness() {
    let u8_1: u8 = kani::any();
    let u8_2: u8 = kani::any();
    let u8_3: u8 = kani::any();
    assert!(!(u8_1 == u8::MIN && u8_2 == 101 && u8_3 == u8::MAX));
}

using the following command line invocation: kani --enable-unstable --concrete-playback=print
with Kani version: 0.34

I expected to see this happen: Concrete playback generates the test

#[test]
fn kani_concrete_playback_harness_6199617291819462955() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 0
        vec![0],
        // 101
        vec![101],
        // 255
        vec![255]
    ];
    kani::concrete_playback_run(concrete_vals, harness);
}

Instead, this happened: In ARM64 Linux, concrete playback generates the test

#[test]
fn kani_concrete_playback_harness_6199617291819462955() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 0
        vec![0],
        // 'e'
        vec![101],
        // 255
        vec![255],
    ];
    kani::concrete_playback_run(concrete_vals, harness);
}

Note that the interpreted value for the byte with value 101 is 'e'. @tautschnig notes in this comment that this comes from CBMC.