diff --git a/charon-pin b/charon-pin
index 0a69199c..81a6e3fd 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-821fe7c71300e00c23e47ae97de1e8dc4ac91f9d
+5651efc286dcee58e8e96be869980a40a26af95c
diff --git a/flake.lock b/flake.lock
index 69b0f2da..475ef9e1 100644
--- a/flake.lock
+++ b/flake.lock
@@ -12,11 +12,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1739284006,
-        "narHash": "sha256-HfvqqGbvj1ZQwRqg83IDC9Y2tIm94g/kXgV1QRCzG0Q=",
+        "lastModified": 1739392485,
+        "narHash": "sha256-HbSbQHWCvwOGQQBBZx427rBWEpE8zBB/CWdd9+I6Fxk=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "821fe7c71300e00c23e47ae97de1e8dc4ac91f9d",
+        "rev": "5651efc286dcee58e8e96be869980a40a26af95c",
         "type": "github"
       },
       "original": {
diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out
index ed135506..9ee78651 100644
--- a/tests/src/borrow-check-negative.borrow-check.out
+++ b/tests/src/borrow-check-negative.borrow-check.out
@@ -1,15 +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 23:12-23:14
+Source: 'tests/src/borrow-check-negative.rs', lines 24:12-24:14
 [Error] Can't end abstraction 8 as it is set as non-endable
-Source: 'tests/src/borrow-check-negative.rs', lines 26:0-32:1
+Source: 'tests/src/borrow-check-negative.rs', lines 27:0-33:1
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 40:4-40:11
+Source: 'tests/src/borrow-check-negative.rs', lines 41:4-41:11
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 49:12-49:14
+Source: 'tests/src/borrow-check-negative.rs', lines 50:12-50:14
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 63:12-63:17
+Source: 'tests/src/borrow-check-negative.rs', lines 64:12-64:17
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 78:12-78:17
+Source: 'tests/src/borrow-check-negative.rs', lines 79:12-79:17
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 89:12-89:15
+Source: 'tests/src/borrow-check-negative.rs', lines 90:12-90:15
diff --git a/tests/src/borrow-check-negative.rs b/tests/src/borrow-check-negative.rs
index 697546dd..213ed9e7 100644
--- a/tests/src/borrow-check-negative.rs
+++ b/tests/src/borrow-check-negative.rs
@@ -1,3 +1,4 @@
+//@ charon-args=--skip-borrowck
 //@ [!borrow-check] skip
 //@ [borrow-check] known-failure
 // Some negative tests for borrow checking
diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out
index 8112e292..65c02cfa 100644
--- a/tests/src/loops-borrow-check-negative.borrow-check.out
+++ b/tests/src/loops-borrow-check-negative.borrow-check.out
@@ -1,3 +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-28:1
+Source: 'tests/src/loops-borrow-check-negative.rs', lines 19:0-29:1
diff --git a/tests/src/loops-borrow-check-negative.rs b/tests/src/loops-borrow-check-negative.rs
index 3386d581..eca47999 100644
--- a/tests/src/loops-borrow-check-negative.rs
+++ b/tests/src/loops-borrow-check-negative.rs
@@ -1,3 +1,4 @@
+//@ charon-args=--skip-borrowck
 //@ [!borrow-check] skip
 //@ [borrow-check] known-failure
 
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 35d2c395..d540b80d 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -116,6 +116,9 @@ let run_charon (env : runner_env) (case : Input.t) =
         [
           env.charon_path;
           "--no-cargo";
+          "--rustc-flag=--crate-type=rlib";
+          "--rustc-flag=--allow=unused";
+          "--rustc-flag=--allow=non_snake_case";
           "--hide-marker-traits";
           "--input";
           case.path;
@@ -146,6 +149,7 @@ let run_charon (env : runner_env) (case : Input.t) =
           [
             env.charon_path;
             "--hide-marker-traits";
+            "--rustc-flag=--allow=unused";
             "--dest";
             Filename_unix.realpath env.llbc_dir;
           ]