2 files changed, 1 insertions, 21 deletions

diff --git a/tests/src/string-chars.lean.out b/tests/src/string-chars.lean.out
deleted file mode 100644
index 0d28744f..00000000
--- a/tests/src/string-chars.lean.out
+++ /dev/null
@@ -1,21 +0,0 @@
-[Info ] Imported: tests/llbc/string_chars.llbc
-[Error] In file SymbolicToPure.ml, line 588:
-ADTs containing borrows are not supported yet
-Source: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20
-
-Uncaught exception:
-  
-  (Failure
-    "In file SymbolicToPure.ml, line 588:\
-   \nIn file SymbolicToPure.ml, line 588:\
-   \nADTs containing borrows are not supported yet\
-   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20\
-   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20")
-
-Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
-Called from Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 588, characters 2-113
-Called from Aeneas__SymbolicToPure.translate_type_decls.(fun) in file "SymbolicToPure.ml", line 3923, characters 15-42
-Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
-Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 229, characters 19-64
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 981, characters 4-33
-Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
index 5ba9a2d6..f8490e76 100644
--- a/tests/src/string-chars.rs
+++ b/tests/src/string-chars.rs
@@ -1,5 +1,6 @@
 //@ [lean] known-failure
 //@ [coq,fstar] skip
+//@ no-check-output
 fn main() {
     let s = "hello";
     let _chs: Vec<char> = s.chars().collect();