15 files changed, 395 insertions, 210 deletions

diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst
index eb26276c..c2412775 100644
--- a/tests/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/betree/BetreeMain.Clauses.Template.fst
@@ -6,6 +6,10 @@ open BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
+(** [core::num::u64::{9}::MAX] *)
+let core_num_u64_max_body : result u64 = Return 18446744073709551615
+let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
+
 (** [betree_main::betree::List::{1}::len]: decreases clause *)
 unfold
 let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : nat =
@@ -42,18 +46,18 @@ let betree_node_apply_upserts_decreases
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
-unfold
-let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
-  (key : u64) (st : state) : nat =
-  admit ()
-
 (** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
 unfold
 let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
   (st : state) : nat =
   admit ()
 
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
+unfold
+let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
+  (key : u64) (st : state) : nat =
+  admit ()
+
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
 let betree_node_lookup_mut_in_bindings_decreases (key : u64)
@@ -86,17 +90,17 @@ let betree_node_apply_messages_to_internal_decreases
   (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
+(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
 unfold
-let betree_internal_flush_decreases (self : betree_internal_t)
+let betree_node_apply_messages_decreases (self : betree_node_t)
   (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
 unfold
-let betree_node_apply_messages_decreases (self : betree_node_t)
+let betree_internal_flush_decreases (self : betree_internal_t)
   (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
   admit ()
 
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index 9b960ce5..e80e96a6 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -80,6 +80,10 @@ let betree_node_id_counter_fresh_id_back
   | Return i -> Return (Mkbetree_node_id_counter_t i)
   end
 
+(** [core::num::u64::{9}::MAX] *)
+let core_num_u64_max_body : result u64 = Return 18446744073709551615
+let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
+
 (** [betree_main::betree::upsert_update] *)
 let betree_upsert_update_fwd
   (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
@@ -92,7 +96,7 @@ let betree_upsert_update_fwd
   | Some prev0 ->
     begin match st with
     | BetreeUpsertFunStateAdd v ->
-      begin match u64_sub 18446744073709551615 prev0 with
+      begin match u64_sub core_num_u64_max_c prev0 with
       | Fail -> Fail
       | Return margin ->
         if margin >= v
@@ -101,7 +105,7 @@ let betree_upsert_update_fwd
           | Fail -> Fail
           | Return i -> Return i
           end
-        else Return 18446744073709551615
+        else Return core_num_u64_max_c
       end
     | BetreeUpsertFunStateSub v ->
       if prev0 >= v
@@ -468,48 +472,8 @@ let rec betree_node_apply_upserts_back
       end
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-let rec betree_internal_lookup_in_children_fwd
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    begin match betree_node_lookup_fwd self.betree_internal_left key st with
-    | Fail -> Fail
-    | Return (st0, opt) -> Return (st0, opt)
-    end
-  else
-    begin match betree_node_lookup_fwd self.betree_internal_right key st with
-    | Fail -> Fail
-    | Return (st0, opt) -> Return (st0, opt)
-    end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-and betree_internal_lookup_in_children_back
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result betree_internal_t)
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    begin match betree_node_lookup_back self.betree_internal_left key st with
-    | Fail -> Fail
-    | Return n ->
-      Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot n self.betree_internal_right)
-    end
-  else
-    begin match betree_node_lookup_back self.betree_internal_right key st with
-    | Fail -> Fail
-    | Return n ->
-      Return (Mkbetree_internal_t self.betree_internal_id
-        self.betree_internal_pivot self.betree_internal_left n)
-    end
-
 (** [betree_main::betree::Node::{5}::lookup] *)
-and betree_node_lookup_fwd
+let rec betree_node_lookup_fwd
   (self : betree_node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
   (decreases (betree_node_lookup_decreases self key st))
@@ -723,6 +687,46 @@ and betree_node_lookup_back
     end
   end
 
+(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
+and betree_internal_lookup_in_children_fwd
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result (state & (option u64)))
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then
+    begin match betree_node_lookup_fwd self.betree_internal_left key st with
+    | Fail -> Fail
+    | Return (st0, opt) -> Return (st0, opt)
+    end
+  else
+    begin match betree_node_lookup_fwd self.betree_internal_right key st with
+    | Fail -> Fail
+    | Return (st0, opt) -> Return (st0, opt)
+    end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
+and betree_internal_lookup_in_children_back
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result betree_internal_t)
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then
+    begin match betree_node_lookup_back self.betree_internal_left key st with
+    | Fail -> Fail
+    | Return n ->
+      Return (Mkbetree_internal_t self.betree_internal_id
+        self.betree_internal_pivot n self.betree_internal_right)
+    end
+  else
+    begin match betree_node_lookup_back self.betree_internal_right key st with
+    | Fail -> Fail
+    | Return n ->
+      Return (Mkbetree_internal_t self.betree_internal_id
+        self.betree_internal_pivot self.betree_internal_left n)
+    end
+
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 let rec betree_node_lookup_mut_in_bindings_fwd
   (key : u64) (bindings : betree_list_t (u64 & u64)) :
@@ -1128,140 +1132,8 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   | BetreeListNil -> Return msgs
   end
 
-(** [betree_main::betree::Internal::{4}::flush] *)
-let rec betree_internal_flush_fwd
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
-  =
-  begin match
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot with
-  | Fail -> Fail
-  | Return p ->
-    let (msgs_left, msgs_right) = p in
-    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
-    | Return len_left ->
-      if len_left >= params.betree_params_min_flush_size
-      then
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st with
-        | Fail -> Fail
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back self.betree_internal_left params
-              node_id_cnt msgs_left st with
-          | Fail -> Fail
-          | Return (_, node_id_cnt0) ->
-            begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
-              with
-            | Fail -> Fail
-            | Return len_right ->
-              if len_right >= params.betree_params_min_flush_size
-              then
-                begin match
-                  betree_node_apply_messages_fwd self.betree_internal_right
-                    params node_id_cnt0 msgs_right st0 with
-                | Fail -> Fail
-                | Return (st1, _) ->
-                  begin match
-                    betree_node_apply_messages_back self.betree_internal_right
-                      params node_id_cnt0 msgs_right st0 with
-                  | Fail -> Fail
-                  | Return (_, _) -> Return (st1, BetreeListNil)
-                  end
-                end
-              else Return (st0, msgs_right)
-            end
-          end
-        end
-      else
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_right params
-            node_id_cnt msgs_right st with
-        | Fail -> Fail
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back self.betree_internal_right params
-              node_id_cnt msgs_right st with
-          | Fail -> Fail
-          | Return (_, _) -> Return (st0, msgs_left)
-          end
-        end
-    end
-  end
-
-(** [betree_main::betree::Internal::{4}::flush] *)
-and betree_internal_flush_back
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (betree_internal_t & betree_node_id_counter_t))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
-  =
-  begin match
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot with
-  | Fail -> Fail
-  | Return p ->
-    let (msgs_left, msgs_right) = p in
-    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
-    | Return len_left ->
-      if len_left >= params.betree_params_min_flush_size
-      then
-        begin match
-          betree_node_apply_messages_fwd self.betree_internal_left params
-            node_id_cnt msgs_left st with
-        | Fail -> Fail
-        | Return (st0, _) ->
-          begin match
-            betree_node_apply_messages_back self.betree_internal_left params
-              node_id_cnt msgs_left st with
-          | Fail -> Fail
-          | Return (n, node_id_cnt0) ->
-            begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
-              with
-            | Fail -> Fail
-            | Return len_right ->
-              if len_right >= params.betree_params_min_flush_size
-              then
-                begin match
-                  betree_node_apply_messages_back self.betree_internal_right
-                    params node_id_cnt0 msgs_right st0 with
-                | Fail -> Fail
-                | Return (n0, node_id_cnt1) ->
-                  Return (Mkbetree_internal_t self.betree_internal_id
-                    self.betree_internal_pivot n n0, node_id_cnt1)
-                end
-              else
-                Return (Mkbetree_internal_t self.betree_internal_id
-                  self.betree_internal_pivot n self.betree_internal_right,
-                  node_id_cnt0)
-            end
-          end
-        end
-      else
-        begin match
-          betree_node_apply_messages_back self.betree_internal_right params
-            node_id_cnt msgs_right st with
-        | Fail -> Fail
-        | Return (n, node_id_cnt0) ->
-          Return (Mkbetree_internal_t self.betree_internal_id
-            self.betree_internal_pivot self.betree_internal_left n,
-            node_id_cnt0)
-        end
-    end
-  end
-
 (** [betree_main::betree::Node::{5}::apply_messages] *)
-and betree_node_apply_messages_fwd
+let rec betree_node_apply_messages_fwd
   (self : betree_node_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
@@ -1450,6 +1322,138 @@ and betree_node_apply_messages_back
     end
   end
 
+(** [betree_main::betree::Internal::{4}::flush] *)
+and betree_internal_flush_fwd
+  (self : betree_internal_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
+  (decreases (betree_internal_flush_decreases self params node_id_cnt content
+  st))
+  =
+  begin match
+    betree_list_partition_at_pivot_fwd betree_message_t content
+      self.betree_internal_pivot with
+  | Fail -> Fail
+  | Return p ->
+    let (msgs_left, msgs_right) = p in
+    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
+    | Fail -> Fail
+    | Return len_left ->
+      if len_left >= params.betree_params_min_flush_size
+      then
+        begin match
+          betree_node_apply_messages_fwd self.betree_internal_left params
+            node_id_cnt msgs_left st with
+        | Fail -> Fail
+        | Return (st0, _) ->
+          begin match
+            betree_node_apply_messages_back self.betree_internal_left params
+              node_id_cnt msgs_left st with
+          | Fail -> Fail
+          | Return (_, node_id_cnt0) ->
+            begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
+              with
+            | Fail -> Fail
+            | Return len_right ->
+              if len_right >= params.betree_params_min_flush_size
+              then
+                begin match
+                  betree_node_apply_messages_fwd self.betree_internal_right
+                    params node_id_cnt0 msgs_right st0 with
+                | Fail -> Fail
+                | Return (st1, _) ->
+                  begin match
+                    betree_node_apply_messages_back self.betree_internal_right
+                      params node_id_cnt0 msgs_right st0 with
+                  | Fail -> Fail
+                  | Return (_, _) -> Return (st1, BetreeListNil)
+                  end
+                end
+              else Return (st0, msgs_right)
+            end
+          end
+        end
+      else
+        begin match
+          betree_node_apply_messages_fwd self.betree_internal_right params
+            node_id_cnt msgs_right st with
+        | Fail -> Fail
+        | Return (st0, _) ->
+          begin match
+            betree_node_apply_messages_back self.betree_internal_right params
+              node_id_cnt msgs_right st with
+          | Fail -> Fail
+          | Return (_, _) -> Return (st0, msgs_left)
+          end
+        end
+    end
+  end
+
+(** [betree_main::betree::Internal::{4}::flush] *)
+and betree_internal_flush_back
+  (self : betree_internal_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+  Tot (result (betree_internal_t & betree_node_id_counter_t))
+  (decreases (betree_internal_flush_decreases self params node_id_cnt content
+  st))
+  =
+  begin match
+    betree_list_partition_at_pivot_fwd betree_message_t content
+      self.betree_internal_pivot with
+  | Fail -> Fail
+  | Return p ->
+    let (msgs_left, msgs_right) = p in
+    begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
+    | Fail -> Fail
+    | Return len_left ->
+      if len_left >= params.betree_params_min_flush_size
+      then
+        begin match
+          betree_node_apply_messages_fwd self.betree_internal_left params
+            node_id_cnt msgs_left st with
+        | Fail -> Fail
+        | Return (st0, _) ->
+          begin match
+            betree_node_apply_messages_back self.betree_internal_left params
+              node_id_cnt msgs_left st with
+          | Fail -> Fail
+          | Return (n, node_id_cnt0) ->
+            begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
+              with
+            | Fail -> Fail
+            | Return len_right ->
+              if len_right >= params.betree_params_min_flush_size
+              then
+                begin match
+                  betree_node_apply_messages_back self.betree_internal_right
+                    params node_id_cnt0 msgs_right st0 with
+                | Fail -> Fail
+                | Return (n0, node_id_cnt1) ->
+                  Return (Mkbetree_internal_t self.betree_internal_id
+                    self.betree_internal_pivot n n0, node_id_cnt1)
+                end
+              else
+                Return (Mkbetree_internal_t self.betree_internal_id
+                  self.betree_internal_pivot n self.betree_internal_right,
+                  node_id_cnt0)
+            end
+          end
+        end
+      else
+        begin match
+          betree_node_apply_messages_back self.betree_internal_right params
+            node_id_cnt msgs_right st with
+        | Fail -> Fail
+        | Return (n, node_id_cnt0) ->
+          Return (Mkbetree_internal_t self.betree_internal_id
+            self.betree_internal_pivot self.betree_internal_left n,
+            node_id_cnt0)
+        end
+    end
+  end
+
 (** [betree_main::betree::Node::{5}::apply] *)
 let betree_node_apply_fwd
   (self : betree_node_t) (params : betree_params_t)
diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti
index a937c726..f0ca1d9e 100644
--- a/tests/betree/BetreeMain.Types.fsti
+++ b/tests/betree/BetreeMain.Types.fsti
@@ -24,8 +24,13 @@ type betree_message_t =
 (** [betree_main::betree::Leaf] *)
 type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
 
+(** [betree_main::betree::Node] *)
+type betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
 (** [betree_main::betree::Internal] *)
-type betree_internal_t =
+and betree_internal_t =
 {
   betree_internal_id : u64;
   betree_internal_pivot : u64;
@@ -33,11 +38,6 @@ type betree_internal_t =
   betree_internal_right : betree_node_t;
 }
 
-(** [betree_main::betree::Node] *)
-and betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
 (** [betree_main::betree::Params] *)
 type betree_params_t =
 {
@@ -55,6 +55,10 @@ type betree_be_tree_t =
   betree_be_tree_root : betree_node_t;
 }
 
+(** [core::num::u64::{9}::MAX] *)
+let core_num_u64_max_body : result u64 = Return 18446744073709551615
+let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
+
 (** The state type used in the state-error monad *)
 val state : Type0
 
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index fe351f3a..b44fe9d1 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
 (*** Misc *)
 type char = FStar.Char.char
 type string = string
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)
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 83c245fb..397ee720 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -188,6 +188,10 @@ let hash_map_insert_no_resize_fwd_back
     end
   end
 
+(** [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] *)
 let rec hash_map_move_elements_from_list_fwd_back
   (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
@@ -244,7 +248,7 @@ let rec hash_map_move_elements_fwd_back
 (** [hashmap::HashMap::{0}::try_resize] *)
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
-  begin match scalar_cast U32 Usize 4294967295 with
+  begin match scalar_cast U32 Usize core_num_u32_max_c with
   | Fail -> Fail
   | Return max_usize ->
     let capacity = vec_len (list_t t) self.hash_map_slots in
diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst
index 91ee26c6..f81f4185 100644
--- a/tests/hashmap/Hashmap.Types.fst
+++ b/tests/hashmap/Hashmap.Types.fst
@@ -19,3 +19,7 @@ type hash_map_t (t : Type0) =
   hash_map_slots : vec (list_t t);
 }
 
+(** [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
+
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index fe351f3a..b44fe9d1 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
 (*** Misc *)
 type char = FStar.Char.char
 type string = string
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 3c5ee819..0cf876d9 100644
--- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -24,6 +24,10 @@ let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize)
   (value : t) (ls : hashmap_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_main::hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
 unfold
 let hashmap_hash_map_move_elements_from_list_decreases (t : Type0)
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index d01046ec..83bf80d1 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -198,6 +198,10 @@ let hashmap_hash_map_insert_no_resize_fwd_back
     end
   end
 
+(** [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_main::hashmap::HashMap::{0}::move_elements_from_list] *)
 let rec hashmap_hash_map_move_elements_from_list_fwd_back
   (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
@@ -257,7 +261,7 @@ let rec hashmap_hash_map_move_elements_fwd_back
 (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
 let hashmap_hash_map_try_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
-  begin match scalar_cast U32 Usize 4294967295 with
+  begin match scalar_cast U32 Usize core_num_u32_max_c with
   | Fail -> Fail
   | Return max_usize ->
     let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/hashmap_on_disk/HashmapMain.Types.fsti
index e289174b..370844db 100644
--- a/tests/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/hashmap_on_disk/HashmapMain.Types.fsti
@@ -19,6 +19,10 @@ type hashmap_hash_map_t (t : Type0) =
   hashmap_hash_map_slots : vec (hashmap_list_t t);
 }
 
+(** [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
+
 (** The state type used in the state-error monad *)
 val state : Type0
 
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index fe351f3a..b44fe9d1 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
 (*** Misc *)
 type char = FStar.Char.char
 type string = string
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
new file mode 100644
index 00000000..4a9a0e48
--- /dev/null
+++ b/tests/misc/Constants.fst
@@ -0,0 +1,137 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [constants] *)
+module Constants
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [constants::X0] *)
+let x0_body : result u32 = Return 0
+let x0_c : u32 = eval_global x0_body
+
+(** [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
+
+(** [constants::X1] *)
+let x1_body : result u32 = Return core_num_u32_max_c
+let x1_c : u32 = eval_global x1_body
+
+(** [constants::X2] *)
+let x2_body : result u32 = Return 3
+let x2_c : u32 = eval_global x2_body
+
+(** [constants::incr] *)
+let incr_fwd (n : u32) : result u32 =
+  begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::X3] *)
+let x3_body : result u32 =
+  begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+let x3_c : u32 = eval_global x3_body
+
+(** [constants::mk_pair0] *)
+let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
+
+(** [constants::Pair] *)
+type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
+
+(** [constants::mk_pair1] *)
+let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
+  Return (Mkpair_t x y)
+
+(** [constants::P0] *)
+let p0_body : result (u32 & u32) =
+  begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+let p0_c : (u32 & u32) = eval_global p0_body
+
+(** [constants::P1] *)
+let p1_body : result (pair_t u32 u32) =
+  begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+let p1_c : pair_t u32 u32 = eval_global p1_body
+
+(** [constants::P2] *)
+let p2_body : result (u32 & u32) = Return (0, 1)
+let p2_c : (u32 & u32) = eval_global p2_body
+
+(** [constants::P3] *)
+let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+let p3_c : pair_t u32 u32 = eval_global p3_body
+
+(** [constants::Wrap] *)
+type wrap_t (t : Type0) = { wrap_val : t; }
+
+(** [constants::Wrap::{0}::new] *)
+let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
+  Return (Mkwrap_t val0)
+
+(** [constants::Y] *)
+let y_body : result (wrap_t i32) =
+  begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+let y_c : wrap_t i32 = eval_global y_body
+
+(** [constants::unwrap_y] *)
+let unwrap_y_fwd : result i32 = Return y_c.wrap_val
+
+(** [constants::YVAL] *)
+let yval_body : result i32 =
+  begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
+let yval_c : i32 = eval_global yval_body
+
+(** [constants::get_z1::Z1] *)
+let get_z1_z1_body : result i32 = Return 3
+let get_z1_z1_c : i32 = eval_global get_z1_z1_body
+
+(** [constants::get_z1] *)
+let get_z1_fwd : result i32 = Return get_z1_z1_c
+
+(** [constants::add] *)
+let add_fwd (a : i32) (b : i32) : result i32 =
+  begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::Q1] *)
+let q1_body : result i32 = Return 5
+let q1_c : i32 = eval_global q1_body
+
+(** [constants::Q2] *)
+let q2_body : result i32 = Return q1_c
+let q2_c : i32 = eval_global q2_body
+
+(** [constants::Q3] *)
+let q3_body : result i32 =
+  begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end
+let q3_c : i32 = eval_global q3_body
+
+(** [constants::get_z2] *)
+let get_z2_fwd : result i32 =
+  begin match get_z1_fwd with
+  | Fail -> Fail
+  | Return i ->
+    begin match add_fwd i q3_c with
+    | Fail -> Fail
+    | Return i0 ->
+      begin match add_fwd q1_c i0 with
+      | Fail -> Fail
+      | Return i1 -> Return i1
+      end
+    end
+  end
+
+(** [constants::S1] *)
+let s1_body : result u32 = Return 6
+let s1_c : u32 = eval_global s1_body
+
+(** [constants::S2] *)
+let s2_body : result u32 =
+  begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end
+let s2_c : u32 = eval_global s2_body
+
+(** [constants::S3] *)
+let s3_body : result (pair_t u32 u32) = Return p3_c
+let s3_c : pair_t u32 u32 = eval_global s3_body
+
+(** [constants::S4] *)
+let s4_body : result (pair_t u32 u32) =
+  begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+let s4_c : pair_t u32 u32 = eval_global s4_body
+
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 35d32514..a694cff1 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -218,36 +218,36 @@ let _ = assert_norm (get_elem_test_fwd = Return ())
 (** [no_nested_borrows::test_char] *)
 let test_char_fwd : result char = Return 'a'
 
-(** [no_nested_borrows::Tree] *)
-type tree_t (t : Type0) =
-| TreeLeaf : t -> tree_t t
-| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
-
 (** [no_nested_borrows::NodeElem] *)
-and node_elem_t (t : Type0) =
+type node_elem_t (t : Type0) =
 | NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
 | NodeElemNil : node_elem_t t
 
-(** [no_nested_borrows::even] *)
-let rec even_fwd (x : u32) : result bool =
+(** [no_nested_borrows::Tree] *)
+and tree_t (t : Type0) =
+| TreeLeaf : t -> tree_t t
+| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
+
+(** [no_nested_borrows::odd] *)
+let rec odd_fwd (x : u32) : result bool =
   if x = 0
-  then Return true
+  then Return false
   else
     begin match u32_sub x 1 with
     | Fail -> Fail
     | Return i ->
-      begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
+      begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
     end
 
-(** [no_nested_borrows::odd] *)
-and odd_fwd (x : u32) : result bool =
+(** [no_nested_borrows::even] *)
+and even_fwd (x : u32) : result bool =
   if x = 0
-  then Return false
+  then Return true
   else
     begin match u32_sub x 1 with
     | Fail -> Fail
     | Return i ->
-      begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
+      begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
     end
 
 (** [no_nested_borrows::test_even_odd] *)
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index fe351f3a..b44fe9d1 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
 (*** Misc *)
 type char = FStar.Char.char
 type string = string