From 60ce69b83cbd749781543bb16becb5357f0e1a0a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 5 Dec 2023 15:00:46 +0100
Subject: Update following changes in Charon

---
 .../betree_back_stateful/BetreeMain.Clauses.Template.fst   | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst')

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 4ae29302..537705c5 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -33,6 +33,13 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
+unfold
+let betree_Node_lookup_in_bindings_decreases (key : u64)
+  (bindings : betree_List_t (u64 & u64)) : nat =
+  admit ()
+
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 unfold
@@ -41,13 +48,6 @@ let betree_Node_apply_upserts_decreases
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
-unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_List_t (u64 & u64)) : nat =
-  admit ()
-
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
     Source: 'src/betree.rs', lines 395:4-395:63 *)
 unfold
-- 
cgit v1.2.3