From ac857b6c6db68f9a11d8b6aa2505a71003d8dbf1 Mon Sep 17 00:00:00 2001
From: coord_e <me@coord-e.com>
Date: Wed, 1 Apr 2026 01:16:34 +0900
Subject: [PATCH 1/2] Skip analysis for closures defined in skipped defs

---
 src/analyze/crate_.rs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs
index 51e21db..b3e9208 100644
--- a/src/analyze/crate_.rs
+++ b/src/analyze/crate_.rs
@@ -100,6 +100,19 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             return;
         }
 
+        // skip analysis if the def is closure defined in skipped def
+        if let Some(root_local_def_id) = self
+            .tcx
+            .typeck_root_def_id(local_def_id.to_def_id())
+            .as_local()
+        {
+            if root_local_def_id != local_def_id && self.skip_analysis.contains(&root_local_def_id)
+            {
+                self.skip_analysis.insert(local_def_id);
+                return;
+            }
+        }
+
         let target_def_id = if analyzer.is_annotated_as_extern_spec_fn() {
             analyzer.extern_spec_fn_target_def_id()
         } else {

From 75d8b48018b6e01153461c9ac93065194d6066de Mon Sep 17 00:00:00 2001
From: coord_e <me@coord-e.com>
Date: Wed, 1 Apr 2026 01:30:00 +0900
Subject: [PATCH 2/2] Skip borrowck also for closures in formula_fn

---
 src/analyze.rs                               |  8 ++++-
 tests/ui/fail/annot_exists_formula_fn_mut.rs | 30 +++++++++++++++++++
 tests/ui/pass/annot_exists_formula_fn_mut.rs | 31 ++++++++++++++++++++
 3 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 tests/ui/fail/annot_exists_formula_fn_mut.rs
 create mode 100644 tests/ui/pass/annot_exists_formula_fn_mut.rs

diff --git a/src/analyze.rs b/src/analyze.rs
index 85ba3b2..523b56d 100644
--- a/src/analyze.rs
+++ b/src/analyze.rs
@@ -39,10 +39,16 @@ pub fn mir_borrowck_skip_formula_fn(
     local_def_id: rustc_span::def_id::LocalDefId,
 ) -> rustc_middle::query::queries::mir_borrowck::ProvidedValue {
     // TODO: unify impl with local_def::Analyzer
+    // if the def is closure defined in formula_fn
+    let root_def_id = tcx.typeck_root_def_id(local_def_id.to_def_id());
     let is_annotated_as_formula_fn = tcx
         .get_attrs_by_path(local_def_id.to_def_id(), &analyze::annot::formula_fn_path())
         .next()
-        .is_some();
+        .is_some()
+        || tcx
+            .get_attrs_by_path(root_def_id, &analyze::annot::formula_fn_path())
+            .next()
+            .is_some();
 
     if is_annotated_as_formula_fn {
         tracing::debug!(?local_def_id, "skipping borrow check for formula fn");
diff --git a/tests/ui/fail/annot_exists_formula_fn_mut.rs b/tests/ui/fail/annot_exists_formula_fn_mut.rs
new file mode 100644
index 0000000..7a698e8
--- /dev/null
+++ b/tests/ui/fail/annot_exists_formula_fn_mut.rs
@@ -0,0 +1,30 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_requires_incr(m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    x > 0
+}
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_ensures_incr(result: (), m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    thrust_models::exists(|y: i32| !m == y && y > *m)
+}
+
+#[allow(path_statements)]
+fn incr(m: &mut i32, x: i32) {
+    #[thrust::requires_path]
+    _thrust_requires_incr;
+    #[thrust::ensures_path]
+    _thrust_ensures_incr;
+
+    *m -= x;
+}
+
+fn main() {
+    let mut a = 0;
+    incr(&mut a, 1);
+}
diff --git a/tests/ui/pass/annot_exists_formula_fn_mut.rs b/tests/ui/pass/annot_exists_formula_fn_mut.rs
new file mode 100644
index 0000000..12726b6
--- /dev/null
+++ b/tests/ui/pass/annot_exists_formula_fn_mut.rs
@@ -0,0 +1,31 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_requires_incr(m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    x > 0
+}
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_ensures_incr(result: (), m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    thrust_models::exists(|y: i32| !m == y && y > *m)
+}
+
+#[allow(path_statements)]
+fn incr(m: &mut i32, x: i32) {
+    #[thrust::requires_path]
+    _thrust_requires_incr;
+    #[thrust::ensures_path]
+    _thrust_ensures_incr;
+
+    *m += x;
+}
+
+fn main() {
+    let mut a = 0;
+    incr(&mut a, 1);
+    assert!(a > 0);
+}