2 files changed, 24 insertions, 22 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index f6045dfd..f4ba7927 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -1139,8 +1139,8 @@ let rec betree_node_apply_messages_fwd
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
   Tot (result (state & unit))
-  (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
-  st))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
   =
   begin match self with
   | BetreeNodeInternal node ->
@@ -1229,8 +1229,8 @@ and betree_node_apply_messages_back
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
   Tot (result (betree_node_t & betree_node_id_counter_t))
-  (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
-  st))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
   =
   begin match self with
   | BetreeNodeInternal node ->
@@ -1329,8 +1329,8 @@ and betree_internal_flush_fwd
   (node_id_cnt : betree_node_id_counter_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) :
   Tot (result (state & (betree_list_t (u64 & betree_message_t))))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
   =
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
@@ -1397,8 +1397,8 @@ and betree_internal_flush_back
   (node_id_cnt : betree_node_id_counter_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) :
   Tot (result (betree_internal_t & betree_node_id_counter_t))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
   =
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 6a2b7c09..1560624b 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -1222,8 +1222,8 @@ let rec betree_node_apply_messages_fwd
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
   Tot (result (state & unit))
-  (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
-  st))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
   =
   begin match self with
   | BetreeNodeInternal node ->
@@ -1318,8 +1318,8 @@ and betree_node_apply_messages_back'a
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
   Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
-  (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
-  st))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
   =
   begin match self with
   | BetreeNodeInternal node ->
@@ -1425,8 +1425,8 @@ and betree_node_apply_messages_back1
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
   Tot (result (state & unit))
-  (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
-  st))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
   =
   begin match self with
   | BetreeNodeInternal node ->
@@ -1533,8 +1533,8 @@ and betree_internal_flush_fwd
   (node_id_cnt : betree_node_id_counter_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) :
   Tot (result (state & (betree_list_t (u64 & betree_message_t))))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
   =
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
@@ -1619,10 +1619,11 @@ and betree_internal_flush_fwd
 and betree_internal_flush_back'a
   (self : betree_internal_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state)
+  :
   Tot (result (state & (betree_internal_t & betree_node_id_counter_t)))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
   =
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
@@ -1716,10 +1717,11 @@ and betree_internal_flush_back'a
 and betree_internal_flush_back1
   (self : betree_internal_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state)
+  :
   Tot (result (state & unit))
-  (decreases (betree_internal_flush_decreases self params node_id_cnt content
-  st))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
   =
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content