summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2024-05-28 18:48:56 +0200
committerSon Ho2024-05-28 18:48:56 +0200
commitb5eac0384818e1f51fbfd900ab580514e851b0ca (patch)
tree7fc94f32e32674892154e7e72c2d589470c17f9a /tests
parentae075db15638ee8878bebe3d31affb1aa320e90f (diff)
Fix an issue with some names being ignored when generating unique variable names
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/arrays/Arrays.v4
-rw-r--r--tests/fstar/arrays/Arrays.Funs.fst4
2 files changed, 4 insertions, 4 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 371e4a12..6e4ab188 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -289,9 +289,9 @@ Definition index_all : result u32 :=
let (s1, to_slice_mut_back) := p in
p1 <- index_mut_slice_u32_0 s1;
let (i7, s2) := p1 in
- i8 <- u32_add i6 i7;
+ i9 <- u32_add i6 i7;
_ <- to_slice_mut_back s2;
- Ok i8
+ Ok i9
.
(** [arrays::update_array]:
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 *)