diff options
Diffstat (limited to 'tests/src/loops.rs')
| -rw-r--r-- | tests/src/loops.rs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tests/src/loops.rs b/tests/src/loops.rs index 2f71d75b..8692c60e 100644 --- a/tests/src/loops.rs +++ b/tests/src/loops.rs @@ -1,3 +1,6 @@ +//@ [coq] aeneas-args=-use-fuel +//@ [fstar] aeneas-args=-decreases-clauses -template-clauses +//@ [fstar] aeneas-args=-split-files use std::vec::Vec; /// No borrows |