diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/hashmap/Primitives.fst | 4 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Primitives.fst | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index 3110b247..71d75c11 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/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() diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index 3110b247..71d75c11 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/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() |