diff --git a/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala b/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala
index 365c365363..b5692c06d5 100644
--- a/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala
+++ b/rewrite/src/main/java/vct/col/rewrite/lang/LangPVLToCol.scala
@@ -63,7 +63,7 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
           UnitAccountedPredicate(AstBuildHelpers.foldStar(cls.declarations.collect {
             case field: InstanceField[Pre] =>
               fieldPerm[Post](result, rw.succ(field), WritePerm())
-          })), tt, Nil, Nil, Nil, None,
+          }) &* IdleToken(result)), tt, Nil, Nil, Nil, None,
         )(TrueSatisfiable)
       )(defaultBlame)))
     }