// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Check that regular arithmetic operations in unsafe blocks still trigger overflow checks.
// kani-verify-fail

#[kani::proof]
pub fn check_sub(a: u8, b: u8) {
    unsafe {
        a - b;
    }
}