diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala index 64235d074..5015bfd35 100644 --- a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala +++ b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala @@ -331,7 +331,9 @@ case class EncodePermissionStratification[Pre <: Generation]( } case cp: ChorPerm[Pre] => - ??? // Unexpected chorperm with something else than a FieldLocation + specializing.having(EndpointName[Post](succ(cp.endpoint.decl))(cp.o)) { + Perm(dispatch(cp.loc), dispatch(cp.perm))(expr.o) + } case Perm(loc: FieldLocation[Pre], perm) if specializing.nonEmpty => makeWrappedPerm(loc, perm, specializing.top)(expr.o)