#![feature(rustc_private)]
#[macro_use]
mod common;
use common::*;

test_verify_one_bv_file! {
    #[test] test1 verus_code! {
        proof fn test1(b: u32) {
            assert(b & 7 == b % 8) by(bit_vector);
            assert(b & 7 == b % 8);

            assert(b ^ b == 0) by(bit_vector);
            assert(b ^ b == 0);

            assert(b & b == b) by(bit_vector);
            assert(b & b == b);

            assert(add(add(b, !b), 1) == 0) by(bit_vector);
            assert(add(add(b, !b), 1) == 0);

            assert(b | b == b) by(bit_vector);
            assert(b | b == b);

            assert(b & 0xff < 0x100) by(bit_vector);
            assert(b & 0xff < 0x100);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test2 verus_code! {
        proof fn test2(b: u32) {
            assert(b << 2 == mul(b, 4)) by(bit_vector);
            assert(b << 2 == mul(b, 4));
            assert(b < 256 ==> b << 2 == b * 4);

            assert(b >> 1 == b / 2) by(bit_vector);
            assert(b >> 1 == b / 2);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test3 verus_code! {
        proof fn test3(b: u32) {
            assert(sub(mul(2, b), b) == b) by(bit_vector);
            assert(sub(mul(2, b), b) == b);

            assert(b <= b) by(bit_vector);
            assert(b >= b) by(bit_vector);

            assert(b & b & b == b | b | (b ^ b)) by(bit_vector);
            assert(b & b & b == b | b | (b ^ b));
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test4 verus_code! {
        proof fn test4(u1: u32, u2:u32) {
            assert( (u1 as u64) << 32u64 | (u2 as u64)  == add(mul(u1 as u64, 0x100000000), u2 as u64))
                by(bit_vector);
            assert( (u1 as u64) << (32 as u64) | (u2 as u64)  == add(mul(u1 as u64, 0x100000000), u2 as u64));
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test5 verus_code! {
        proof fn test5(u:u64) {
            assert( (u >> 32) as u32  ==  (u / 0x100000000) as u32)
                by(bit_vector);
            assert( (u >> 32) as u32  ==  (u / 0x100000000) as u32);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test6 verus_code! {
        proof fn test6(a:u64, b:u64, c:u64) {
            assert((a ^ b == a ^ c) ==> (b == c)) by(bit_vector);
            assert((a ^ b == a ^ c) ==> (b == c));
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test7 verus_code! {
        proof fn test7(b1:u64, b2:u64, b3:u64) {
            assert( !b1 != !b2 ==> !(b1 == b2)) by(bit_vector);
            assert(((b1 == 1u64) && (b2 == b3)) ==> (add(b1, b2) == add(b3, 1))) by(bit_vector);
            assert((b1 == b2) ==> (!b1 == !b2)) by(bit_vector);
            assert( b1 == (!(!b1))) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test8 verus_code! {
        proof fn test8(b: u32) {
            assert(forall|a: u32, b: u32| #[trigger] (a & b) == b & a) by(bit_vector);
            assert(b & 0xff < 0x100) by(bit_vector);
            assert(0xff & b < 0x100);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test9 verus_code! {
        proof fn test9(x: u32, y:u32) {
            let max:u32 = 0xffff_ffff;
            assert(x >> 1 >= 0);
            assert(x & y <= max);
            assert(x | y >= 0);
            assert(x << y <= max);
            assert((!x) <= max);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test1_fails verus_code! {
        proof fn test1(b: u32) {
            assert(b | b > b) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test2_fails verus_code! {
        proof fn test2(b: u32) {
            assert(add(b, 1) == b) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test3_fails verus_code! {
        proof fn test3(b: u32) {
            assert(b & 0 > 0) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test4_fails verus_code! {
        proof fn test4(b: u32) {
            assert( (b << 2) >> 2 == b) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test5_fails verus_code! {
        proof fn test5(b: u32) {
            assert((b << 1) == mul(b, 2)) by(bit_vector);
            assert((b << 1) == mul(b, 4)); // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test6_fails verus_code! {
        proof fn test6(b: u32) {
            assert(b << 2 == mul(b, 4)) by(bit_vector);
            assert(b << 2 == b * 4);  // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test6_fails2 verus_code! {
        proof fn test6(b: u32) {
            assert(b << 2 == b * 4) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test7_fails verus_code! {
        proof fn test7(b: u32) {
            assert(!0u32 == 0xffffffffu32) by(bit_vector);
            assert(!0u64 == 0xffffffff_ffffffffu64) by(bit_vector);
            assert(false); // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] test8_ok verus_code! {
        proof fn test8(b: i32) {
            assert(b <= b) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    //https://github.com/verus-lang/verus/issues/191 (@matthias-brun)
    #[test] test10_fails verus_code! {
        #[verifier(bit_vector)]
        proof fn f2() { // FAILS
            ensures(forall |i: u64| (1u64 << i) > 0); // Although this line should be reported instead of the above line, since Z3 does not return model which we utilize for error reporting, just use the above line
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_bv_file! {
    #[test] usize_in_by_bit_vector verus_code! {
        proof fn test_usize(x: usize) {
            assert(x & x == x) by (bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] const_usize_in_by_bit_vector verus_code! {
        proof fn test_usize() {
            assert(1usize == 1usize) by (bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] not_supported_int_in_by_bit_vector verus_code! {
        proof fn test_int(x: int, y: int) {
            assert(x == y) by (bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "expected finite-width integer")
}

test_verify_one_bv_file! {
    #[test] not_supported_datatype_in_by_bit_vector verus_code! {
        struct X { }
        proof fn test_int(x: X, y: X) {
            assert(x == y) by (bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "`bit_vector` prover cannot handle type `test_crate::X`")
}

test_verify_one_bv_file! {
    #[test] const_int_in_by_bit_vector verus_code! {
        proof fn test_int() {
            assert(0int == 0int) by (bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] strslice_len_not_supported_in_by_bit_vector verus_code! {
        proof fn test() {
            use verus_builtin::*;
            assert(strslice_len::<u64>(7u64) == 0int) by(bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "string slice length not supported in `bit_vector` assert")
}

test_verify_one_bv_file! {
    #[test] float_to_bits_not_supported_in_by_bit_vector verus_code! {
        proof fn test() {
            use verus_builtin::*;
            assert(f32_to_bits(0.0f32) == 0u32) by(bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "float-to-bits coercion not supported in `bit_vector` assert")
}

test_verify_one_bv_file! {
    #[test] real_to_int_not_supported_in_by_bit_vector verus_code! {
        proof fn test() {
            assert(1.0real.floor() == 1int) by(bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "real-to-int coercion not supported in `bit_vector` assert")
}

test_verify_one_bv_file! {
    #[test] usize_cast_in_by_bit_vector verus_code! {
        proof fn test_usize(x: u64) {
            assert((x as usize) == (x as usize)) by (bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] bit_vector_with_usize_valid_expr verus_code! {
        spec fn stuff(x: usize, y: usize, z: usize) -> usize {
            (x | y) & !z
        }

        proof fn test_usize(x: usize, y: usize, z: usize) {
            // We can only prove trivial things without by(bit_vector)
            // but these should at least be well-formed expressions.
            assert(((x & y) | !z) == ((x & y) | !z));
        }

        proof fn test_usize2(x: usize, y: usize, z: usize) {
            // This should fail (it is wrong)
            assert(stuff(x, y, z) == stuff(y, z, x)); // FAILS
        }

        proof fn test_usize3(x: usize) {
            // This should fail (if usize is 32-bit, then these expressions are different)
            assert((!x) as u64 == (!(x as u64))); // FAILS
        }

        proof fn test_usize4(x: usize) {
            // This should fail (if usize is 64-bit, this is wrong)
            assert((x >> 32) == 0usize); // FAILS
        }

        proof fn test_usize5(x: usize) {
            // This should fail (if usize is 32-bit, this is wrong)
            assert(((1usize << 35) >> 34) == 2usize); // FAILS
        }
    } => Err(err) => assert_fails(err, 4)
}

test_verify_one_bv_file_with_options! {
    #[test] bit_vector_usize_as_32bit ["vstd"] => verus_code! {
        global size_of usize == 4;

        proof fn test1(x: usize) {
            assert(x & x == x) by(bit_vector);
        }

        proof fn test2(y: usize) {
            // This should only work for 32-bit usize
            assert((y >> 32) == 0usize) by(bit_vector);
        }

        proof fn test3(x: usize) {
            assert((!x) as u64 == (!(x as u64))); // FAILS
        }

        proof fn test4(x: usize) {
            assert((!x) as u64 == (!(x as u64))) by(bit_vector); // FAILS
        }

        proof fn test5(x: usize) {
            assert((x >> 32) == 0usize) by(bit_vector);
        }

        proof fn test6(x: usize) {
            assert(((1usize << 35) >> 34) == 2usize); // FAILS
        }

        proof fn test7(x: usize) {
            assert(((1usize << 35) >> 34) == 2usize) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 4)
}

test_verify_one_bv_file_with_options! {
    #[test] bit_vector_usize_as_64bit ["vstd"] => verus_code! {
        global size_of usize == 8;

        proof fn test1(x: usize) {
            assert(x & x == x) by(bit_vector);
        }

        proof fn test2(y: usize) {
            assert((y >> 32) == 0usize); // FAILS
        }

        proof fn test3(y: usize) {
            assert((y >> 32) == 0usize) by(bit_vector); // FAILS
        }

        proof fn test4(x: usize) {
            assert((!x) as u64 == (!(x as u64))) by(bit_vector);
        }

        proof fn test5(x: usize) {
            assert((x >> 32) == 0usize); // FAILS
        }

        proof fn test6(x: usize) {
            assert((x >> 32) == 0usize) by(bit_vector); // FAILS
        }

        proof fn test7(x: usize) {
            assert(((1usize << 35) >> 34) == 2usize) by(bit_vector);
        }
    } => Err(err) => assert_fails(err, 4)
}

test_verify_one_bv_file! {
    #[test] test_casting_to_higher_width_issue386 verus_code! {
        proof fn test() {
            let b: u8 = 20;
            let w: u64 = 20;

            // In order to augment b to a u64, it has to add 64 - 8 = 56 bits.
            // 56 isn't a power of 2
            // Thus, this test makes sure that bitwidths of non-powers-of-2 work.

            assert((b as u64) == w) by (bit_vector)
                requires b == 20 && w == 20 { }
        }

        proof fn test2() {
            let b: u8 = 20;
            let w: u64 = 276;

            assert((b as u64) == w) by (bit_vector) // FAILS
                requires b == 20 && w == 276 { }
        }
    } => Err(err) => assert_fails(err, 1)
}

test_verify_one_bv_file! {
    #[test] test_bool_variable_issue369 verus_code! {
        proof fn test() {
            let b: bool = true;
            assert(b ==> (0 | 1u8 == 1) == b) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_issue415 verus_code! {
        #[verifier(bit_vector)]
        proof fn lemma_shift_right_u64_upper_bound(val: u64, amt: u64, upper_bound: u64)
        requires
            amt < 64u64,
            val <= upper_bound,
        ensures
            (val >> amt) <= (upper_bound >> amt)
        {}
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] bitvector_in_decreases_by verus_code! {
        spec fn stuff(n: u64) -> int
            decreases n
              via stuff_dec
        {
            if n == 0 {
                0
            } else {
                stuff(n >> 1) + 1
            }
        }

        #[verifier::decreases_by]
        proof fn stuff_dec(n: u64) {
            assert((n > 0) ==> (n >> 1) < n) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] bitvector_ineq_different_bitwidth verus_code! {
        proof fn test() {
            let b: u8 = 5;

            assert(b >= 3u64) by(bit_vector)
                requires b == 5;
        }

        proof fn test2() {
            let b: u8 = 5;

            assert(3u64 <= b) by(bit_vector)
                requires b == 5;
        }

        proof fn test3() {
            let b: u8 = 5;

            assert(b <= 3u64) by(bit_vector) // FAILS
                requires b == 5;
        }
    } => Err(err) => assert_fails(err, 1)
}

test_verify_one_bv_file! {
    #[test] test_extreme_cases_arithmetic1 verus_code! {
        fn test_arith_4_4() {
            assert(((-1i32) ^ (7i32)) + ((-1i32) ^ (7i32)) == -16) by(bit_vector);
            assert(((-1i32) ^ (7i32)) - ((-1i32) ^ (7i32)) == 0) by(bit_vector);
            assert(((-1i32) ^ (7i32)) * ((-1i32) ^ (7i32)) == 64) by(bit_vector);
            assert(((-1i32) ^ (7i32)) + !(-8i32) == -1) by(bit_vector);
            assert(((-1i32) ^ (7i32)) - !(-8i32) == -15) by(bit_vector);
            assert(((-1i32) ^ (7i32)) * !(-8i32) == -56) by(bit_vector);
            assert(!(-8i32) + ((-1i32) ^ (7i32)) == -1) by(bit_vector);
            assert(!(-8i32) - ((-1i32) ^ (7i32)) == 15) by(bit_vector);
            assert(!(-8i32) * ((-1i32) ^ (7i32)) == -56) by(bit_vector);
            assert(!(-8i32) + !(-8i32) == 14) by(bit_vector);
            assert(!(-8i32) - !(-8i32) == 0) by(bit_vector);
            assert(!(-8i32) * !(-8i32) == 49) by(bit_vector);
            assert(((-1i32) ^ (7i32)) + 15 == 7) by(bit_vector);
            assert(((-1i32) ^ (7i32)) - 15 == -23) by(bit_vector);
            assert(((-1i32) ^ (7i32)) * 15 == -120) by(bit_vector);
            assert(!(-8i32) + 15 == 22) by(bit_vector);
            assert(!(-8i32) - 15 == -8) by(bit_vector);
            assert(!(-8i32) * 15 == 105) by(bit_vector);
            assert(15 + ((-1i32) ^ (7i32)) == 7) by(bit_vector);
            assert(15 - ((-1i32) ^ (7i32)) == 23) by(bit_vector);
            assert(15 * ((-1i32) ^ (7i32)) == -120) by(bit_vector);
            assert(15 + !(-8i32) == 22) by(bit_vector);
            assert(15 - !(-8i32) == 8) by(bit_vector);
            assert(15 * !(-8i32) == 105) by(bit_vector);
            assert(0 + 0 == 0) by(bit_vector);
            assert(0 - 0 == 0) by(bit_vector);
            assert(0 * 0 == 0) by(bit_vector);
            assert(15 + 15 == 30) by(bit_vector);
            assert(15 - 15 == 0) by(bit_vector);
            assert(15 * 15 == 225) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_extreme_cases_arithmetic2 verus_code! {
        fn test_arith_8_8() {
            assert(((-1i32) ^ (127i32)) + ((-1i32) ^ (127i32)) == -256) by(bit_vector);
            assert(((-1i32) ^ (127i32)) - ((-1i32) ^ (127i32)) == 0) by(bit_vector);
            assert(((-1i32) ^ (127i32)) * ((-1i32) ^ (127i32)) == 16384) by(bit_vector);
            assert(((-1i32) ^ (127i32)) + !(-128i32) == -1) by(bit_vector);
            assert(((-1i32) ^ (127i32)) - !(-128i32) == -255) by(bit_vector);
            assert(((-1i32) ^ (127i32)) * !(-128i32) == -16256) by(bit_vector);
            assert(!(-128i32) + ((-1i32) ^ (127i32)) == -1) by(bit_vector);
            assert(!(-128i32) - ((-1i32) ^ (127i32)) == 255) by(bit_vector);
            assert(!(-128i32) * ((-1i32) ^ (127i32)) == -16256) by(bit_vector);
            assert(!(-128i32) + !(-128i32) == 254) by(bit_vector);
            assert(!(-128i32) - !(-128i32) == 0) by(bit_vector);
            assert(!(-128i32) * !(-128i32) == 16129) by(bit_vector);
            assert(((-1i32) ^ (127i32)) + 255 == 127) by(bit_vector);
            assert(((-1i32) ^ (127i32)) - 255 == -383) by(bit_vector);
            assert(((-1i32) ^ (127i32)) * 255 == -32640) by(bit_vector);
            assert(!(-128i32) + 255 == 382) by(bit_vector);
            assert(!(-128i32) - 255 == -128) by(bit_vector);
            assert(!(-128i32) * 255 == 32385) by(bit_vector);
            assert(255 + ((-1i32) ^ (127i32)) == 127) by(bit_vector);
            assert(255 - ((-1i32) ^ (127i32)) == 383) by(bit_vector);
            assert(255 * ((-1i32) ^ (127i32)) == -32640) by(bit_vector);
            assert(255 + !(-128i32) == 382) by(bit_vector);
            assert(255 - !(-128i32) == 128) by(bit_vector);
            assert(255 * !(-128i32) == 32385) by(bit_vector);
            assert(255 + 255 == 510) by(bit_vector);
            assert(255 - 255 == 0) by(bit_vector);
            assert(255 * 255 == 65025) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_extreme_cases_arithmetic3 verus_code! {
        fn test_arith_8_16() {
            assert(((-1i32) ^ (127i32)) + ((-1i32) ^ (32767i32)) == -32896) by(bit_vector);
            assert(((-1i32) ^ (127i32)) - ((-1i32) ^ (32767i32)) == 32640) by(bit_vector);
            assert(((-1i32) ^ (127i32)) * ((-1i32) ^ (32767i32)) == 4194304) by(bit_vector);
            assert(((-1i32) ^ (127i32)) + !(-32768i32) == 32639) by(bit_vector);
            assert(((-1i32) ^ (127i32)) - !(-32768i32) == -32895) by(bit_vector);
            assert(((-1i32) ^ (127i32)) * !(-32768i32) == -4194176) by(bit_vector);
            assert(!(-128i32) + ((-1i32) ^ (32767i32)) == -32641) by(bit_vector);
            assert(!(-128i32) - ((-1i32) ^ (32767i32)) == 32895) by(bit_vector);
            assert(!(-128i32) * ((-1i32) ^ (32767i32)) == -4161536) by(bit_vector);
            assert(!(-128i32) + !(-32768i32) == 32894) by(bit_vector);
            assert(!(-128i32) - !(-32768i32) == -32640) by(bit_vector);
            assert(!(-128i32) * !(-32768i32) == 4161409) by(bit_vector);
            assert(((-1i32) ^ (127i32)) + 65535 == 65407) by(bit_vector);
            assert(((-1i32) ^ (127i32)) - 65535 == -65663) by(bit_vector);
            assert(((-1i32) ^ (127i32)) * 65535 == -8388480) by(bit_vector);
            assert(!(-128i32) + 65535 == 65662) by(bit_vector);
            assert(!(-128i32) - 65535 == -65408) by(bit_vector);
            assert(!(-128i32) * 65535 == 8322945) by(bit_vector);
            assert(255 + ((-1i32) ^ (32767i32)) == -32513) by(bit_vector);
            assert(255 - ((-1i32) ^ (32767i32)) == 33023) by(bit_vector);
            assert(255 * ((-1i32) ^ (32767i32)) == -8355840) by(bit_vector);
            assert(255 + !(-32768i32) == 33022) by(bit_vector);
            assert(255 - !(-32768i32) == -32512) by(bit_vector);
            assert(255 * !(-32768i32) == 8355585) by(bit_vector);
            assert(255 + 65535 == 65790) by(bit_vector);
            assert(255 - 65535 == -65280) by(bit_vector);
            assert(255 * 65535 == 16711425) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_extreme_cases_arithmetic4 verus_code! {
        fn test_arith_16_8() {
            assert(((-1i32) ^ (32767i32)) + ((-1i32) ^ (127i32)) == -32896) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) - ((-1i32) ^ (127i32)) == -32640) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) * ((-1i32) ^ (127i32)) == 4194304) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) + !(-128i32) == -32641) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) - !(-128i32) == -32895) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) * !(-128i32) == -4161536) by(bit_vector);
            assert(!(-32768i32) + ((-1i32) ^ (127i32)) == 32639) by(bit_vector);
            assert(!(-32768i32) - ((-1i32) ^ (127i32)) == 32895) by(bit_vector);
            assert(!(-32768i32) * ((-1i32) ^ (127i32)) == -4194176) by(bit_vector);
            assert(!(-32768i32) + !(-128i32) == 32894) by(bit_vector);
            assert(!(-32768i32) - !(-128i32) == 32640) by(bit_vector);
            assert(!(-32768i32) * !(-128i32) == 4161409) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) + 255 == -32513) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) - 255 == -33023) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) * 255 == -8355840) by(bit_vector);
            assert(!(-32768i32) + 255 == 33022) by(bit_vector);
            assert(!(-32768i32) - 255 == 32512) by(bit_vector);
            assert(!(-32768i32) * 255 == 8355585) by(bit_vector);
            assert(65535 + ((-1i32) ^ (127i32)) == 65407) by(bit_vector);
            assert(65535 - ((-1i32) ^ (127i32)) == 65663) by(bit_vector);
            assert(65535 * ((-1i32) ^ (127i32)) == -8388480) by(bit_vector);
            assert(65535 + !(-128i32) == 65662) by(bit_vector);
            assert(65535 - !(-128i32) == 65408) by(bit_vector);
            assert(65535 * !(-128i32) == 8322945) by(bit_vector);
            assert(65535 + 255 == 65790) by(bit_vector);
            assert(65535 - 255 == 65280) by(bit_vector);
            assert(65535 * 255 == 16711425) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_extreme_cases_arithmetic5 verus_code! {
        fn test_arith_15_16() {
            assert(((-1i32) ^ (16383i32)) + ((-1i32) ^ (32767i32)) == -49152) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) - ((-1i32) ^ (32767i32)) == 16384) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) * ((-1i32) ^ (32767i32)) == 536870912) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) + !(-32768i32) == 16383) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) - !(-32768i32) == -49151) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) * !(-32768i32) == -536854528) by(bit_vector);
            assert(!(-16384i32) + ((-1i32) ^ (32767i32)) == -16385) by(bit_vector);
            assert(!(-16384i32) - ((-1i32) ^ (32767i32)) == 49151) by(bit_vector);
            assert(!(-16384i32) * ((-1i32) ^ (32767i32)) == -536838144) by(bit_vector);
            assert(!(-16384i32) + !(-32768i32) == 49150) by(bit_vector);
            assert(!(-16384i32) - !(-32768i32) == -16384) by(bit_vector);
            assert(!(-16384i32) * !(-32768i32) == 536821761) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) + 65535 == 49151) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) - 65535 == -81919) by(bit_vector);
            assert(((-1i32) ^ (16383i32)) * 65535 == -1073725440) by(bit_vector);
            assert(!(-16384i32) + 65535 == 81918) by(bit_vector);
            assert(!(-16384i32) - 65535 == -49152) by(bit_vector);
            assert(!(-16384i32) * 65535 == 1073659905) by(bit_vector);
            assert(32767 + ((-1i32) ^ (32767i32)) == -1) by(bit_vector);
            assert(32767 - ((-1i32) ^ (32767i32)) == 65535) by(bit_vector);
            assert(32767 * ((-1i32) ^ (32767i32)) == -1073709056) by(bit_vector);
            assert(32767 + !(-32768i32) == 65534) by(bit_vector);
            assert(32767 - !(-32768i32) == 0) by(bit_vector);
            assert(32767 * !(-32768i32) == 1073676289) by(bit_vector);
            assert(0 + 65535 == 65535) by(bit_vector);
            assert(0 - 65535 == -65535) by(bit_vector);
            assert(0 * 65535 == 0) by(bit_vector);
            assert(32767 + 65535 == 98302) by(bit_vector);
            assert(32767 - 65535 == -32768) by(bit_vector);
            assert(32767 * 65535 == 2147385345) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_extreme_cases_arithmetic6 verus_code! {
        fn test_arith_16_15() {
            assert(((-1i32) ^ (32767i32)) + ((-1i32) ^ (16383i32)) == -49152) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) - ((-1i32) ^ (16383i32)) == -16384) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) * ((-1i32) ^ (16383i32)) == 536870912) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) + !(-16384i32) == -16385) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) - !(-16384i32) == -49151) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) * !(-16384i32) == -536838144) by(bit_vector);
            assert(!(-32768i32) + ((-1i32) ^ (16383i32)) == 16383) by(bit_vector);
            assert(!(-32768i32) - ((-1i32) ^ (16383i32)) == 49151) by(bit_vector);
            assert(!(-32768i32) * ((-1i32) ^ (16383i32)) == -536854528) by(bit_vector);
            assert(!(-32768i32) + !(-16384i32) == 49150) by(bit_vector);
            assert(!(-32768i32) - !(-16384i32) == 16384) by(bit_vector);
            assert(!(-32768i32) * !(-16384i32) == 536821761) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) + 0 == -32768) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) - 0 == -32768) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) * 0 == 0) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) + 32767 == -1) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) - 32767 == -65535) by(bit_vector);
            assert(((-1i32) ^ (32767i32)) * 32767 == -1073709056) by(bit_vector);
            assert(!(-32768i32) + 32767 == 65534) by(bit_vector);
            assert(!(-32768i32) - 32767 == 0) by(bit_vector);
            assert(!(-32768i32) * 32767 == 1073676289) by(bit_vector);
            assert(65535 + ((-1i32) ^ (16383i32)) == 49151) by(bit_vector);
            assert(65535 - ((-1i32) ^ (16383i32)) == 81919) by(bit_vector);
            assert(65535 * ((-1i32) ^ (16383i32)) == -1073725440) by(bit_vector);
            assert(65535 + !(-16384i32) == 81918) by(bit_vector);
            assert(65535 - !(-16384i32) == 49152) by(bit_vector);
            assert(65535 * !(-16384i32) == 1073659905) by(bit_vector);
            assert(65535 + 32767 == 98302) by(bit_vector);
            assert(65535 - 32767 == 32768) by(bit_vector);
            assert(65535 * 32767 == 2147385345) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_double_arch_ok verus_code! {
        proof fn test_works_both(a: usize, b: usize, c: u32) {
            assert(
                (usize::BITS == 64 ==> (((c as usize) << 32) >> 32 == c))
                && (usize::BITS == 32 ==> (a as u32) == (b as u32) ==> a == b)) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_double_arch_fail32 verus_code! {
        proof fn test(c: u32) {
            assert(((c as usize) << 32) >> 32 == c) by(bit_vector);
        }
    } => Err(err) => assert_fails_bv_32bit(err)
}

test_verify_one_bv_file! {
    #[test] test_double_arch_fail64 verus_code! {
        proof fn test(a: usize, b: usize) {
            assert((a as u32) == (b as u32) ==> a == b) by(bit_vector);
        }
    } => Err(err) => assert_fails_bv_64bit(err)
}

test_verify_one_bv_file! {
    #[test] test_double_arch_fail_both verus_code! {
        proof fn test_works_neither(a: usize, b: usize) {
            assert((a as u32) == (b as u32)) by(bit_vector);
        }
    } => Err(err) => assert_fails_bv_32bit_64bit(err)
}

test_verify_one_bv_file! {
    #[test] test_double_arch_fail64_req_ens verus_code! {
        proof fn test_only_32_2(a: usize) by(bit_vector)
            requires (a as u32) != a
            ensures false
        { }
    } => Err(err) => assert_fails_bv_64bit(err)
}

test_verify_one_bv_file! {
    #[test] test_shl_signed_unsupported verus_code! {
        fn test_shl_neg(x: i32, y: i32) {
            assert(x << y == x) by(bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "Verus does not currently support bit-shift with possibly negative shift")
}

test_verify_one_bv_file! {
    #[test] test_shr_signed_unsupported verus_code! {
        fn test_shl_neg(x: i32, y: i32) {
            assert(x >> y == x) by(bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "Verus does not currently support bit-shift with possibly negative shift")
}

test_verify_one_bv_file! {
    #[test] test_eq_ineq verus_code! {
        fn test_eq(x: u8, y: i8) {
            assert(x == y as u8 ==> y == x) by(bit_vector); // FAILS
        }

        fn test_ineq(x: u8, y: i8, z: u8) {
            assert(y == -5 ==> x >= y) by(bit_vector);
            assert(x >= (y as u8) ==> x >= y) by(bit_vector);
            assert(x >= (x as i8)) by(bit_vector);

            assert(x >= (z as i8) ==> x >= z) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 2)
}

test_verify_one_bv_file! {
    #[test] test_eq_ineq2 verus_code! {
        fn test_comparisons(a: u32, b: i32) {
            assert(a < b <==> (b & (-0x8000_0000i32) == 0) && (a < (b as u32))) by(bit_vector);
            assert(a < b ==> a < (b as u32)) by(bit_vector);
            assert(a < b <== a < (b as u32)) by(bit_vector); // FAILS
            assert(a < b <==> (a as i64) < b) by(bit_vector);

            assert(a > b <==> (b & (-0x8000_0000i32) != 0) || (a > (b as u32))) by(bit_vector);
            assert(a > b ==> a > (b as u32)) by(bit_vector); // FAILS
            assert(a > b <== a > (b as u32)) by(bit_vector);
            assert(a > b <==> (a as i64) > b) by(bit_vector);
        }

        fn test_comparisons_2(a: u32, b: i64) {
            assert(a < b <==> (b & (-0x8000_0000_0000_0000i64) == 0) && ((a as u64) < (b as u64))) by(bit_vector);
            assert(a < b ==> a < (b as u64)) by(bit_vector);
            assert(a < b <== a < (b as u64)) by(bit_vector); // FAILS
            assert(a < b <==> (a as i128) < b) by(bit_vector);

            assert(a > b <==> (b & (-0x8000_0000_0000_0000i64) != 0) || ((a as u64) > (b as u64))) by(bit_vector);
            assert(a > b ==> a > (b as u64)) by(bit_vector); // FAILS
            assert(a > b <== a > (b as u64)) by(bit_vector);
            assert(a > b <==> (a as i128) > b) by(bit_vector);
        }

        fn test_comparisons_3(a: u32, b: i16) {
            assert(a < b <==> (b & (-0x8000i16) == 0) && (a < (b as u16))) by(bit_vector);
            assert(a < b ==> a < (b as u16)) by(bit_vector);
            assert(a < b <== a < (b as u16)) by(bit_vector); // FAILS
            assert(a < b <==> (a as i64) < (b as i64)) by(bit_vector);

            assert(a > b <==> (b & (-0x8000i16) != 0) || (a > (b as u16))) by(bit_vector);
            assert(a > b ==> a > (b as u16)) by(bit_vector); // FAILS
            assert(a > b <== a > (b as u16)) by(bit_vector);
            assert(a > b <==> (a as i64) > b) by(bit_vector);
        }
    } => Err(err) => assert_fails(err, 6)
}

test_verify_one_bv_file! {
    #[test] test_clipping_and_casting verus_code! {
        fn test_clipping(a: u32, b: i32) {
            assert(a as u64 == a) by(bit_vector);
            assert(a as u16 == a) by(bit_vector); // FAILS
            assert(a as u16 == (a as i32) as u16) by(bit_vector);

            assert(b as i64 == b) by(bit_vector);
            assert(b as u64 == b) by(bit_vector); // FAILS
            assert(b as i16 == b) by(bit_vector); // FAILS
            assert(b as i16 == (b as u64) as i16) by(bit_vector);
        }


        fn test_casting(x: u16, y: i16) {
            assert(x as u32 == x) by(bit_vector);
            assert(y as i32 == y) by(bit_vector);
            assert(x as i64 == x) by(bit_vector);

            assert(x as i8 as u8 == x as u8) by(bit_vector);
            assert(y as u8 as i8 == y as i8) by(bit_vector);

            assert(y as u64 == y) by(bit_vector); // FAILS
            assert(x as u8 == x) by(bit_vector); // FAILS
            assert(y as i8 == y) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 6)
}

test_verify_one_bv_file! {
    #[test] test_or verus_code! {
        fn test_or(x: u16, y: u16, z: i16) {
            assert((x | y) == (x as i16 | y as i16) as u16) by(bit_vector);
            assert((x | y) == (x as i16 | y as i16)) by(bit_vector); // FAILS
            assert((x | 0x7777) & 0x8000 == x & 0x8000) by(bit_vector);
            assert((z | 0x7777) & (0x8000u16 as i16) == z & (0x8000u16 as i16)) by(bit_vector);

            assert((x as i32 | z as i32) == (x | z as u16)) by(bit_vector); // FAILS
            assert((x as i32 | z as i32) == (x as i16 | z)) by(bit_vector); // FAILS
            assert((x as i32 | z as i32) ==
                ((x | z as u16) as u32 | (if z < 0 { 0xffff0000u32 } else { 0 })) as i32) by(bit_vector);
        }
    } => Err(err) => assert_fails(err, 3)
}

test_verify_one_bv_file! {
    #[test] test_and verus_code! {
        fn test_and(x: u16, y: u16, z: i16) {
            assert((x & y) == (x as i16 & y as i16) as u16) by(bit_vector);
            assert((x & y) == (x as i16 & y as i16)) by(bit_vector); // FAILS
            assert((x & 0x7777) & 0x8000 == 0) by(bit_vector);
            assert((z & 0x7777) & (0x8000u16 as i16) == 0) by(bit_vector);

            assert((x as i32 & z as i32) == (x & z as u16)) by(bit_vector);
            assert((x as i32 & z as i32) == (x as i16 & z)) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 2)
}

test_verify_one_bv_file! {
    #[test] test_xor verus_code! {
        fn test_xor(x: u16, y: u16, z: i16) {
            assert((x ^ y) == (x as i16 ^ y as i16) as u16) by(bit_vector);
            assert((x ^ y) == (x as i16 ^ y as i16)) by(bit_vector); // FAILS
            assert((x ^ 0x7777) & 0x8000 == x & 0x8000) by(bit_vector);
            assert((z ^ 0x7777) & (0x8000u16 as i16) == z & (0x8000u16 as i16)) by(bit_vector);

            assert((x as i32 ^ z as i32) == (x ^ z as u16)) by(bit_vector); // FAILS
            assert((x as i32 ^ z as i32) == (x as i16 ^ z)) by(bit_vector); // FAILS
            assert((x as i32 ^ z as i32) ==
                ((x ^ z as u16) as u32 | (if z < 0 { 0xffff0000u32 } else { 0 })) as i32) by(bit_vector);
        }
    } => Err(err) => assert_fails(err, 3)
}

test_verify_one_bv_file! {
    #[test] test_shl verus_code! {
        fn test_shl(x: u32, y: u16) {
            assert(x == y ==> (x << 2) == (y << 2)) by(bit_vector); // FAILS
            assert((x << 32) == (y << 32)) by(bit_vector);

            assert((x << 2) as i32 == (x as i32) << 2) by(bit_vector);
            assert((x << 2) == (x as i32) << 2) by(bit_vector); // FAILS

            assert((x << 2) == x * 4) by(bit_vector); // FAILS
            assert(((x as u64) << 2) == x * 4) by(bit_vector);

            assert((y << 2) == y * 4) by(bit_vector); // FAILS
            assert(((y as u64) << 2) == y * 4) by(bit_vector);

            assert((y << 2) == ((y as u32) << 2) as u16) by(bit_vector);
            assert((y << 2) == ((y as i32) << 2) as u16) by(bit_vector);
        }
    } => Err(err) => assert_fails(err, 4)
}

test_verify_one_bv_file! {
    #[test] test_shl_signed verus_code! {
        fn test_shl_signed(x: i32, y: i16, z: i32) {
            assert(x & (0xff000000u32 as i32) == 0 ==> (x << 2) == x * 4) by(bit_vector);
            assert((x << 2) == (x * 4) as i32) by(bit_vector);

            assert(x == y ==> (x << 2) == (y << 2)) by(bit_vector); // FAILS
            assert((x << 32) == (y << 32)) by(bit_vector);

            assert((x << 2) as u32 == (x as u32) << 2) by(bit_vector);

            assert((x << 2) == (y << 2)) by(bit_vector); // FAILS
            assert((x << 2) == (x as u32) << 2) by(bit_vector); // FAILS
            assert((x << 2) == x * 4) by(bit_vector); // FAILS
            assert(((x as i64) << 2) == x * 4) by(bit_vector);

            assert((y << 2) == ((y as u32) << 2) as i16) by(bit_vector);
            assert((y << 2) == ((y as i32) << 2) as i16) by(bit_vector);
        }

        fn test_shl_shift_is_signed_but_still_nonnegative(x: i32, z: i32) {
            assert(z == 2 ==> x << (z as u32) == (x * 4) as i32) by(bit_vector);
            assert(z == 2 ==> x << z == (x * 4) as i32); // normal solver, not bit-vector
        }
    } => Err(err) => assert_fails(err, 4)
}

test_verify_one_bv_file! {
    #[test] test_shr verus_code! {
        fn test_shr(x: u32, y: u16) {
            assert(x == y ==> (x >> 2) == (y >> 2)) by(bit_vector);
            assert(x >> 32 == y >> 16) by(bit_vector);
            assert(x >> 16 == y >> 16) by(bit_vector); // FAILS

            assert((x >> 2) as i32 == (x as i32) >> 2) by(bit_vector); // FAILS
            assert((x >> 2) == (x as i32) >> 2) by(bit_vector); // FAILS

            assert((x >> 2) == x / 4) by(bit_vector);

            assert((y >> 2) == (y as u32) >> 2) by(bit_vector);
            assert((y >> 2) == (y as i32) >> 2) by(bit_vector);
        }
    } => Err(err) => assert_fails(err, 3)
}

test_verify_one_bv_file! {
    #[test] test_shr_signed verus_code! {
        fn test_shr_signed(x: i32, y: i16, z: i32) {
            assert(x & 0x3 == 0 ==> (x >> 2) * 4 == x) by(bit_vector);
            assert(x >> 2 == (if x > 0 { ((x as u64) / 4) as i64 } else { -(((-x) as u64 + 3) / 4) as i64 })) by(bit_vector);

            assert(x == y ==> (x >> 2) == (y >> 2)) by(bit_vector);
            assert(x >> 32 == y >> 16) by(bit_vector); // FAILS
            assert(y >> 16 == 0 || y >> 16 == -1) by(bit_vector);
            assert(x >> 16 == y >> 16) by(bit_vector); // FAILS

            assert((x >> 2) as u32 == (x as u32) >> 2) by(bit_vector); // FAILS
            assert((x >> 2) == (x as u32) >> 2) by(bit_vector); // FAILS

            assert((y >> 2) == (y as u32) >> 2) by(bit_vector); // FAILS
            assert((y >> 2) == (y as i32) >> 2) by(bit_vector);
        }

        fn test_shr_shift_is_signed_but_still_nonnegative(x: i32, z: i32) {
            assert(z == 2 ==> x & 0x3 == 0 ==> (x >> (z as u32)) * 4 == x) by(bit_vector);
            assert(z == 2 ==> x & 0x3 == 0 ==> (x >> z) * 4 == x);  // normal solver, not bit-vector
        }
    } => Err(err) => assert_fails(err, 5)
}

test_verify_one_bv_file! {
    #[test] div_signed_euclidean verus_code! {
        fn div_signed_euclidean() {
           assert(7i32 / 3i32 == 2i32) by(bit_vector);
           assert(7i32 / 3i32 == 2i32);

           assert(-7i32 / 3i32 == -3i32) by(bit_vector);
           assert(-7i32 / 3i32 == -3i32);

           assert(7i32 / -3i32 == -2i32) by(bit_vector);
           assert(7i32 / -3i32 == -2i32);

           assert(-7i32 / -3i32 == 3i32) by(bit_vector);
           assert(-7i32 / -3i32 == 3i32);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] div_signed_overflow verus_code! {
        fn div_signed_overflow() {
            assert(-128i8 / -1i8 == 128) by(bit_vector);
            assert(-128i8 / -1i8 == 128);

            assert(-32768i16 / -1i16 == 32768) by(bit_vector);
            assert(-32768i16 / -1i16 == 32768);

            assert(-2147483648i32 / -1i32 == 2147483648) by(bit_vector);
            assert(-2147483648i32 / -1i32 == 2147483648);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] div_mod_signed_properties verus_code! {
        fn div_mod_signed_properties(x: i8, y: i8) {
            assert(y != 0 ==> (x / y) * y + (x % y) == x) by(bit_vector);
            assert(y != 0 ==> (x % y) >= 0) by(bit_vector);
            assert(y > 0 ==> (x % y) < y) by(bit_vector);
            assert(y < 0 ==> (x % y) < -y) by(bit_vector);
            assert(x as int / (-1) == -x) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] div0_underspecified verus_code! {
        fn div_0_underspecified(x: u32, y: u32) {
            assert(0u32 / y == 0) by(bit_vector); // FAILS
            assert(y != 0 ==> 0u32 / y == 0) by(bit_vector);

            assert(y / y == 1) by(bit_vector); // FAILS
            assert(y != 0 ==> y / y == 1) by(bit_vector);

            assert(x == 0 && y == 0 ==> x/y == 0xffffffff) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 3)
}

test_verify_one_bv_file! {
    #[test] mod_signed_euclidean verus_code! {
        fn mod_signed_euclidean() {
           assert(7i32 % 3i32 == 1i32) by(bit_vector);
           assert(7i32 % 3i32 == 1i32);

           assert(-7i32 % 3i32 == 2i32) by(bit_vector);
           assert(-7i32 % 3i32 == 2i32);

           assert(7i32 % -3i32 == 1i32) by(bit_vector);
           assert(7i32 % -3i32 == 1i32);

           assert(-7i32 % -3i32 == 2i32) by(bit_vector);
           assert(-7i32 % -3i32 == 2i32);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] mod0_underspecified verus_code! {
        fn mod_0_underspecified(x: u32, y: u32) {
            assert(0u32 % y == 0) by(bit_vector); // FAILS
            assert(y != 0 ==> 0u32 % y == 0) by(bit_vector);

            assert(y % y == 0) by(bit_vector); // FAILS
            assert(y != 0 ==> y % y == 0) by(bit_vector);

            assert(x == 0 && y == 0 ==> x%y == 0) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 3)
}

test_verify_one_file_with_options! {
    #[test] mod0_div0_consistency_no_simplify ["no-bv-simplify"] => verus_code! {
        fn mod_0_div_0_consistency(x: u32, y: u32) {
            assert(x % y == x % y) by(bit_vector); // FAILS
            assert(x / y == x / y) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 2)
}

test_verify_one_file! {
    #[test] mod0_div0_consistency verus_code! {
        fn mod_0_div_0_consistency(x: u32, y: u32) {
            assert(x % y == x % y) by(bit_vector);
            assert(x / y == x / y) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] bitnot verus_code! {
        fn test_bitnot_unsigned(x: u32, y: u64) {
            assert(x == y ==> (!x) == (!y)) by(bit_vector); // FAILS
            assert(x == y ==> ((!x) as u64 ^ 0xffff_ffff_0000_0000) == (!y)) by(bit_vector);
            assert((!y) == 0xffff_ffff_ffff_ffff - y) by(bit_vector);
        }

        fn test_bitnot_signed(x: i32, y: i64) {
            assert(x == y ==> (!x) == (!y)) by(bit_vector);
            assert((!y) == (-1) - y) by(bit_vector);
            assert(!0xffffi32 == -0x10000) by(bit_vector);
        }

        fn test_bitnot_signed_unsigned(a: u32, b: i32) {
            assert(a == (b as u32) ==> !a == (!b) as u32) by(bit_vector);
            assert(a == (b as u32) ==> !a == (!b)) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 2)
}

test_verify_one_file! {
    // https://github.com/verus-lang/verus/issues/3081
    #[test] bitnot_signed_without_bit_vector verus_code! {
        proof fn in_a_local(x: i8) {
            let y: i8 = !x;
            assert(-128 <= y <= 127);
            assert(y == -x - 1);
        }

        fn exec_i64(x: i64) {
            let y = !x;
            assert(y == -x - 1);
        }
    } => Ok(())
}

// test_by_equating:
// test `x op y` for all combinations of
//    - (x, y) are (8 bits, 8 bits); (8 bits, 9 bits); (9 bits, 8 bits)
//    - all combinations signed/unsigned
//    - for a bunch of different ops
// by comparing the results to the same operation done on a higher number of bits
// to get a '9 bit' thing, we add two 8 bits things together (e.g., ai + ai2)

test_verify_one_bv_file! {
    #[test] test_by_equating_add verus_code! {
        fn test_add(au: u8, au2: u8, bu: u8, bu2: u8, ai: i8, ai2: i8, bi: i8, bi2: i8, x: i32, y: i32) {
            assert(ai == x && bi == y ==> (ai + bi) == (x + y)) by(bit_vector);
            assert(ai == x && bu == y ==> (ai + bu) == (x + y)) by(bit_vector);
            assert(au == x && bi == y ==> (au + bi) == (x + y)) by(bit_vector);
            assert(au == x && bu == y ==> (au + bu) == (x + y)) by(bit_vector);
            assert(ai == x && (bi + bi2) == y ==> (ai + (bi + bi2)) == (x + y)) by(bit_vector);
            assert(ai == x && (bu + bu2) == y ==> (ai + (bu + bu2)) == (x + y)) by(bit_vector);
            assert(au == x && (bi + bi2) == y ==> (au + (bi + bi2)) == (x + y)) by(bit_vector);
            assert(au == x && (bu + bu2) == y ==> (au + (bu + bu2)) == (x + y)) by(bit_vector);
            assert((ai + ai2) == x && bi == y ==> ((ai + ai2) + bi) == (x + y)) by(bit_vector);
            assert((ai + ai2) == x && bu == y ==> ((ai + ai2) + bu) == (x + y)) by(bit_vector);
            assert((au + au2) == x && bi == y ==> ((au + au2) + bi) == (x + y)) by(bit_vector);
            assert((au + au2) == x && bu == y ==> ((au + au2) + bu) == (x + y)) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_by_equating_sub verus_code! {
        fn test_sub(au: u8, au2: u8, bu: u8, bu2: u8, ai: i8, ai2: i8, bi: i8, bi2: i8, x: i32, y: i32) {
            assert(ai == x && bi == y ==> (ai - bi) == (x - y)) by(bit_vector);
            assert(ai == x && bu == y ==> (ai - bu) == (x - y)) by(bit_vector);
            assert(au == x && bi == y ==> (au - bi) == (x - y)) by(bit_vector);
            assert(au == x && bu == y ==> (au - bu) == (x - y)) by(bit_vector);
            assert(ai == x && (bi + bi2) == y ==> (ai - (bi + bi2)) == (x - y)) by(bit_vector);
            assert(ai == x && (bu + bu2) == y ==> (ai - (bu + bu2)) == (x - y)) by(bit_vector);
            assert(au == x && (bi + bi2) == y ==> (au - (bi + bi2)) == (x - y)) by(bit_vector);
            assert(au == x && (bu + bu2) == y ==> (au - (bu + bu2)) == (x - y)) by(bit_vector);
            assert((ai + ai2) == x && bi == y ==> ((ai + ai2) - bi) == (x - y)) by(bit_vector);
            assert((ai + ai2) == x && bu == y ==> ((ai + ai2) - bu) == (x - y)) by(bit_vector);
            assert((au + au2) == x && bi == y ==> ((au + au2) - bi) == (x - y)) by(bit_vector);
            assert((au + au2) == x && bu == y ==> ((au + au2) - bu) == (x - y)) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_by_equating_mul verus_code! {
        fn test_mul(au: u8, au2: u8, bu: u8, bu2: u8, ai: i8, ai2: i8, bi: i8, bi2: i8, x: i32, y: i32) {
            assert(ai == x && bi == y ==> (ai * bi) == (x * y)) by(bit_vector);
            assert(ai == x && bu == y ==> (ai * bu) == (x * y)) by(bit_vector);
            assert(au == x && bi == y ==> (au * bi) == (x * y)) by(bit_vector);
            assert(au == x && bu == y ==> (au * bu) == (x * y)) by(bit_vector);
            assert(ai == x && (bi + bi2) == y ==> (ai * (bi + bi2)) == (x * y)) by(bit_vector);
            assert(ai == x && (bu + bu2) == y ==> (ai * (bu + bu2)) == (x * y)) by(bit_vector);
            assert(au == x && (bi + bi2) == y ==> (au * (bi + bi2)) == (x * y)) by(bit_vector);
            assert(au == x && (bu + bu2) == y ==> (au * (bu + bu2)) == (x * y)) by(bit_vector);
            assert((ai + ai2) == x && bi == y ==> ((ai + ai2) * bi) == (x * y)) by(bit_vector);
            assert((ai + ai2) == x && bu == y ==> ((ai + ai2) * bu) == (x * y)) by(bit_vector);
            assert((au + au2) == x && bi == y ==> ((au + au2) * bi) == (x * y)) by(bit_vector);
            assert((au + au2) == x && bu == y ==> ((au + au2) * bu) == (x * y)) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_by_equating_le verus_code! {
        fn test_le(au: u8, au2: u8, bu: u8, bu2: u8, ai: i8, ai2: i8, bi: i8, bi2: i8, x: i32, y: i32) {
            assert(ai == x && bi == y ==> (ai <= bi) == (x <= y)) by(bit_vector);
            assert(ai == x && bu == y ==> (ai <= bu) == (x <= y)) by(bit_vector);
            assert(au == x && bi == y ==> (au <= bi) == (x <= y)) by(bit_vector);
            assert(au == x && bu == y ==> (au <= bu) == (x <= y)) by(bit_vector);
            assert(ai == x && (bi + bi2) == y ==> (ai <= (bi + bi2)) == (x <= y)) by(bit_vector);
            assert(ai == x && (bu + bu2) == y ==> (ai <= (bu + bu2)) == (x <= y)) by(bit_vector);
            assert(au == x && (bi + bi2) == y ==> (au <= (bi + bi2)) == (x <= y)) by(bit_vector);
            assert(au == x && (bu + bu2) == y ==> (au <= (bu + bu2)) == (x <= y)) by(bit_vector);
            assert((ai + ai2) == x && bi == y ==> ((ai + ai2) <= bi) == (x <= y)) by(bit_vector);
            assert((ai + ai2) == x && bu == y ==> ((ai + ai2) <= bu) == (x <= y)) by(bit_vector);
            assert((au + au2) == x && bi == y ==> ((au + au2) <= bi) == (x <= y)) by(bit_vector);
            assert((au + au2) == x && bu == y ==> ((au + au2) <= bu) == (x <= y)) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_by_equating_div verus_code! {
        fn test_div(au: u8, au2: u8, bu: u8, bu2: u8, ai: i8, ai2: i8, bi: i8, bi2: i8, x: u32, y: u32) {
            assert(y != 0 ==> ai == x && bi == y ==> (ai as int) / (bi as int) == x / y) by(bit_vector);
            assert(y != 0 ==> ai == x && bu == y ==> (ai as int) / (bu as int) == x / y) by(bit_vector);
            assert(y != 0 ==> au == x && bi == y ==> (au as int) / (bi as int) == x / y) by(bit_vector);
            assert(y != 0 ==> au == x && bu == y ==> (au as int) / (bu as int) == x / y) by(bit_vector);
            assert(y != 0 ==> ai == x && (bi + bi2) == y ==> (ai as int) / ((bi + bi2) as int) == x / y) by(bit_vector);
            assert(y != 0 ==> ai == x && (bu + bu2) == y ==> (ai as int) / ((bu + bu2) as int) == x / y) by(bit_vector);
            assert(y != 0 ==> au == x && (bi + bi2) == y ==> (au as int) / ((bi + bi2) as int) == x / y) by(bit_vector);
            assert(y != 0 ==> au == x && (bu + bu2) == y ==> (au as int) / ((bu + bu2) as int) == x / y) by(bit_vector);
            assert(y != 0 ==> (ai + ai2) == x && bi == y ==> ((ai + ai2) as int) / (bi as int) == x / y) by(bit_vector);
            assert(y != 0 ==> (ai + ai2) == x && bu == y ==> ((ai + ai2) as int) / (bu as int) == x / y) by(bit_vector);
            assert(y != 0 ==> (au + au2) == x && bi == y ==> ((au + au2) as int) / (bi as int) == x / y) by(bit_vector);
            assert(y != 0 ==> (au + au2) == x && bu == y ==> ((au + au2) as int) / (bu as int) == x / y) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_by_equating_mod verus_code! {
        fn test_mod(au: u8, au2: u8, bu: u8, bu2: u8, ai: i8, ai2: i8, bi: i8, bi2: i8, x: u32, y: u32) {
            assert(y != 0 ==> ai == x && bi == y ==> (ai as int) % (bi as int) == x % y) by(bit_vector);
            assert(y != 0 ==> ai == x && bu == y ==> (ai as int) % (bu as int) == x % y) by(bit_vector);
            assert(y != 0 ==> au == x && bi == y ==> (au as int) % (bi as int) == x % y) by(bit_vector);
            assert(y != 0 ==> au == x && bu == y ==> (au as int) % (bu as int) == x % y) by(bit_vector);
            assert(y != 0 ==> ai == x && (bi + bi2) == y ==> (ai as int) % ((bi + bi2) as int) == x % y) by(bit_vector);
            assert(y != 0 ==> ai == x && (bu + bu2) == y ==> (ai as int) % ((bu + bu2) as int) == x % y) by(bit_vector);
            assert(y != 0 ==> au == x && (bi + bi2) == y ==> (au as int) % ((bi + bi2) as int) == x % y) by(bit_vector);
            assert(y != 0 ==> au == x && (bu + bu2) == y ==> (au as int) % ((bu + bu2) as int) == x % y) by(bit_vector);
            assert(y != 0 ==> (ai + ai2) == x && bi == y ==> ((ai + ai2) as int) % (bi as int) == x % y) by(bit_vector);
            assert(y != 0 ==> (ai + ai2) == x && bu == y ==> ((ai + ai2) as int) % (bu as int) == x % y) by(bit_vector);
            assert(y != 0 ==> (au + au2) == x && bi == y ==> ((au + au2) as int) % (bi as int) == x % y) by(bit_vector);
            assert(y != 0 ==> (au + au2) == x && bu == y ==> ((au + au2) as int) % (bu as int) == x % y) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_by_equating_shr verus_code! {
        fn test_shr(au8: u8, au16: u16, bu8: u8, bu16: u16, ai8: i8, ai16: i16, x: i32, y: u32) {
            assert(ai8 == x && bu8 == y ==> (ai8 >> bu8) == (x >> y)) by(bit_vector);
            assert(au8 == x && bu8 == y ==> (au8 >> bu8) == (x >> y)) by(bit_vector);
            assert(ai8 == x && bu16 == y ==> (ai8 >> bu16) == (x >> y)) by(bit_vector);
            assert(au8 == x && bu16 == y ==> (au8 >> bu16) == (x >> y)) by(bit_vector);
            assert(ai16 == x && bu8 == y ==> (ai16 >> bu8) == (x >> y)) by(bit_vector);
            assert(au16 == x && bu8 == y ==> (au16 >> bu8) == (x >> y)) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_by_equating_shl verus_code! {
        fn test_shl(au8: u8, au16: u16, bu8: u8, bu16: u16, ai8: i8, ai16: i16, x: i32, y: u32) {
            assert(ai8 == x && bu8 == y ==> (ai8 << bu8) == (x << y) as i8) by(bit_vector);
            assert(au8 == x && bu8 == y ==> (au8 << bu8) == (x << y) as u8) by(bit_vector);
            assert(ai8 == x && bu16 == y ==> (ai8 << bu16) == (x << y) as i8) by(bit_vector);
            assert(au8 == x && bu16 == y ==> (au8 << bu16) == (x << y) as u8) by(bit_vector);
            assert(ai16 == x && bu8 == y ==> (ai16 << bu8) == (x << y) as i16) by(bit_vector);
            assert(au16 == x && bu8 == y ==> (au16 << bu8) == (x << y) as u16) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_signed_and_unsigned verus_code! {
        fn test_signed_comparing_to_unsigned(x: i8, y: i8, a: u8, b: u8) {
            // + / +
            assert(x >= 0 && y > 0 && x == a && y == b ==>
                x / y == a / b && x % y == a % b) by(bit_vector);

            // + / -
            assert(x >= 0 && y < 0 && x == a && (-y) == b ==>
                x / y == -(a / b) && x % y == a % b) by(bit_vector);

            // - / + (divisible)
            assert(x < 0 && y > 0 && (-x) == a && y == b ==>
                a % b == 0 ==>
                x / y == -(a / b) && x % y == 0) by(bit_vector);

            // - / + (not divisible)
            assert(x < 0 && y > 0 && (-x) == a && y == b ==>
                a % b != 0 ==>
                x / y == -(a / b) - 1 && x % y == b - (a % b)) by(bit_vector);

            // - / - (divisible)
            assert(x < 0 && y < 0 && (-x) == a && (-y) == b ==>
                a % b == 0 ==>
                x / y == (a / b) && x % y == 0) by(bit_vector);

            // - / - (not divisible)
            assert(x < 0 && y < 0 && (-x) == a && (-y) == b ==>
                a % b != 0 ==>
                x / y == (a / b) + 1 && x % y == b - (a % b)) by(bit_vector);
        }

        // test various combinations of signedness / bitwidth
        fn test_i_i(x: i8, y: i8, z: i8, a: i16, b: i16) {
            // i8 / i8
            assert(b != 0 && x == a && y == b ==>
                x / y == a / b) by(bit_vector);

            // i9 / i8
            assert(b != 0 && x+z == a && y == b ==>
                (x+z) / y as int == a / b) by(bit_vector);

            // i8 / i9
            assert(b != 0 && x == a && (y+z) == b ==>
                x as int / (y+z) == a / b) by(bit_vector);

            assert(b != 0 && x == a && y == b ==>
                x % y == a % b) by(bit_vector);

            assert(b != 0 && x+z == a && y == b ==>
                (x+z) % y as int == a % b) by(bit_vector);

            assert(b != 0 && x == a && (y+z) == b ==>
                x as int % (y+z) == a % b) by(bit_vector);
        }

        fn test_u_i(x: u8, w: u8, y: i8, z: i8, a: i16, b: i16) {
            assert(b != 0 && x == a && y == b ==>
                x as int / y as int == a / b) by(bit_vector);

            assert(b != 0 && x+w == a && y == b ==>
                (x+w) / y as int == a / b) by(bit_vector);

            assert(b != 0 && x == a && (y+z) == b ==>
                x as int / (y+z) == a / b) by(bit_vector);

            assert(b != 0 && x == a && y == b ==>
                x as int % y as int == a % b) by(bit_vector);

            assert(b != 0 && x+w == a && y == b ==>
                (x+w) % y as int == a % b) by(bit_vector);

            assert(b != 0 && x == a && (y+z) == b ==>
                x as int % (y+z) == a % b) by(bit_vector);
        }

        fn test_i_u(x: i8, w: i8, y: u8, z: u8, a: i16, b: i16) {
            assert(b != 0 && x == a && y == b ==>
                x as int / y as int == a / b) by(bit_vector);

            assert(b != 0 && x+w == a && y == b ==>
                (x+w) / y as int == a / b) by(bit_vector);

            assert(b != 0 && x == a && (y+z) == b ==>
                x as int / (y+z) == a / b) by(bit_vector);

            assert(b != 0 && x == a && y == b ==>
                x as int % y as int == a % b) by(bit_vector);

            assert(b != 0 && x+w == a && y == b ==>
                (x+w) % y as int == a % b) by(bit_vector);

            assert(b != 0 && x == a && (y+z) == b ==>
                x as int % (y+z) == a % b) by(bit_vector);
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_forall verus_code! {
        proof fn test() {
            assert(forall |x: i32, y: i16| x == y ==> (x >> 2) == (y >> 2)) by(bit_vector);
            assert(forall |x: i32, y: i16| x >> 32 == y >> 16) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 1)
}

test_verify_one_bv_file! {
    #[test] test_let_binder verus_code! {
        proof fn test(x: i32, y: i16) {
            assert({let z = y; x == y ==> (x >> 2) == (z >> 2)}) by(bit_vector);
            assert({let z = y; x == y ==> (x >> 2) == (z >> 3)}) by(bit_vector); // FAILS
        }
    } => Err(err) => assert_fails(err, 1)
}

test_verify_one_bv_file! {
    #[test] issue_2778_unique_temporary_ids verus_code! {
        proof fn lemma_bv_crash(v: i32) {
            let lsb: i32 = if v % 2 == 1 { 1i32 } else { 0i32 };
            let mut v_shifted: i32 = (v / 2) as i32;

            if v < 0 {
                v_shifted = (v + 1) as i32;
                v_shifted = (-v_shifted) as i32;
                v_shifted = (v_shifted / 2) as i32;
                v_shifted = (v_shifted + 1) as i32;
                v_shifted = (-v_shifted) as i32;
            }

            assert(true) by (bit_vector)
                requires
                    v_shifted == if v >= 0 { v / 2 } else { -((-v - 1) / 2) - 1 },
                    lsb == if v % 2 == 1 { 1i32 } else { 0i32 },
                ;
        }
    } => Ok(())
}

test_verify_one_bv_file! {
    #[test] test_normal_solver verus_code! {
        fn test_unsigned(x: u16, y: u16) {
            assert((x | y) == (x as u32) | (y as u32));
            assert((x & y) == (x as u32) & (y as u32));
            assert((x ^ y) == (x as u32) ^ (y as u32));

            assert((x | y) == (x as i64) | (y as i64));
            assert((x & y) == (x as i64) & (y as i64));
            assert((x ^ y) == (x as i64) ^ (y as i64));
        }

        fn test_signed(x: i16, y: i16) {
            assert((x | y) == (x as i32) | (y as i32));
            assert((x & y) == (x as i32) & (y as i32));
            assert((x ^ y) == (x as i32) ^ (y as i32));
        }

        fn test_signed_fail(x: i16, y: i16) {
            assert((x | y) == (x as u32) | (y as u32)); // FAILS
        }

        fn test_signed_fail2(x: i16, y: i16) {
            assert((x & y) == (x as u32) & (y as u32)); // FAILS
        }

        fn test_signed_not(x: i16) {
            assert(!x == !(x as i32));
        }

        fn test_unsigned_not(x: u16) {
            assert(!x == !(x as u32)); // FAILS
        }

        fn test_shr(x: u16, y: u16) {
            assert(x >> 2 == (x as u32) >> 2);
            assert(x >> y == x >> (y as u32));
        }

        fn test_shl(x: u16) {
            assert(x << 2 == (x as u32) << 2); // FAILS
        }

        fn test_shl2(x: u16, y: u16) {
            assert(x >> y == x >> (y as u32));
        }

        fn test_shr_signed(x: i16, y: u16) {
            assert(x >> 2 == (x as i32) >> 2);
            assert(x >> y == x >> (y as u32));
        }

        fn test_shl_signed(x: i16) {
            assert(x << 2 == (x as i32) << 2); // FAILS
        }

        fn test_shl2_signed(x: i16, y: u16) {
            assert(x >> y == x >> (y as u32));
        }

        fn test_bounds(x: u16, y: u16, z: u32, w: int) {
            assert(0 <= (x | y) < 0x1_0000);
            assert(0 <= (x & y) < 0x1_0000);
            assert(0 <= (x ^ y) < 0x1_0000);
            assert(0 <= (x >> y) < 0x1_0000);
            assert(0 <= (x << y) < 0x1_0000);

            assert(0 <= (x >> z) < 0x1_0000);
            assert(0 <= (x << z) < 0x1_0000);

            assert(0 <= (x >> w) < 0x1_0000);
            assert(0 <= (x << w) < 0x1_0000);
        }
    } => Err(err) => assert_fails(err, 5)
}

// Only verify with simplification, since this won't succeed without it
test_verify_one_file! {
    #[test] test_functions verus_code! {
        const LIFE: u32 = 42;

        spec fn shifter(u: u32) -> u32 {
            u >> 1
        }

        spec fn xor(u: u32, v: u32) -> u32 {
            u & v
        }

        fn test() {
            let u: u32;
            let v: u32;
            assert(shifter(LIFE) == 21) by (bit_vector);
            assert(xor(add(u, v), add(v, u)) == add(u, v)) by (bit_vector);
            assert(forall |i:u32| shifter(i) == i / 2) by (bit_vector);
        }


        spec fn get_bit64(u: u64, index: u64) -> bool {
            (0x1u64 & (u >> index)) == 1
        }

        proof fn myproof() by (bit_vector)
            ensures
                get_bit64(1u64, 0),
        {}

        spec fn set_bit64(u: u64, index: u64, bit: bool) -> u64 {
            if bit {
                u | 1u64 << index
            } else {
                u & (!(1u64 << index))
            }
        }

        proof fn set_bit64_proof(bv_new: u64, bv_old: u64, index: u64, bit: bool) by (bit_vector)
            requires
                bv_new == set_bit64(bv_old, index, bit),
                index < 64,
            ensures
                get_bit64(bv_new, index) == bit,
                forall|loc2: u64|
                    (loc2 < 64 && loc2 != index) ==> (get_bit64(bv_new, loc2) == get_bit64(bv_old, loc2)),
        {
        }

        proof fn use_proof(bv_new: u64, bv_old: u64, index: u64, bit: bool, loc2: u64) {
            assume(bv_new == set_bit64(bv_old, index, bit));
            assume(index < 64);
            assume(loc2 < 64 && loc2 != index);
            set_bit64_proof(bv_new, bv_old, index, bit);
            assert(get_bit64(bv_new, loc2) == get_bit64(bv_old, loc2));
        }

        spec fn bv_shift(u: u32) -> u32 {
            u >> 1
        }

        fn test_assert_quantifiers_still_trigger(x: u32) {
            assert(forall |u| bv_shift(u) <= u) by (bit_vector);
            assert(bv_shift(x) <= x);
        }

    } => Ok(())
}

// Check the handling of WithTriggers expressions (created by the #![trigger ...] syntax).
//   https://github.com/verus-lang/verus/issues/1995
// This only works with simplification enabled,
test_verify_one_file! {
    #[test] test_const_in_with_triggers verus_code! {
        const ONE: u64 = 1;

        proof fn test_const_inlined_in_with_triggers() {
            // This works because the trigger is on the expression itself
            assert(forall|a: u64| #[trigger] (a & ONE) == a & ONE) by (bit_vector);
            // This requires the interpreter to inline ONE inside the WithTriggers body
            assert(forall|a: u64| #![trigger (a & 1)] a & ONE == a & ONE) by (bit_vector);
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_dereference_mut_ref verus_code! {
        fn nonlinear_test(x: &mut u64)
        {
            *x = 0;

            assert(*x == 0) by(bit_vector)
              requires *x == 0
        }

        fn nonlinear_test2(x: &mut u64)
        {
            *x = 0;

            assert(*x == 1) by(bit_vector) // FAILS
              requires *x == 0
        }
    } => Err(err) => assert_fails(err, 1)
}

test_verify_one_file_with_options! {
    #[test] test_dereference_mut_ref_2 [] => verus_code! {
        fn nonlinear_test(x: &mut u64, y: &mut u64)
        {
            assert(*x == *y ==> x == y) by(bit_vector)
        }
    } => Err(err) => assert_vir_error_msg(err, "`bit_vector` prover cannot handle type `&mut u64`")
}

test_verify_one_file_with_options! {
    #[test] test_dereference_mut_ref_final_not_supported [] => verus_code! {
        fn nonlinear_test(x: &mut u64)
        {
            assert(*final(x) == *x) by(bit_vector)
        }
    } => Err(err) => assert_vir_error_msg(err, "Verus does not currently support this mutable reference operator")
}

test_verify_one_file_with_options! {
    #[test] test_old_not_supported [] => verus_code! {
        fn nonlinear(x: &mut u64)
            requires *x == 0,
        {
            *x = 5;
            assert(*x == 0 && *old(x) == 5) by(bit_vector);
        }
    } => Err(err) => assert_vir_error_msg(err, "`old` is not supported in `bit_vector` assert")
}

test_verify_one_file! {
    #[test] bad_assign_in_assert_by_bitvector_issue3035 verus_code! {
        proof fn bad_assign()
            ensures false
        {
            let ghost mut g: int = 0;
            assert(g == 1) by(bit_vector) {
                g = 1;  // only visible to the inner query
            }
        }
    } => Err(err) => assert_vir_error_msg(err, "assignment is not allowed in `assert ... by` statement")
}