VERIFICATION:- FAILED

Concrete playback
```
#[test]
fn kani_concrete_playback_harness
    let concrete_vals: Vec<Vec<u8>> = vec![
        // -inf
        vec![0, 0, 0, 0, 0, 0, 240, 255],
        // -1.797693e+308
        vec![255, 255, 255, 255, 255, 255, 239, 255],
        // -101
        vec![0, 0, 0, 0, 0, 64, 89, 192],
        // -0
        vec![0, 0, 0, 0, 0, 0, 0, 128],
        // 2.225074e-308
        vec![0, 0, 0, 0, 0, 0, 16, 0],
        // 101
        vec![0, 0, 0, 0, 0, 64, 89, 64],
        // 1.797693e+308
        vec![255, 255, 255, 255, 255, 255, 239, 127],
        // +inf
        vec![0, 0, 0, 0, 0, 0, 240, 127]
    ];
    kani::concrete_playback_run(concrete_vals, harness);
}
```