diff --git a/prusti-common/src/vir/optimizations/methods/purifier.rs b/prusti-common/src/vir/optimizations/methods/purifier.rs
index f465e7c54bf..07f1dd42756 100644
--- a/prusti-common/src/vir/optimizations/methods/purifier.rs
+++ b/prusti-common/src/vir/optimizations/methods/purifier.rs
@@ -258,6 +258,19 @@ impl ast::StmtWalker for VarCollector {
         }
         self.is_pure_context = old_pure_context;
     }
+    fn walk_exhale(
+        &mut self,
+        ast::Exhale {
+            expr,
+            ..
+        }: &ast::Exhale,
+    ) {
+        // When a field is fully exhaled, the purified encoding should havoc the purified variable.
+        // This pass currently does not generate such havoc statement, which is why we mark the
+        // variables used in an havoc as non-purifiable.
+        // See: https://github.com/viperproject/prusti-dev/pull/1464
+        self.walk_expr(expr);
+    }
 }
 
 struct VarPurifier {