From 05a937efaf57f7537e2ae0116502c78518e8226f Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Tue, 10 Oct 2023 17:26:34 -0700
Subject: [PATCH] Add test for issue 286 (#539)

---
 crates/flux-tests/tests/neg/surface/arr02.rs | 7 +++++++
 crates/flux-tests/tests/pos/surface/arr02.rs | 7 +++++++
 2 files changed, 14 insertions(+)

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]
+}