diff options
author | Son Ho | 2024-05-28 18:48:56 +0200 |
---|---|---|
committer | Son Ho | 2024-05-28 18:48:56 +0200 |
commit | b5eac0384818e1f51fbfd900ab580514e851b0ca (patch) | |
tree | 7fc94f32e32674892154e7e72c2d589470c17f9a /tests | |
parent | ae075db15638ee8878bebe3d31affb1aa320e90f (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.v | 4 | ||||
-rw-r--r-- | tests/fstar/arrays/Arrays.Funs.fst | 4 |
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 *) |