diff --git a/src/refine/env.rs b/src/refine/env.rs
index 778bcfde..efb86089 100644
--- a/src/refine/env.rs
+++ b/src/refine/env.rs
@@ -1160,7 +1160,7 @@ where
                 pred_args.push(field_term.clone());
 
                 if let Some(p) = field_type.as_pointer() {
-                    if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) {
+                    if p.elem.ty.to_sort() == ty.to_sort() {
                         // TODO: we need recursively defined drop_pred for the recursive ADTs!
                         tracing::warn!("skipping recursive variant");
                         continue;
diff --git a/tests/ui/fail/enum_nested_same_enum_mut_drop.rs b/tests/ui/fail/enum_nested_same_enum_mut_drop.rs
new file mode 100644
index 00000000..e0ae7d60
--- /dev/null
+++ b/tests/ui/fail/enum_nested_same_enum_mut_drop.rs
@@ -0,0 +1,14 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut slot: Option<i64> = None;
+    let o: Option<&mut Option<i64>> = Some(&mut slot);
+    if let Some(s) = o {
+        *s = Some(3);
+    }
+    match slot {
+        Some(y) => assert!(y == 4),
+        None => assert!(false),
+    }
+}
diff --git a/tests/ui/pass/enum_nested_same_enum_mut_drop.rs b/tests/ui/pass/enum_nested_same_enum_mut_drop.rs
new file mode 100644
index 00000000..dfd8f6c7
--- /dev/null
+++ b/tests/ui/pass/enum_nested_same_enum_mut_drop.rs
@@ -0,0 +1,14 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut slot: Option<i64> = None;
+    let o: Option<&mut Option<i64>> = Some(&mut slot);
+    if let Some(s) = o {
+        *s = Some(3);
+    }
+    match slot {
+        Some(y) => assert!(y == 3),
+        None => assert!(false),
+    }
+}