summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar')
-rw-r--r--tests/fstar/arrays/Arrays.Funs.fst4
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index 289e603d..26a695bb 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -241,9 +241,9 @@ let index_all : result u32 =
let* (s1, to_slice_mut_back) =
array_to_slice_mut u32 2 (mk_array u32 2 [ 0; 0 ]) in
let* (i7, s2) = index_mut_slice_u32_0 s1 in
- let* i8 = u32_add i6 i7 in
+ let* i9 = u32_add i6 i7 in
let* _ = to_slice_mut_back s2 in
- Ok i8
+ Ok i9
(** [arrays::update_array]:
Source: 'tests/src/arrays.rs', lines 187:0-187:36 *)