add missing 'ghost' (#377)

viperproject · Sep 16, 2024 · 2aebfb2 · 2aebfb2
1 parent b1055a9
commit 2aebfb2
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/verification/utils/bitwise/bitwise-eqs.gobra b/verification/utils/bitwise/bitwise-eqs.gobra
@@ -69,6 +69,7 @@ ensures 3 & 2 == 2
 decreases
 pure func InfoFieldFirstByteSerializationLemmas() bool
 
+ghost
 ensures csum > 0xffff ==>
 	let newCsum := (csum >> 16) + (csum & 0xffff) in
 	newCsum < csum