Merge pull request #4 from AeneasVerif/son_update_charon

Update the code to account for changes in Charon

1 files changed, 5 insertions, 5 deletions

diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreePolonius.fst
index b548a18b..2bac07b6 100644
--- a/tests/misc/BetreeNll.fst
+++ b/tests/misc/BetreePolonius.fst
@@ -1,16 +1,16 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_nll] *)
-module BetreeNll
+(** [betree_polonius] *)
+module BetreePolonius
 open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_nll::List] *)
+(** [betree_polonius::List] *)
 type list_t (t : Type0) =
 | ListCons : t -> list_t t -> list_t t
 | ListNil : list_t t
 
-(** [betree_nll::get_list_at_x] *)
+(** [betree_polonius::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_nll::get_list_at_x] *)
+(** [betree_polonius::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