From 7ecf28dc36f724a4ab4b3b4976421e4e4c397f3b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 23:33:20 +0100
Subject: Rename and regenerate some files

---
 tests/fstar-split/array/Array.Clauses.Template.fst | 21 ---------------------
 1 file changed, 21 deletions(-)
 delete 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
deleted file mode 100644
index b2f2649c..00000000
--- a/tests/fstar-split/array/Array.Clauses.Template.fst
+++ /dev/null
@@ -1,21 +0,0 @@
-(** 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