Merge pull request #219 from AeneasVerif/son/infinite

Fix the infinite loop test

1 files changed, 24 insertions, 0 deletions

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
+