From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 17:33:56 +0200
Subject: Add some tests

---
 tests/src/infinite-loop.rs | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 tests/src/infinite-loop.rs

(limited to 'tests/src/infinite-loop.rs')

diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs
new file mode 100644
index 00000000..906fc1fa
--- /dev/null
+++ b/tests/src/infinite-loop.rs
@@ -0,0 +1,11 @@
+//@ [coq,fstar,lean] skip
+//@ [coq,fstar] aeneas-args=-use-fuel
+//@ [coq,fstar] subdir=misc
+// FIXME: make it work
+fn bar() {}
+
+fn foo() {
+    loop {
+        bar()
+    }
+}
-- 
cgit v1.2.3


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/src/infinite-loop.rs | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tests/src/infinite-loop.rs')

diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs
index 906fc1fa..0e247d20 100644
--- a/tests/src/infinite-loop.rs
+++ b/tests/src/infinite-loop.rs
@@ -1,4 +1,3 @@
-//@ [coq,fstar,lean] skip
 //@ [coq,fstar] aeneas-args=-use-fuel
 //@ [coq,fstar] subdir=misc
 // FIXME: make it work
-- 
cgit v1.2.3