From 8543092569616ef6a75949a72532f7b73dc696f2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 18 Aug 2023 12:23:03 +0200
Subject: Regenerate the array tests

---
 tests/fstar/array/Array.Funs.fst | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tests/fstar/array')

diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst
index 72163585..83256398 100644
--- a/tests/fstar/array/Array.Funs.fst
+++ b/tests/fstar/array/Array.Funs.fst
@@ -347,6 +347,14 @@ let f3_fwd : result u32 =
         ]) 16 18 in
   sum2_fwd s s0
 
+(** [array::SZ] *)
+let sz_body : result usize = Return 32
+let sz_c : usize = eval_global sz_body
+
+(** [array::f5]: forward function *)
+let f5_fwd (x : array u32 32) : result u32 =
+  array_index_shared u32 32 x 0
+
 (** [array::ite]: forward function *)
 let ite_fwd : result unit =
   let* s = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in
-- 
cgit v1.2.3