--- /dev/null
+-- { dg-do compile }
+-- { dg-options "-gnata" }
+
+procedure Post_Block is
+ package Pack is
+ function Size (X : Integer) return Integer;
+ pragma Postcondition (Size'Result = Value (X)'Length); -- OK
+ pragma Postcondition (Value (X)'Length = Size'Result);
+
+ -- Calling the following requires a transient block.
+ function Value (X : Integer) return String;
+ end Pack;
+
+ package body Pack is
+ function Size (X : Integer) return Integer is
+ begin
+ return 0;
+ end;
+
+ function Value (X : Integer) return String is
+ begin
+ return Integer'image (X);
+ end;
+ end Pack;
+begin
+ null;
+end;