From a4efda3fd27364316bd65f34bc3eac3fd2cbf87d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 16:13:19 +0100
Subject: Remove the split test files for F*

---
 .../fstar-split/arrays/Arrays.Clauses.Template.fst  | 21 ---------------------
 1 file changed, 21 deletions(-)
 delete mode 100644 tests/fstar-split/arrays/Arrays.Clauses.Template.fst

(limited to 'tests/fstar-split/arrays/Arrays.Clauses.Template.fst')

diff --git a/tests/fstar-split/arrays/Arrays.Clauses.Template.fst b/tests/fstar-split/arrays/Arrays.Clauses.Template.fst
deleted file mode 100644
index 8cc32583..00000000
--- a/tests/fstar-split/arrays/Arrays.Clauses.Template.fst
+++ /dev/null
@@ -1,21 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [arrays]: templates for the decreases clauses *)
-module Arrays.Clauses.Template
-open Primitives
-open Arrays.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [arrays::sum]: decreases clause
-    Source: 'src/arrays.rs', lines 242:0-250:1 *)
-unfold
-let sum_loop_decreases (s : slice u32) (sum1 : u32) (i : usize) : nat =
-  admit ()
-
-(** [arrays::sum2]: decreases clause
-    Source: 'src/arrays.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