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-split/array/Array.Clauses.Template.fst | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 tests/fstar-split/array/Array.Clauses.Template.fst

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

diff --git a/tests/fstar-split/array/Array.Clauses.Template.fst b/tests/fstar-split/array/Array.Clauses.Template.fst
new file mode 100644
index 00000000..b2f2649c
--- /dev/null
+++ b/tests/fstar-split/array/Array.Clauses.Template.fst
@@ -0,0 +1,21 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [array]: templates for the decreases clauses *)
+module Array.Clauses.Template
+open Primitives
+open Array.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [array::sum]: decreases clause
+    Source: 'src/array.rs', lines 242:0-250:1 *)
+unfold
+let sum_loop_decreases (s : slice u32) (sum1 : u32) (i : usize) : nat =
+  admit ()
+
+(** [array::sum2]: decreases clause
+    Source: 'src/array.rs', lines 252:0-261:1 *)
+unfold
+let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum1 : u32)
+  (i : usize) : nat =
+  admit ()
+
-- 
cgit v1.2.3