From cd754eabe3af025ca3465c5fc6d8cb48da66a1ae Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Wed, 10 Aug 2022 18:56:25 +0200
Subject: Corrected translation without using functions, remaining bug in
 hashmap translation

---
 tests/hashmap/Hashmap.Clauses.Template.fst | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tests/hashmap/Hashmap.Clauses.Template.fst')

diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst
index c1549e6b..2a3d9cb9 100644
--- a/tests/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/hashmap/Hashmap.Clauses.Template.fst
@@ -24,6 +24,10 @@ let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
   (ls : list_t t) : nat =
   admit ()
 
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
 (** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
 unfold
 let hash_map_move_elements_from_list_decreases (t : Type0)
-- 
cgit v1.2.3