I assumed ZST addresses are dangling, so they may or may not be equal for different instances of a type.

I tried this code:

#[repr(C)]
#[derive(Copy, Clone)]
struct Z(i8, i64);

struct Y;

#[kani::proof]
fn test_z() -> Z {
	let m = Y;
	let n = Y;
	let zz = Z(1, -1);
	
	let ptr: *const Z = if &n as *const _ == &m as *const _ {
		std::ptr::null()
	} else {
		&zz
	};
	unsafe{ *ptr }
}

using the following command line invocation:

kani main.rs

with Kani version: 0.48.0

I expected to see this happen: An error because addresses to ZSTs are not guaranteed to have distinct addresses at runtime. Running this snippet crashes playground

Instead, this happened:

...
SUMMARY:
 ** 0 of 7 failed

VERIFICATION:- SUCCESSFUL

Thanks!