Fixing new opaque annotation example

[marcoeilers]

The previous example

• used an assertion that would have failed to verify even if the function was not opaque
• did not demonstrate that function postconditions are known to callers even for opaque functions