Register global names, one error remaining

1 files changed, 10 insertions, 0 deletions

diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index e1a942a0..f5bd41cb 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -4,3 +4,13 @@ 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] *)
\ No newline at end of file