From 1110b3da85e93ba0755a665edd5b8c986c54cef0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 16:15:35 +0200
Subject: Make minor modifications and update the array test for F*

---
 tests/fstar/array/Array.Clauses.Template.fst | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tests/fstar/array/Array.Clauses.Template.fst')

diff --git a/tests/fstar/array/Array.Clauses.Template.fst b/tests/fstar/array/Array.Clauses.Template.fst
index 8a15e230..06056d61 100644
--- a/tests/fstar/array/Array.Clauses.Template.fst
+++ b/tests/fstar/array/Array.Clauses.Template.fst
@@ -8,11 +8,12 @@ open Array.Types
 
 (** [array::sum]: decreases clause *)
 unfold
-let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat = admit ()
+let sum_loop_decreases (s : slice u32) (sum0 : u32) (i : usize) : nat =
+  admit ()
 
 (** [array::sum2]: decreases clause *)
 unfold
-let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32)
+let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum0 : u32)
   (i : usize) : nat =
   admit ()
 
-- 
cgit v1.2.3


From 137cc7335e64fcb70c254e7fd2a6fa353fb43e61 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 14:57:38 +0100
Subject: Regenerate the files

---
 tests/fstar/array/Array.Clauses.Template.fst | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tests/fstar/array/Array.Clauses.Template.fst')

diff --git a/tests/fstar/array/Array.Clauses.Template.fst b/tests/fstar/array/Array.Clauses.Template.fst
index 06056d61..08a2925f 100644
--- a/tests/fstar/array/Array.Clauses.Template.fst
+++ b/tests/fstar/array/Array.Clauses.Template.fst
@@ -6,12 +6,14 @@ open Array.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [array::sum]: decreases clause *)
+(** [array::sum]: decreases clause
+    Source: 'src/array.rs', lines 228:0-236:1 *)
 unfold
 let sum_loop_decreases (s : slice u32) (sum0 : u32) (i : usize) : nat =
   admit ()
 
-(** [array::sum2]: decreases clause *)
+(** [array::sum2]: decreases clause
+    Source: 'src/array.rs', lines 238:0-247:1 *)
 unfold
 let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum0 : u32)
   (i : usize) : nat =
-- 
cgit v1.2.3


From 94efdf274eb11f4f1ba9a510eb3dd6e190cfc507 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 29 Nov 2023 12:50:45 +0100
Subject: Regenerate the tests

---
 tests/fstar/array/Array.Clauses.Template.fst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/fstar/array/Array.Clauses.Template.fst')

diff --git a/tests/fstar/array/Array.Clauses.Template.fst b/tests/fstar/array/Array.Clauses.Template.fst
index 08a2925f..84347ab9 100644
--- a/tests/fstar/array/Array.Clauses.Template.fst
+++ b/tests/fstar/array/Array.Clauses.Template.fst
@@ -7,13 +7,13 @@ open Array.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [array::sum]: decreases clause
-    Source: 'src/array.rs', lines 228:0-236:1 *)
+    Source: 'src/array.rs', lines 242:0-250:1 *)
 unfold
 let sum_loop_decreases (s : slice u32) (sum0 : u32) (i : usize) : nat =
   admit ()
 
 (** [array::sum2]: decreases clause
-    Source: 'src/array.rs', lines 238:0-247:1 *)
+    Source: 'src/array.rs', lines 252:0-261:1 *)
 unfold
 let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum0 : u32)
   (i : usize) : nat =
-- 
cgit v1.2.3