diff options
Diffstat (limited to 'tests/src/infinite-loop.rs')
-rw-r--r-- | tests/src/infinite-loop.rs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs new file mode 100644 index 00000000..0e247d20 --- /dev/null +++ b/tests/src/infinite-loop.rs @@ -0,0 +1,10 @@ +//@ [coq,fstar] aeneas-args=-use-fuel +//@ [coq,fstar] subdir=misc +// FIXME: make it work +fn bar() {} + +fn foo() { + loop { + bar() + } +} |