2 files changed, 15 insertions, 15 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index a694cff1..8161e7cd 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -184,18 +184,18 @@ let test_split_list_fwd : result unit =
 (** Unit test for [no_nested_borrows::test_split_list] *)
 let _ = assert_norm (test_split_list_fwd = Return ())
 
-(** [no_nested_borrows::get_elem] *)
-let get_elem_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
+(** [no_nested_borrows::choose] *)
+let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
   if b then Return x else Return y
 
-(** [no_nested_borrows::get_elem] *)
-let get_elem_back
+(** [no_nested_borrows::choose] *)
+let choose_back
   (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
   if b then Return (ret, y) else Return (x, ret)
 
-(** [no_nested_borrows::get_elem_test] *)
-let get_elem_test_fwd : result unit =
-  begin match get_elem_fwd i32 true 0 0 with
+(** [no_nested_borrows::choose_test] *)
+let choose_test_fwd : result unit =
+  begin match choose_fwd i32 true 0 0 with
   | Fail -> Fail
   | Return z ->
     begin match i32_add z 1 with
@@ -204,7 +204,7 @@ let get_elem_test_fwd : result unit =
       if not (z0 = 1)
       then Fail
       else
-        begin match get_elem_back i32 true 0 0 z0 with
+        begin match choose_back i32 true 0 0 z0 with
         | Fail -> Fail
         | Return (x, y) ->
           if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
@@ -212,8 +212,8 @@ let get_elem_test_fwd : result unit =
     end
   end
 
-(** Unit test for [no_nested_borrows::get_elem_test] *)
-let _ = assert_norm (get_elem_test_fwd = Return ())
+(** Unit test for [no_nested_borrows::choose_test] *)
+let _ = assert_norm (choose_test_fwd = Return ())
 
 (** [no_nested_borrows::test_char] *)
 let test_char_fwd : result char = Return 'a'
diff --git a/tests/misc/BetreePolonius.fst b/tests/misc/PoloniusList.fst
index 2bac07b6..73e98884 100644
--- a/tests/misc/BetreePolonius.fst
+++ b/tests/misc/PoloniusList.fst
@@ -1,16 +1,16 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_polonius] *)
-module BetreePolonius
+(** [polonius_list] *)
+module PoloniusList
 open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_polonius::List] *)
+(** [polonius_list::List] *)
 type list_t (t : Type0) =
 | ListCons : t -> list_t t -> list_t t
 | ListNil : list_t t
 
-(** [betree_polonius::get_list_at_x] *)
+(** [polonius_list::get_list_at_x] *)
 let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
   begin match ls with
   | ListCons hd tl ->
@@ -24,7 +24,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
   | ListNil -> Return ListNil
   end
 
-(** [betree_polonius::get_list_at_x] *)
+(** [polonius_list::get_list_at_x] *)
 let rec get_list_at_x_back
   (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
   begin match ls with