From 3c5fb260012ee8bb8b9fd90bc4624d893ac7678a Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Mon, 8 Aug 2022 15:16:14 +0200
Subject: Register global names, one error remaining

---
 tests/misc/Constants.fst | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'tests/misc')

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
-- 
cgit v1.2.3