4 files changed, 30 insertions, 4 deletions
diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst
index a6808c98..8f0bfbbd 100644
--- a/tests/fstar/array/Array.Funs.fst
+++ b/tests/fstar/array/Array.Funs.fst
@@ -277,12 +277,12 @@ let deref_array_mut_borrow_back (x : array u32 2) : result (array u32 2) =
   let* _ = array_index_usize u32 2 x 0 in Return x
 
 (** [array::take_array_t]: forward function *)
-let take_array_t (a : array ab_t 2) : result unit =
+let take_array_t (a : array aB_t 2) : result unit =
   Return ()
 
 (** [array::non_copyable_array]: forward function *)
 let non_copyable_array : result unit =
-  let* _ = take_array_t (mk_array ab_t 2 [ ABA; ABB ]) in Return ()
+  let* _ = take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) in Return ()
 
 (** [array::sum]: loop 0: forward function *)
 let rec sum_loop
diff --git a/tests/fstar/array/Array.Opaque.fsti b/tests/fstar/array/Array.Opaque.fsti
new file mode 100644
index 00000000..484cb9ee
--- /dev/null
+++ b/tests/fstar/array/Array.Opaque.fsti
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [array]: external function declarations *)
+module Array.Opaque
+open Primitives
+include Array.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::array::[T; N]::{15}::index]: forward function *)
+val core_array_[T; N]_index_fwd
+  (t i : Type0) (n : usize) (inst : core_ops_index_Index (slice t) i) :
+  array t n -> i -> result inst.core_ops_index_Index_Output
+
+(** [core::array::[T; N]::{16}::index_mut]: forward function *)
+val core_array_[T; N]_index_mut_fwd
+  (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
+  array t n -> i -> result inst.index_inst.core_ops_index_Index_Output
+
+(** [core::array::[T; N]::{16}::index_mut]: backward function 0 *)
+val core_array_[T; N]_index_mut_back
+  (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
+  array t n -> i -> inst.index_inst.core_ops_index_Index_Output -> result
+    (array t n)
+
diff --git a/tests/fstar/array/Array.Types.fst b/tests/fstar/array/Array.Types.fst
index 0ec9c12f..4e8d5566 100644
--- a/tests/fstar/array/Array.Types.fst
+++ b/tests/fstar/array/Array.Types.fst
@@ -6,5 +6,5 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [array::AB] *)
-type ab_t = | ABA : ab_t | ABB : ab_t
+type aB_t = | AB_A : aB_t | AB_B : aB_t
 
diff --git a/tests/fstar/array/Primitives.fst b/tests/fstar/array/Primitives.fst
index 3110b247..71d75c11 100644
--- a/tests/fstar/array/Primitives.fst
+++ b/tests/fstar/array/Primitives.fst
@@ -707,5 +707,7 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
 let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
   Lemma (
     alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x ==
-      alloc_vec_Vec_update_usize v i x) =
+      alloc_vec_Vec_update_usize v i x)
+  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x)]
+  =
   admit()