19 files changed, 289 insertions, 118 deletions

diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options
index c71e01df..5a1e4180 100644
--- a/tests/src/betree/aeneas-test-options
+++ b/tests/src/betree/aeneas-test-options
@@ -1,4 +1,4 @@
 charon-args=--polonius --opaque=betree_utils
-aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
+[!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
 [coq] aeneas-args=-use-fuel
 [fstar] aeneas-args=-decreases-clauses -template-clauses
diff --git a/tests/src/betree/src/betree.rs b/tests/src/betree/src/betree.rs
index 12f2847d..8ba07824 100644
--- a/tests/src/betree/src/betree.rs
+++ b/tests/src/betree/src/betree.rs
@@ -274,25 +274,41 @@ pub fn upsert_update(prev: Option<Value>, st: UpsertFunState) -> Value {
 
 impl<T> List<T> {
     fn len(&self) -> u64 {
-        match self {
-            List::Nil => 0,
-            List::Cons(_, tl) => 1 + tl.len(),
+        let mut l = self;
+        let mut len = 0;
+        while let List::Cons(_, tl) = l {
+            len += 1;
+            l = tl;
         }
+        len
     }
 
     /// Split a list at a given length
-    fn split_at(self, n: u64) -> (List<T>, List<T>) {
-        if n == 0 {
-            (List::Nil, self)
-        } else {
-            match self {
+    fn split_at(self, mut n: u64) -> (List<T>, List<T>) {
+        let mut beg = List::Nil;
+        let mut end = self;
+        while n > 0 {
+            match end {
                 List::Nil => unreachable!(),
-                List::Cons(hd, tl) => {
-                    let (ls0, ls1) = tl.split_at(n - 1);
-                    (List::Cons(hd, Box::new(ls0)), ls1)
+                List::Cons(hd, mut tl) => {
+                    n -= 1;
+                    end = *tl;
+                    *tl = beg;
+                    beg = List::Cons(hd, tl);
                 }
             }
         }
+        (beg.reverse(), end)
+    }
+
+    fn reverse(mut self) -> Self {
+        let mut out = List::Nil;
+        while let List::Cons(hd, mut tl) = self {
+            self = *tl;
+            *tl = out;
+            out = List::Cons(hd, tl);
+        }
+        out
     }
 
     /// Push an element at the front of the list.
@@ -337,17 +353,20 @@ impl<T> Map<Key, T> {
     /// Note that the bindings in the map are supposed to be sorted in
     /// order of increasing keys.
     fn partition_at_pivot(self, pivot: Key) -> (Map<Key, T>, Map<Key, T>) {
-        match self {
-            List::Nil => (List::Nil, List::Nil),
-            List::Cons(hd, tl) => {
-                if hd.0 >= pivot {
-                    (List::Nil, List::Cons(hd, tl))
-                } else {
-                    let (ls0, ls1) = tl.partition_at_pivot(pivot);
-                    (List::Cons(hd, Box::new(ls0)), ls1)
-                }
+        let mut beg = List::Nil;
+        let mut end = List::Nil;
+        let mut curr = self;
+        while let List::Cons(hd, mut tl) = curr {
+            curr = *tl;
+            if hd.0 >= pivot {
+                *tl = end;
+                end = List::Cons(hd, tl);
+            } else {
+                *tl = beg;
+                beg = List::Cons(hd, tl);
             }
         }
+        (beg.reverse(), end.reverse())
     }
 }
 
@@ -443,14 +462,11 @@ impl Node {
     /// Apply a list of message to ourselves: leaf node case
     fn apply_messages_to_leaf<'a>(
         bindings: &'a mut Map<Key, Value>,
-        new_msgs: List<(Key, Message)>,
+        mut new_msgs: List<(Key, Message)>,
     ) {
-        match new_msgs {
-            List::Nil => (),
-            List::Cons(new_msg, new_msgs_tl) => {
-                Node::apply_to_leaf(bindings, new_msg.0, new_msg.1);
-                Node::apply_messages_to_leaf(bindings, *new_msgs_tl);
-            }
+        while let List::Cons(new_msg, new_msgs_tl) = new_msgs {
+            Node::apply_to_leaf(bindings, new_msg.0, new_msg.1);
+            new_msgs = *new_msgs_tl;
         }
     }
 
@@ -501,14 +517,11 @@ impl Node {
     /// Apply a list of message to ourselves: internal node case
     fn apply_messages_to_internal<'a>(
         msgs: &'a mut Map<Key, Message>,
-        new_msgs: List<(Key, Message)>,
+        mut new_msgs: List<(Key, Message)>,
     ) {
-        match new_msgs {
-            List::Nil => (),
-            List::Cons(new_msg, new_msgs_tl) => {
-                Node::apply_to_internal(msgs, new_msg.0, new_msg.1);
-                Node::apply_messages_to_internal(msgs, *new_msgs_tl);
-            }
+        while let List::Cons(new_msg, new_msgs_tl) = new_msgs {
+            Node::apply_to_internal(msgs, new_msg.0, new_msg.1);
+            new_msgs = *new_msgs_tl;
         }
     }
 
@@ -633,38 +646,34 @@ impl Node {
 
     /// Lookup a value in a list of bindings.
     /// Note that the values should be stored in order of increasing key.
-    fn lookup_in_bindings(key: Key, bindings: &Map<Key, Value>) -> Option<Value> {
-        match bindings {
-            List::Nil => Option::None,
-            List::Cons(hd, tl) => {
-                if hd.0 == key {
-                    Option::Some(hd.1)
-                } else if hd.0 > key {
-                    Option::None
-                } else {
-                    Node::lookup_in_bindings(key, tl)
-                }
+    fn lookup_in_bindings(key: Key, mut bindings: &Map<Key, Value>) -> Option<Value> {
+        while let List::Cons(hd, tl) = bindings {
+            if hd.0 == key {
+                return Option::Some(hd.1);
+            } else if hd.0 > key {
+                return Option::None;
+            } else {
+                bindings = tl;
             }
         }
+        Option::None
     }
 
     /// Lookup a value in a list of bindings, and return a borrow to the position
     /// where the value is (or should be inserted, if the key is not in the bindings).
     fn lookup_mut_in_bindings<'a>(
         key: Key,
-        bindings: &'a mut Map<Key, Value>,
+        mut bindings: &'a mut Map<Key, Value>,
     ) -> &'a mut Map<Key, Value> {
-        match bindings {
-            List::Nil => bindings,
-            List::Cons(hd, tl) => {
-                // This requires Polonius
-                if hd.0 >= key {
-                    bindings
-                } else {
-                    Node::lookup_mut_in_bindings(key, tl)
-                }
+        while let List::Cons(hd, tl) = bindings {
+            // This requires Polonius
+            if hd.0 >= key {
+                break;
+            } else {
+                bindings = tl;
             }
         }
+        bindings
     }
 
     /// Filter all the messages which concern [key].
@@ -672,34 +681,28 @@ impl Node {
     /// Note that the stack of messages must start with a message for [key]:
     /// we stop filtering at the first message which is not about [key].
     fn filter_messages_for_key<'a>(key: Key, msgs: &'a mut Map<Key, Message>) {
-        match msgs {
-            List::Nil => (),
-            List::Cons((k, _), _) => {
-                if *k == key {
-                    msgs.pop_front();
-                    Node::filter_messages_for_key(key, msgs);
-                } else {
-                    // Stop
-                    ()
-                }
+        while let List::Cons((k, _), _) = msgs {
+            if *k == key {
+                msgs.pop_front();
+            } else {
+                // Stop
+                break;
             }
         }
     }
 
     fn lookup_first_message_after_key<'a>(
         key: Key,
-        msgs: &'a mut Map<Key, Message>,
+        mut msgs: &'a mut Map<Key, Message>,
     ) -> &'a mut Map<Key, Message> {
-        match msgs {
-            List::Nil => msgs,
-            List::Cons((k, _), next_msgs) => {
-                if *k == key {
-                    Node::lookup_first_message_after_key(key, next_msgs)
-                } else {
-                    msgs
-                }
+        while let List::Cons((k, _), next_msgs) = msgs {
+            if *k == key {
+                msgs = next_msgs;
+            } else {
+                break;
             }
         }
+        return msgs;
     }
 
     /// Returns the value bound to a key.
@@ -788,24 +791,22 @@ impl Node {
     /// of the list).
     fn lookup_first_message_for_key<'a>(
         key: Key,
-        msgs: &'a mut Map<Key, Message>,
+        mut msgs: &'a mut Map<Key, Message>,
     ) -> &'a mut Map<Key, Message> {
-        match msgs {
-            List::Nil => msgs,
-            List::Cons(x, next_msgs) => {
-                // Rk.: we need Polonius here
-                // We wouldn't need Polonius if directly called the proper
-                // function to make the modifications here (because we wouldn't
-                // need to return anything). However, it would not be very
-                // idiomatic, especially with regards to the fact that we will
-                // rewrite everything with loops at some point.
-                if x.0 >= key {
-                    msgs
-                } else {
-                    Node::lookup_first_message_for_key(key, next_msgs)
-                }
+        while let List::Cons(x, next_msgs) = msgs {
+            // Rk.: we need Polonius here
+            // We wouldn't need Polonius if directly called the proper
+            // function to make the modifications here (because we wouldn't
+            // need to return anything). However, it would not be very
+            // idiomatic, especially with regards to the fact that we will
+            // rewrite everything with loops at some point.
+            if x.0 >= key {
+                return msgs;
+            } else {
+                msgs = next_msgs;
             }
         }
+        msgs
     }
 
     /// Apply the upserts from the current messages stack to a looked up value.
@@ -816,8 +817,8 @@ impl Node {
     /// Note that if there are no more upserts to apply, then the value must be
     /// `Some`. Also note that we use the invariant that in the message stack,
     /// upsert messages are sorted from the first to the last to apply.
-    fn apply_upserts(msgs: &mut Map<Key, Message>, prev: Option<Value>, key: Key) -> Value {
-        if msgs.head_has_key(key) {
+    fn apply_upserts(msgs: &mut Map<Key, Message>, mut prev: Option<Value>, key: Key) -> Value {
+        while msgs.head_has_key(key) {
             // Pop the front message.
             // Note that it *must* be an upsert.
             let msg = msgs.pop_front();
@@ -825,9 +826,8 @@ impl Node {
                 Message::Upsert(s) => {
                     // Apply the update
                     let v = upsert_update(prev, s);
-                    let prev = Option::Some(v);
+                    prev = Option::Some(v);
                     // Continue
-                    Node::apply_upserts(msgs, prev, key)
                 }
                 _ => {
                     // Unreachable: we can only have [Upsert] messages
@@ -835,13 +835,12 @@ impl Node {
                     unreachable!();
                 }
             }
-        } else {
-            // We applied all the upsert messages: simply put an [Insert]
-            // message and return the value.
-            let v = prev.unwrap();
-            msgs.push_front((key, Message::Insert(v)));
-            return v;
         }
+        // We applied all the upsert messages: simply put an [Insert]
+        // message and return the value.
+        let v = prev.unwrap();
+        msgs.push_front((key, Message::Insert(v)));
+        v
     }
 }
 
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index fda8eff3..be12cea0 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,4 +1,4 @@
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! Exercise the bitwise operations
 
diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..dc9dd5a7
--- /dev/null
+++ b/tests/src/borrow-check-negative.borrow-check.out
@@ -0,0 +1,15 @@
+[Info ] Imported: tests/llbc/borrow_check_negative.llbc
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 17:4-24:1
+[Error] Can't end abstraction 8 as it is set as non-endable
+Source: 'tests/src/borrow-check-negative.rs', lines 26:0-26:76
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 87:4-90:1
diff --git a/tests/src/borrow-check-negative.rs b/tests/src/borrow-check-negative.rs
new file mode 100644
index 00000000..697546dd
--- /dev/null
+++ b/tests/src/borrow-check-negative.rs
@@ -0,0 +1,90 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+// Some negative tests for borrow checking
+
+// This succeeds
+fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y
+    }
+}
+
+pub fn choose_test() {
+    let mut x = 0;
+    let mut y = 0;
+    let z = choose(true, &mut x, &mut y);
+    *z += 1;
+    assert!(*z == 1);
+    // drop(z)
+    assert!(x == 1);
+    assert!(y == 0);
+    assert!(*z == 1); // z is not valid anymore
+}
+
+fn choose_wrong<'a, 'b, T>(b: bool, x: &'a mut T, y: &'b mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y // Expected lifetime 'a
+    }
+}
+
+fn test_mut1(b: bool) {
+    let mut x = 0;
+    let mut y = 1;
+    let z = if b { &mut x } else { &mut y };
+    *z += 1;
+    assert!(x >= 0);
+    *z += 1; // z is not valid anymore
+}
+
+#[allow(unused_assignments)]
+fn test_mut2(b: bool) {
+    let mut x = 0;
+    let mut y = 1;
+    let z = if b { &x } else { &y };
+    x += 1;
+    assert!(*z == 0); // z is not valid anymore
+}
+
+fn test_move1<T>(x: T) -> T {
+    let _ = x;
+    return x; // x has been moved
+}
+
+pub fn refs_test1() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    **ppx = 1;
+    assert!(x == 1);
+    assert!(**ppx == 1); // ppx has ended
+}
+
+pub fn refs_test2() {
+    let mut x = 0;
+    let mut y = 1;
+    let mut px = &mut x;
+    let py = &mut y;
+    let ppx = &mut px;
+    *ppx = py;
+    **ppx = 2;
+    assert!(*px == 2);
+    assert!(x == 0);
+    assert!(*py == 2);
+    assert!(y == 2);
+    assert!(**ppx == 2); // ppx has ended
+}
+
+pub fn test_box1() {
+    use std::ops::Deref;
+    use std::ops::DerefMut;
+    let mut b: Box<i32> = Box::new(0);
+    let x0 = b.deref_mut();
+    *x0 = 1;
+    let x1 = b.deref();
+    assert!(*x1 == 1);
+    assert!(*x0 == 1); // x0 has ended
+}
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
index ac24dcd4..71d7c557 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! Tests with constants
 
diff --git a/tests/src/external.rs b/tests/src/external.rs
index baea76e4..00acdb0b 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,6 +1,6 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-state -split-files
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-state -split-files
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! This module uses external types and functions
 
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 19832a84..7dda2404 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--opaque=utils
-//@ aeneas-args=-state -split-files
+//@ [!borrow-check] aeneas-args=-state -split-files
 //@ [coq] aeneas-args=-use-fuel
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 //@ [lean] aeneas-args=-no-gen-lib-entry
diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out
new file mode 100644
index 00000000..34eb75f8
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.borrow-check.out
@@ -0,0 +1,5 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_fail.llbc
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 7:4-12:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1
diff --git a/tests/src/loops-borrow-check-fail.rs b/tests/src/loops-borrow-check-fail.rs
new file mode 100644
index 00000000..24be052c
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.rs
@@ -0,0 +1,21 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// We need to use the general rules for joining the loans
+fn loop_reborrow_mut() {
+    let mut x = 0;
+    let mut px = &mut x;
+    while *px > 0 {
+        x += 1;
+        px = &mut x;
+    }
+}
+
+// We need to imrpove [prepare_ashared_loans]
+fn iter_local_shared_borrow() {
+    let mut x = 0;
+    let mut p = &x;
+    loop {
+        p = &(*p);
+    }
+}
diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..093d8b8a
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.borrow-check.out
@@ -0,0 +1,3 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_negative.llbc
+[Error] Can't end abstraction 16 as it is set as non-endable
+Source: 'tests/src/loops-borrow-check-negative.rs', lines 18:0-18:66
diff --git a/tests/src/loops-borrow-check-negative.rs b/tests/src/loops-borrow-check-negative.rs
new file mode 100644
index 00000000..3386d581
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.rs
@@ -0,0 +1,28 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// This succeeds
+fn loop_a<'a>(a: &'a mut u32, b: &'a mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b
+    }
+}
+
+// This fails
+fn loop_a_b<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b // Expect lifetime 'a
+    }
+}
diff --git a/tests/src/loops-borrow-check.rs b/tests/src/loops-borrow-check.rs
new file mode 100644
index 00000000..ab300b37
--- /dev/null
+++ b/tests/src/loops-borrow-check.rs
@@ -0,0 +1,10 @@
+//@ [!borrow-check] skip
+
+fn iter_local_mut_borrow() {
+    let mut x = 0;
+    let mut p = &mut x;
+    loop {
+        p = &mut (*p);
+        *p += 1;
+    }
+}
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index 6d638644..e2ed3abc 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -1,17 +1,17 @@
 [Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
-[Error] In file Translate.ml, line 812:
+[Error] In file Translate.ml, line 813:
 Mutually recursive trait declarations are not supported
 
 Uncaught exception:
   
   (Failure
-    "In file Translate.ml, line 812:\
-   \nIn file Translate.ml, line 812:\
+    "In file Translate.ml, line 813:\
+   \nIn file Translate.ml, line 813:\
    \nMutually recursive trait declarations are not supported")
 
 Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 835, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 953, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1501, characters 5-42
-Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42
+Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66
diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs
index 351763b2..9bc4ca63 100644
--- a/tests/src/mutually-recursive-traits.rs
+++ b/tests/src/mutually-recursive-traits.rs
@@ -1,6 +1,6 @@
 //@ [lean] known-failure
-//@ [coq,fstar] skip
-//@ subdir=misc
+//@ [!lean] skip
+//@ [lean] subdir=misc
 pub trait Trait1 {
     type T: Trait2;
 }
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 6d3074ef..11c4a695 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! This module doesn't contain **functions which use nested borrows in their
 //! signatures**, and doesn't contain functions with loops.
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
index 6a4a7c31..d9fb1032 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! The examples from the ICFP submission, all in one place.
 
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index b029ad02..084441aa 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--polonius
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 #![allow(dead_code)]
 
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
index f8490e76..9fd91752 100644
--- a/tests/src/string-chars.rs
+++ b/tests/src/string-chars.rs
@@ -1,5 +1,5 @@
 //@ [lean] known-failure
-//@ [coq,fstar] skip
+//@ [!lean] skip
 //@ no-check-output
 fn main() {
     let s = "hello";