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);
+}