diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra
index 33e1448c5..5aef3f771 100644
--- a/pkg/slayers/scion_spec.gobra
+++ b/pkg/slayers/scion_spec.gobra
@@ -810,8 +810,5 @@ ensures  b
 decreases
 pure func (s *SCION) ValidSizeOhpUb(ub []byte) (b bool) {
 	return unfolding s.Mem(ub) in
-		// let pathSlice := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
-		// let pathLen := s.Path.LenSpec(pathSlice) in
-		// CmnHdrLen + s.AddrHdrLenSpecInternal() + pathLen <= len(ub)
 		s.ValidSizeOhpUbOpenInv(ub)
 }
\ No newline at end of file