From a0c58326c43a7a8026b3d4c158017bf126180e90 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 23:23:30 +0100
Subject: Regenerate the test files and add the fstar-split tests

---
 tests/fstar/misc/Constants.fst | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'tests/fstar/misc/Constants.fst')

diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index daeefbb0..7bf42b46 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -20,7 +20,7 @@ let x1_c : u32 = eval_global x1_body
 let x2_body : result u32 = Return 3
 let x2_c : u32 = eval_global x2_body
 
-(** [constants::incr]: forward function
+(** [constants::incr]:
     Source: 'src/constants.rs', lines 17:0-17:32 *)
 let incr (n : u32) : result u32 =
   u32_add n 1
@@ -30,7 +30,7 @@ let incr (n : u32) : result u32 =
 let x3_body : result u32 = incr 32
 let x3_c : u32 = eval_global x3_body
 
-(** [constants::mk_pair0]: forward function
+(** [constants::mk_pair0]:
     Source: 'src/constants.rs', lines 23:0-23:51 *)
 let mk_pair0 (x : u32) (y : u32) : result (u32 & u32) =
   Return (x, y)
@@ -39,7 +39,7 @@ let mk_pair0 (x : u32) (y : u32) : result (u32 & u32) =
     Source: 'src/constants.rs', lines 36:0-36:23 *)
 type pair_t (t1 t2 : Type0) = { x : t1; y : t2; }
 
-(** [constants::mk_pair1]: forward function
+(** [constants::mk_pair1]:
     Source: 'src/constants.rs', lines 27:0-27:55 *)
 let mk_pair1 (x : u32) (y : u32) : result (pair_t u32 u32) =
   Return { x = x; y = y }
@@ -68,7 +68,7 @@ let p3_c : pair_t u32 u32 = eval_global p3_body
     Source: 'src/constants.rs', lines 49:0-49:18 *)
 type wrap_t (t : Type0) = { value : t; }
 
-(** [constants::{constants::Wrap<T>}::new]: forward function
+(** [constants::{constants::Wrap<T>}::new]:
     Source: 'src/constants.rs', lines 54:4-54:41 *)
 let wrap_new (t : Type0) (value : t) : result (wrap_t t) =
   Return { value = value }
@@ -78,7 +78,7 @@ let wrap_new (t : Type0) (value : t) : result (wrap_t t) =
 let y_body : result (wrap_t i32) = wrap_new i32 2
 let y_c : wrap_t i32 = eval_global y_body
 
-(** [constants::unwrap_y]: forward function
+(** [constants::unwrap_y]:
     Source: 'src/constants.rs', lines 43:0-43:30 *)
 let unwrap_y : result i32 =
   Return y_c.value
@@ -93,12 +93,12 @@ let yval_c : i32 = eval_global yval_body
 let get_z1_z1_body : result i32 = Return 3
 let get_z1_z1_c : i32 = eval_global get_z1_z1_body
 
-(** [constants::get_z1]: forward function
+(** [constants::get_z1]:
     Source: 'src/constants.rs', lines 61:0-61:28 *)
 let get_z1 : result i32 =
   Return get_z1_z1_c
 
-(** [constants::add]: forward function
+(** [constants::add]:
     Source: 'src/constants.rs', lines 66:0-66:39 *)
 let add (a : i32) (b : i32) : result i32 =
   i32_add a b
@@ -118,10 +118,10 @@ let q2_c : i32 = eval_global q2_body
 let q3_body : result i32 = add q2_c 3
 let q3_c : i32 = eval_global q3_body
 
-(** [constants::get_z2]: forward function
+(** [constants::get_z2]:
     Source: 'src/constants.rs', lines 70:0-70:28 *)
 let get_z2 : result i32 =
-  let* i = get_z1 in let* i0 = add i q3_c in add q1_c i0
+  let* i = get_z1 in let* i1 = add i q3_c in add q1_c i1
 
 (** [constants::S1]
     Source: 'src/constants.rs', lines 80:0-80:18 *)
-- 
cgit v1.2.3