From 26c1cea9c6db160593d27ed6652b82baf392f64d Mon Sep 17 00:00:00 2001
From: coord_e <me@coord-e.com>
Date: Mon, 22 Jun 2026 19:25:00 +0900
Subject: [PATCH] Add test cases of #138

---
 tests/ui/fail/closure_receiver_mut_model.rs | 24 +++++++++++++++++++++
 tests/ui/pass/closure_receiver_mut_model.rs | 24 +++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 tests/ui/fail/closure_receiver_mut_model.rs
 create mode 100644 tests/ui/pass/closure_receiver_mut_model.rs

diff --git a/tests/ui/fail/closure_receiver_mut_model.rs b/tests/ui/fail/closure_receiver_mut_model.rs
new file mode 100644
index 00000000..337a20e9
--- /dev/null
+++ b/tests/ui/fail/closure_receiver_mut_model.rs
@@ -0,0 +1,24 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+use thrust_models::{exists, model::{Mut, Int}};
+
+#[thrust_macros::ensures(exists(|g, h, i: Int|
+  thrust_macros::post!(Mut::new(*f, g)(), i)
+  && thrust_macros::post!(Mut::new(h, !f)(), result)
+))]
+fn call_twice<F: FnMut() -> i32>(f: &mut F) -> i32 {
+    f();
+    f()
+}
+
+fn main() {
+    let mut x = 1;
+    let mut f = move || {
+        x += 1;
+        x
+    };
+    let r = call_twice(&mut f);
+    assert!(r == 3);
+}
diff --git a/tests/ui/pass/closure_receiver_mut_model.rs b/tests/ui/pass/closure_receiver_mut_model.rs
new file mode 100644
index 00000000..f26c4318
--- /dev/null
+++ b/tests/ui/pass/closure_receiver_mut_model.rs
@@ -0,0 +1,24 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+use thrust_models::{exists, model::{Mut, Int}};
+
+#[thrust_macros::ensures(exists(|g, i: Int|
+  thrust_macros::post!(Mut::new(*f, g)(), i)
+  && thrust_macros::post!(Mut::new(g, !f)(), result)
+))]
+fn call_twice<F: FnMut() -> i32>(f: &mut F) -> i32 {
+    f();
+    f()
+}
+
+fn main() {
+    let mut x = 1;
+    let mut f = move || {
+        x += 1;
+        x
+    };
+    let r = call_twice(&mut f);
+    assert!(r == 3);
+}