thanhnguyen-aws

Thanks for reporting this issue. This is not a problem of user specified `loop_assign` (`loop_modifies`) clause, but that of handling lifetime of variables that are declared in a loop-body, then...

@feliperodri @zhassan-aws Thank you very much for your response.

Another example: This harness fails: ```rust #[kani::ensures(|result : &NonNull| !result.as_ptr().is_null())] pub const fn from_raw_parts_test( data_pointer: NonNull, metadata: ::Metadata, ) -> NonNull { // SAFETY: The result of `ptr::from::raw_parts_mut` is non-null...

Another example ```rust #[kani::requires(true)] pub const unsafe fn byte_add_n(s : NonNull, count: usize) -> NonNull { unsafe { NonNull::new_unchecked( s.as_ptr().byte_add(count) ) } } #[kani::proof_for_contract(byte_add_n)] pub fn non_null_byte_add_dangling_proof() { let ptr...

> A few notes from a discussion that was held out-of-band: it would be nice to have a syntax like `kani::index` (instead of `kaniindex` or `kani_index`) to make it entirely...

> Have you got my inc_vector() test case done? If so, please point me at the sources in the repo... Hello, we are fixing some issue with using quantifiers in...

Here is Z3's result: ``` Checking harness main3... CBMC 6.7.1 (cbmc-6.7.1) CBMC version 6.7.1 (cbmc-6.7.1) 64-bit arm64 macos Reading GOTO program from file /Users/ntson/kanitest/src/main__RNvCs9wCRUdekRrZ_4main5main3.out Generating GOTO Program Adding CPROVER library...