From 1226e2b61cc374a524e9cbbc43594371b4b313e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Tue, 7 Jan 2025 18:09:20 +0100
Subject: [PATCH] Update pkg/slayers/scion_spec.gobra

---
 pkg/slayers/scion_spec.gobra | 3 ---
 1 file changed, 3 deletions(-)

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