From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/hol4/betree/betreeMain_FunsScript.sml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'tests/hol4/betree/betreeMain_FunsScript.sml')

diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml
index 5e604f8c..bd16c16c 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betreeMain_FunsScript.sml
@@ -88,14 +88,6 @@ val betree_node_id_counter_fresh_id_back_def = Define ‘
     od
 ’
 
-(** [core::num::u64::{9}::MAX] *)
-Definition core_num_u64_max_body_def:
-  core_num_u64_max_body : u64 result = Return (int_to_u64 18446744073709551615)
-End
-Definition core_num_u64_max_c_def:
-  core_num_u64_max_c : u64 = get_return_value core_num_u64_max_body
-End
-
 val betree_upsert_update_fwd_def = Define ‘
   (** [betree_main::betree::upsert_update]: forward function *)
   betree_upsert_update_fwd
@@ -109,8 +101,8 @@ val betree_upsert_update_fwd_def = Define ‘
       (case st of
       | BetreeUpsertFunStateAdd v =>
         do
-        margin <- u64_sub core_num_u64_max_c prev0;
-        if u64_ge margin v then u64_add prev0 v else Return core_num_u64_max_c
+        margin <- u64_sub core_u64_max prev0;
+        if u64_ge margin v then u64_add prev0 v else Return core_u64_max
         od
       | BetreeUpsertFunStateSub v =>
         if u64_ge prev0 v then u64_sub prev0 v else Return (int_to_u64 0)))
-- 
cgit v1.2.3