From e7b4aba11391bede785799237a73ef7bd16d0372 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Oct 2022 18:04:31 +0200
Subject: Use "polonius" in the names instead of "nll"

---
 tests/misc/BetreeNll.fst      | 41 -----------------------------------------
 tests/misc/BetreePolonius.fst | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 41 deletions(-)
 delete mode 100644 tests/misc/BetreeNll.fst
 create mode 100644 tests/misc/BetreePolonius.fst

(limited to 'tests/misc')

diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreeNll.fst
deleted file mode 100644
index b548a18b..00000000
--- a/tests/misc/BetreeNll.fst
+++ /dev/null
@@ -1,41 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_nll] *)
-module BetreeNll
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_nll::List] *)
-type list_t (t : Type0) =
-| ListCons : t -> list_t t -> list_t t
-| ListNil : list_t t
-
-(** [betree_nll::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 ->
-    if hd = x
-    then Return (ListCons hd tl)
-    else
-      begin match get_list_at_x_fwd tl x with
-      | Fail -> Fail
-      | Return l -> Return l
-      end
-  | ListNil -> Return ListNil
-  end
-
-(** [betree_nll::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
-  | ListCons hd tl ->
-    if hd = x
-    then Return ret
-    else
-      begin match get_list_at_x_back tl x ret with
-      | Fail -> Fail
-      | Return tl0 -> Return (ListCons hd tl0)
-      end
-  | ListNil -> Return ret
-  end
-
diff --git a/tests/misc/BetreePolonius.fst b/tests/misc/BetreePolonius.fst
new file mode 100644
index 00000000..2bac07b6
--- /dev/null
+++ b/tests/misc/BetreePolonius.fst
@@ -0,0 +1,41 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_polonius] *)
+module BetreePolonius
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_polonius::List] *)
+type list_t (t : Type0) =
+| ListCons : t -> list_t t -> list_t t
+| ListNil : list_t t
+
+(** [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 ->
+    if hd = x
+    then Return (ListCons hd tl)
+    else
+      begin match get_list_at_x_fwd tl x with
+      | Fail -> Fail
+      | Return l -> Return l
+      end
+  | ListNil -> Return ListNil
+  end
+
+(** [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
+  | ListCons hd tl ->
+    if hd = x
+    then Return ret
+    else
+      begin match get_list_at_x_back tl x ret with
+      | Fail -> Fail
+      | Return tl0 -> Return (ListCons hd tl0)
+      end
+  | ListNil -> Return ret
+  end
+
-- 
cgit v1.2.3


From 6ca61f1deb2f2e45bf55c2b3fcf15b57a7b51ecb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Oct 2022 21:12:33 +0200
Subject: Regenerate the files

---
 tests/misc/Constants.fst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/misc')

diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index 4a9a0e48..884d1778 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -9,7 +9,7 @@ open Primitives
 let x0_body : result u32 = Return 0
 let x0_c : u32 = eval_global x0_body
 
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::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
 
-- 
cgit v1.2.3