diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
index 943b7573..dd1999e0 100644
--- a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
+++ b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
@@ -640,6 +640,9 @@ class DefaultHeapModule(val verifier: Verifier)
 
               If(UnExp(Not,hasDirectPerm(loc)), resetPredicateInfo, Nil) ++
                 addPermissionToPMask(loc) ++ stateModule.assumeGoodState}  )
+          case sil.Unfold(sil.PredicateAccessPredicate(loc@sil.PredicateAccess(_, _), _)) =>
+            val knownfolded_update: Stmt = curHeapAssignUpdatePredWandMask(predicateMask(loc).maskField, zeroPMask)
+            stmt ++ knownfolded_update
           case sil.FieldAssign(lhs, rhs) =>
             if(usingOldState) sys.error("heap module: field is assigned while using old state")
             stmt ++ (currentHeapAssignUpdate(lhs, translateExp(rhs))) // after all checks