From 553b47dfc79e7b96929c75b9486cc92442ef2bed Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Wed, 8 Jul 2026 13:58:19 +0200
Subject: [PATCH] Fixed opaque annotation example

---
 src/language-annotations.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/language-annotations.md b/src/language-annotations.md
index 4ecbaad..4d2a0e0 100644
--- a/src/language-annotations.md
+++ b/src/language-annotations.md
@@ -17,6 +17,7 @@ To make the definition of an opaque function available at a *specific* applicati
 ```viper,editable,playground
 @opaque()
 function fac(i: Int): Int
+  ensures result >= 1
 {
   i <= 1 ? 1 : i * fac(i - 1)
 }
@@ -24,9 +25,11 @@ function fac(i: Int): Int
 method opaqueClient()
 {
   var x: Int := fac(3)
+  // The postcondition of fac is known, so the following assertion succeeds.
+  assert x >= 1
   // The definition of fac is hidden, so the following assertion
   // fails, even though it is true.
-  assert x == 6
+  assert x == 3 * fac(2)
 }
 
 method revealClient()