From ae075db15638ee8878bebe3d31affb1aa320e90f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 28 May 2024 18:05:01 +0200
Subject: Reactivate the infinite-loop.rs test

---
 tests/fstar/misc/InfiniteLoop.fst | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/fstar/misc/InfiniteLoop.fst

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

diff --git a/tests/fstar/misc/InfiniteLoop.fst b/tests/fstar/misc/InfiniteLoop.fst
new file mode 100644
index 00000000..4e7c8c06
--- /dev/null
+++ b/tests/fstar/misc/InfiniteLoop.fst
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [infinite_loop] *)
+module InfiniteLoop
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [infinite_loop::bar]:
+    Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 *)
+let bar : result unit =
+  Ok ()
+
+(** [infinite_loop::foo]: loop 0:
+    Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 *)
+let rec foo_loop (n : nat) : result unit =
+  if is_zero n
+  then Fail OutOfFuel
+  else let n1 = decrease n in let* _ = bar in foo_loop n1
+
+(** [infinite_loop::foo]:
+    Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 *)
+let foo (n : nat) : result unit =
+  foo_loop n
+
-- 
cgit v1.2.3