diff --git a/crates/flux-tests/tests/neg/surface/arr02.rs b/crates/flux-tests/tests/neg/surface/arr02.rs index 743f1942d7..6350a47361 100644 --- a/crates/flux-tests/tests/neg/surface/arr02.rs +++ b/crates/flux-tests/tests/neg/surface/arr02.rs @@ -14,3 +14,10 @@ fn test01() -> i32 { *arr[1] += 1; v1 //~ ERROR refinement type } + +#[flux::sig(fn() -> i32{v: v < 0})] +fn test02() -> i32 { + let v = 42; + let arr = [&v, &v]; + *arr[0] //~ ERROR refinement type +} diff --git a/crates/flux-tests/tests/pos/surface/arr02.rs b/crates/flux-tests/tests/pos/surface/arr02.rs index fcb29c3bd7..0c0cb7c9cf 100644 --- a/crates/flux-tests/tests/pos/surface/arr02.rs +++ b/crates/flux-tests/tests/pos/surface/arr02.rs @@ -14,3 +14,10 @@ fn test01() -> i32 { *arr[1] += 1; v1 } + +#[flux::sig(fn() -> i32{v: v >= 0})] +fn test02() -> i32 { + let v = 42; + let arr = [&v, &v]; + *arr[0] +}