diff --git a/silver b/silver
index 63c30b18..16a8d42e 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 63c30b18fdafd81d90eabbc8bccfd13a31becd61
+Subproject commit 16a8d42e990aca50d7a0a6a481f8675b490040af
diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
index 943b7573..f9d498d4 100644
--- a/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
+++ b/src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
@@ -638,7 +638,6 @@ class DefaultHeapModule(val verifier: Verifier)
                 Havoc(newVersion) ++
                 currentHeapAssignUpdate(loc, newVersion)
 
-              If(UnExp(Not,hasDirectPerm(loc)), resetPredicateInfo, Nil) ++
                 addPermissionToPMask(loc) ++ stateModule.assumeGoodState}  )
           case sil.FieldAssign(lhs, rhs) =>
             if(usingOldState) sys.error("heap module: field is assigned while using old state")