diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra
index b933026cb..b12aec326 100644
--- a/pkg/slayers/path/scion/base_spec.gobra
+++ b/pkg/slayers/path/scion/base_spec.gobra
@@ -45,13 +45,6 @@ pred (b *Base) Mem() {
 	(0 < b.NumINF ==> 0 < b.NumHops)
 }
 
-ghost 
-ensures res
-decreases
-pure func validMetaLenInPath() (res bool) {
-	return MetaLen == path.MetaLen
-}
-
 ghost
 decreases
 pure func (b Base) ValidCurrInfSpec() bool {
diff --git a/pkg/slayers/path/scion/base_spec_test.gobra b/pkg/slayers/path/scion/base_spec_test.gobra
index d48116d9b..5d07d6a53 100644
--- a/pkg/slayers/path/scion/base_spec_test.gobra
+++ b/pkg/slayers/path/scion/base_spec_test.gobra
@@ -16,7 +16,18 @@
 
 package scion
 
+import (
+	"github.com/scionproto/scion/pkg/slayers/path"
+)
+
 func canAllocateBase() {
 	b := &Base{}
 	fold b.Mem()
+}
+
+ghost 
+ensures res
+decreases
+pure func validMetaLenInPath() (res bool) {
+	return MetaLen == path.MetaLen
 }
\ No newline at end of file